:: ORDINAL4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
let L be Ordinal-Sequence;
cluster last L -> ordinal ;
coherence
last L is ordinal
;
end;

theorem :: ORDINAL4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fi being Ordinal-Sequence
for A being Ordinal st dom fi = succ A holds
( last fi is_limes_of fi & lim fi = last fi )
proof end;

definition
let fi, psi be T-Sequence;
func fi ^ psi -> T-Sequence means :Def1: :: ORDINAL4:def 1
( dom it = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
it . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
it . ((dom fi) +^ A) = psi . A ) );
existence
ex b1 being T-Sequence st
( dom b1 = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
b1 . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
b1 . ((dom fi) +^ A) = psi . A ) )
proof end;
uniqueness
for b1, b2 being T-Sequence st dom b1 = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
b1 . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
b1 . ((dom fi) +^ A) = psi . A ) & dom b2 = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
b2 . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
b2 . ((dom fi) +^ A) = psi . A ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines ^ ORDINAL4:def 1 :
for fi, psi, b3 being T-Sequence holds
( b3 = fi ^ psi iff ( dom b3 = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
b3 . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
b3 . ((dom fi) +^ A) = psi . A ) ) );

registration
let fi, psi be Ordinal-Sequence;
cluster fi ^ psi -> Ordinal-yielding ;
coherence
fi ^ psi is Ordinal-yielding
proof end;
end;

theorem :: ORDINAL4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: ORDINAL4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for psi, fi being Ordinal-Sequence
for A being Ordinal st A is_limes_of psi holds
A is_limes_of fi ^ psi
proof end;

theorem :: ORDINAL4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fi being Ordinal-Sequence
for A, B being Ordinal st A is_limes_of fi holds
B +^ A is_limes_of B +^ fi
proof end;

Lm1: for fi being Ordinal-Sequence
for A being Ordinal st A is_limes_of fi holds
dom fi <> {}
proof end;

theorem Th5: :: ORDINAL4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fi being Ordinal-Sequence
for A, B being Ordinal st A is_limes_of fi holds
A *^ B is_limes_of fi *^ B
proof end;

theorem Th6: :: ORDINAL4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fi, psi being Ordinal-Sequence
for B, C being Ordinal st dom fi = dom psi & B is_limes_of fi & C is_limes_of psi & ( for A being Ordinal st A in dom fi holds
fi . A c= psi . A or for A being Ordinal st A in dom fi holds
fi . A in psi . A ) holds
B c= C
proof end;

theorem :: ORDINAL4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fi being Ordinal-Sequence
for A being Ordinal
for f1, f2 being Ordinal-Sequence st dom f1 = dom fi & dom fi = dom f2 & A is_limes_of f1 & A is_limes_of f2 & ( for A being Ordinal st A in dom fi holds
( f1 . A c= fi . A & fi . A c= f2 . A ) ) holds
A is_limes_of fi
proof end;

theorem Th8: :: ORDINAL4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fi being Ordinal-Sequence st dom fi <> {} & dom fi is_limit_ordinal & fi is increasing holds
( sup fi is_limes_of fi & lim fi = sup fi )
proof end;

theorem Th9: :: ORDINAL4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fi being Ordinal-Sequence
for A, B being Ordinal st fi is increasing & A c= B & B in dom fi holds
fi . A c= fi . B
proof end;

theorem Th10: :: ORDINAL4:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fi being Ordinal-Sequence
for A being Ordinal st fi is increasing & A in dom fi holds
A c= fi . A
proof end;

theorem Th11: :: ORDINAL4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for phi being Ordinal-Sequence
for A being Ordinal st phi is increasing holds
phi " A is Ordinal
proof end;

theorem Th12: :: ORDINAL4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being Ordinal-Sequence st f1 is increasing holds
f2 * f1 is Ordinal-Sequence
proof end;

theorem :: ORDINAL4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being Ordinal-Sequence st f1 is increasing & f2 is increasing holds
ex phi being Ordinal-Sequence st
( phi = f1 * f2 & phi is increasing )
proof end;

theorem Th14: :: ORDINAL4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fi being Ordinal-Sequence
for A being Ordinal
for f1, f2 being Ordinal-Sequence st f1 is increasing & A is_limes_of f2 & sup (rng f1) = dom f2 & fi = f2 * f1 holds
A is_limes_of fi
proof end;

theorem Th15: :: ORDINAL4:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for phi being Ordinal-Sequence
for A being Ordinal st phi is increasing holds
phi | A is increasing
proof end;

theorem Th16: :: ORDINAL4:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for phi being Ordinal-Sequence st phi is increasing & dom phi is_limit_ordinal holds
sup phi is_limit_ordinal
proof end;

Lm2: for f, g being Function
for X being set st rng f c= X holds
(g | X) * f = g * f
proof end;

theorem :: ORDINAL4:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fi, psi, phi being Ordinal-Sequence st fi is increasing & fi is continuous & psi is continuous & phi = psi * fi holds
phi is continuous
proof end;

theorem :: ORDINAL4:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fi being Ordinal-Sequence
for C being Ordinal st ( for A being Ordinal st A in dom fi holds
fi . A = C +^ A ) holds
fi is increasing
proof end;

theorem Th19: :: ORDINAL4:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fi being Ordinal-Sequence
for C being Ordinal st C <> {} & ( for A being Ordinal st A in dom fi holds
fi . A = A *^ C ) holds
fi is increasing
proof end;

theorem Th20: :: ORDINAL4:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal st A <> {} holds
exp {} ,A = {}
proof end;

Lm3: for A being Ordinal st A <> {} & A is_limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp {} ,B ) holds
{} is_limes_of fi
proof end;

Lm4: for A being Ordinal st A <> {} & A is_limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp one ,B ) holds
one is_limes_of fi
proof end;

Lm5: for C, A being Ordinal st A <> {} & A is_limit_ordinal holds
ex fi being Ordinal-Sequence st
( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp C,B ) & ex D being Ordinal st D is_limes_of fi )
proof end;

theorem Th21: :: ORDINAL4:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, C being Ordinal st A <> {} & A is_limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp C,B ) holds
exp C,A is_limes_of fi
proof end;

theorem Th22: :: ORDINAL4:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, A being Ordinal st C <> {} holds
exp C,A <> {}
proof end;

theorem Th23: :: ORDINAL4:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, A being Ordinal st one in C holds
exp C,A in exp C,(succ A)
proof end;

theorem Th24: :: ORDINAL4:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, A, B being Ordinal st one in C & A in B holds
exp C,A in exp C,B
proof end;

theorem Th25: :: ORDINAL4:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fi being Ordinal-Sequence
for C being Ordinal st one in C & ( for A being Ordinal st A in dom fi holds
fi . A = exp C,A ) holds
fi is increasing
proof end;

theorem :: ORDINAL4:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, A being Ordinal st one in C & A <> {} & A is_limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp C,B ) holds
exp C,A = sup fi
proof end;

theorem :: ORDINAL4:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, A, B being Ordinal st C <> {} & A c= B holds
exp C,A c= exp C,B
proof end;

theorem :: ORDINAL4:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Ordinal st A c= B holds
exp A,C c= exp B,C
proof end;

theorem :: ORDINAL4:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, A being Ordinal st one in C & A <> {} holds
one in exp C,A
proof end;

theorem Th30: :: ORDINAL4:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, A, B being Ordinal holds exp C,(A +^ B) = (exp C,B) *^ (exp C,A)
proof end;

theorem :: ORDINAL4:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, A, B being Ordinal holds exp (exp C,A),B = exp C,(B *^ A)
proof end;

theorem :: ORDINAL4:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, A being Ordinal st one in C holds
A c= exp C,A
proof end;

scheme :: ORDINAL4:sch 1
CriticalNumber{ F1( Ordinal) -> Ordinal } :
ex A being Ordinal st F1(A) = A
provided
A1: for A, B being Ordinal st A in B holds
F1(A) in F1(B) and
A2: for fi being Ordinal-Sequence
for A being Ordinal st A <> {} & A is_limit_ordinal holds
for phi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
phi . B = F1(B) ) holds
F1(A) is_limes_of phi
proof end;

definition
let W be Universe;
mode Ordinal of W -> Ordinal means :Def2: :: ORDINAL4:def 2
it in W;
existence
ex b1 being Ordinal st b1 in W
proof end;
mode Ordinal-Sequence of W -> Ordinal-Sequence means :Def3: :: ORDINAL4:def 3
( dom it = On W & rng it c= On W );
existence
ex b1 being Ordinal-Sequence st
( dom b1 = On W & rng b1 c= On W )
proof end;
end;

:: deftheorem Def2 defines Ordinal ORDINAL4:def 2 :
for W being Universe
for b2 being Ordinal holds
( b2 is Ordinal of W iff b2 in W );

:: deftheorem Def3 defines Ordinal-Sequence ORDINAL4:def 3 :
for W being Universe
for b2 being Ordinal-Sequence holds
( b2 is Ordinal-Sequence of W iff ( dom b2 = On W & rng b2 c= On W ) );

registration
let W be Universe;
cluster non empty Ordinal of W;
existence
not for b1 being Ordinal of W holds b1 is empty
proof end;
end;

scheme :: ORDINAL4:sch 2
UOSLambda{ F1() -> Universe, F2( set ) -> Ordinal of F1() } :
ex phi being Ordinal-Sequence of F1() st
for a being Ordinal of F1() holds phi . a = F2(a)
proof end;

definition
let W be Universe;
func 0-element_of W -> Ordinal of W equals :: ORDINAL4:def 4
{} ;
correctness
coherence
{} is Ordinal of W
;
proof end;
func 1-element_of W -> non empty Ordinal of W equals :: ORDINAL4:def 5
one ;
correctness
coherence
one is non empty Ordinal of W
;
proof end;
let phi be Ordinal-Sequence of W;
let A1 be Ordinal of W;
:: original: .
redefine func phi . A1 -> Ordinal of W;
coherence
phi . A1 is Ordinal of W
proof end;
end;

:: deftheorem defines 0-element_of ORDINAL4:def 4 :
for W being Universe holds 0-element_of W = {} ;

:: deftheorem defines 1-element_of ORDINAL4:def 5 :
for W being Universe holds 1-element_of W = one ;

definition
let W be Universe;
let p2, p1 be Ordinal-Sequence of W;
:: original: *
redefine func p1 * p2 -> Ordinal-Sequence of W;
coherence
p2 * p1 is Ordinal-Sequence of W
proof end;
end;

theorem :: ORDINAL4:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ORDINAL4:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ORDINAL4:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Universe holds
( 0-element_of W = {} & 1-element_of W = one ) ;

definition
let W be Universe;
let A1 be Ordinal of W;
:: original: succ
redefine func succ A1 -> non empty Ordinal of W;
coherence
succ A1 is non empty Ordinal of W
proof end;
let B1 be Ordinal of W;
:: original: +^
redefine func A1 +^ B1 -> Ordinal of W;
coherence
A1 +^ B1 is Ordinal of W
proof end;
end;

definition
let W be Universe;
let A1, B1 be Ordinal of W;
:: original: *^
redefine func A1 *^ B1 -> Ordinal of W;
coherence
A1 *^ B1 is Ordinal of W
proof end;
end;

theorem Th36: :: ORDINAL4:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Universe
for A1 being Ordinal of W
for phi being Ordinal-Sequence of W holds A1 in dom phi
proof end;

theorem Th37: :: ORDINAL4:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fi being Ordinal-Sequence
for W being Universe st dom fi in W & rng fi c= W holds
sup fi in W
proof end;

theorem :: ORDINAL4:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Universe
for phi being Ordinal-Sequence of W st phi is increasing & phi is continuous & omega in W holds
ex A being Ordinal st
( A in dom phi & phi . A = A )
proof end;