:: ORDINAL2 semantic presentation
begin
scheme :: ORDINAL2:sch 1
OrdinalInd{ P1[ Ordinal] } :
for A being Ordinal holds P1[A]
provided
A1: P1[ {} ] and
A2: for A being Ordinal st P1[A] holds
P1[ succ A] and
A3: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
P1[B] ) holds
P1[A]
proof
A4: for A being Ordinal st ( for B being Ordinal st B in A holds
P1[B] ) holds
P1[A]
proof
let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds
P1[B] ) implies P1[A] )
assume A5: for B being Ordinal st B in A holds
P1[B] ; ::_thesis: P1[A]
A6: now__::_thesis:_(_A_<>_{}_&_(_for_B_being_Ordinal_holds_A_<>_succ_B_)_implies_P1[A]_)
assume that
A7: A <> {} and
A8: for B being Ordinal holds A <> succ B ; ::_thesis: P1[A]
A is limit_ordinal by A8, ORDINAL1:29;
hence P1[A] by A3, A5, A7; ::_thesis: verum
end;
now__::_thesis:_(_ex_B_being_Ordinal_st_A_=_succ_B_implies_P1[A]_)
given B being Ordinal such that A9: A = succ B ; ::_thesis: P1[A]
B in A by A9, ORDINAL1:6;
hence P1[A] by A2, A5, A9; ::_thesis: verum
end;
hence P1[A] by A1, A6; ::_thesis: verum
end;
thus for A being Ordinal holds P1[A] from ORDINAL1:sch_2(A4); ::_thesis: verum
end;
theorem Th1: :: ORDINAL2:1
for A, B being Ordinal holds
( A c= B iff succ A c= succ B )
proof
let A, B be Ordinal; ::_thesis: ( A c= B iff succ A c= succ B )
( A c= B iff A in succ B ) by ORDINAL1:22;
hence ( A c= B iff succ A c= succ B ) by ORDINAL1:21; ::_thesis: verum
end;
theorem Th2: :: ORDINAL2:2
for A being Ordinal holds union (succ A) = A
proof
let A be Ordinal; ::_thesis: union (succ A) = A
thus union (succ A) c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= union (succ A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (succ A) or x in A )
assume x in union (succ A) ; ::_thesis: x in A
then consider X being set such that
A1: x in X and
A2: X in succ A by TARSKI:def_4;
reconsider X = X as Ordinal by A2;
X c= A by A2, ORDINAL1:22;
hence x in A by A1; ::_thesis: verum
end;
thus A c= union (succ A) by ORDINAL1:6, ZFMISC_1:74; ::_thesis: verum
end;
theorem :: ORDINAL2:3
for A being Ordinal holds succ A c= bool A
proof
let A be Ordinal; ::_thesis: succ A c= bool A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in succ A or x in bool A )
assume A1: x in succ A ; ::_thesis: x in bool A
then reconsider B = x as Ordinal ;
( x in A or x = A ) by A1, ORDINAL1:8;
then B c= A by ORDINAL1:def_2;
hence x in bool A ; ::_thesis: verum
end;
theorem :: ORDINAL2:4
{} is limit_ordinal
proof
thus {} = union {} by ZFMISC_1:2; :: according to ORDINAL1:def_6 ::_thesis: verum
end;
theorem Th5: :: ORDINAL2:5
for A being Ordinal holds union A c= A
proof
let A be Ordinal; ::_thesis: union A c= A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union A or x in A )
assume x in union A ; ::_thesis: x in A
then consider Y being set such that
A1: x in Y and
A2: Y in A by TARSKI:def_4;
Y c= A by A2, ORDINAL1:def_2;
hence x in A by A1; ::_thesis: verum
end;
definition
let L be T-Sequence;
func last L -> set equals :: ORDINAL2:def 1
L . (union (dom L));
coherence
L . (union (dom L)) is set ;
end;
:: deftheorem defines last ORDINAL2:def_1_:_
for L being T-Sequence holds last L = L . (union (dom L));
theorem :: ORDINAL2:6
for A being Ordinal
for L being T-Sequence st dom L = succ A holds
last L = L . A by Th2;
theorem :: ORDINAL2:7
for X being set holds On X c= X
proof
let X be set ; ::_thesis: On X c= X
thus for x being set st x in On X holds
x in X by ORDINAL1:def_9; :: according to TARSKI:def_3 ::_thesis: verum
end;
theorem Th8: :: ORDINAL2:8
for A being Ordinal holds On A = A
proof
let A be Ordinal; ::_thesis: On A = A
for x being set holds
( x in A iff ( x in A & x is Ordinal ) ) ;
hence On A = A by ORDINAL1:def_9; ::_thesis: verum
end;
theorem Th9: :: ORDINAL2:9
for X, Y being set st X c= Y holds
On X c= On Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies On X c= On Y )
assume A1: X c= Y ; ::_thesis: On X c= On Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in On X or x in On Y )
assume x in On X ; ::_thesis: x in On Y
then ( x in X & x is Ordinal ) by ORDINAL1:def_9;
hence x in On Y by A1, ORDINAL1:def_9; ::_thesis: verum
end;
theorem :: ORDINAL2:10
for X being set holds Lim X c= X
proof
let X be set ; ::_thesis: Lim X c= X
thus for x being set st x in Lim X holds
x in X by ORDINAL1:def_10; :: according to TARSKI:def_3 ::_thesis: verum
end;
theorem :: ORDINAL2:11
for X, Y being set st X c= Y holds
Lim X c= Lim Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies Lim X c= Lim Y )
assume A1: X c= Y ; ::_thesis: Lim X c= Lim Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim X or x in Lim Y )
assume x in Lim X ; ::_thesis: x in Lim Y
then ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) by ORDINAL1:def_10;
hence x in Lim Y by A1, ORDINAL1:def_10; ::_thesis: verum
end;
theorem :: ORDINAL2:12
for X being set holds Lim X c= On X
proof
let X be set ; ::_thesis: Lim X c= On X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim X or x in On X )
assume x in Lim X ; ::_thesis: x in On X
then ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) by ORDINAL1:def_10;
hence x in On X by ORDINAL1:def_9; ::_thesis: verum
end;
theorem Th13: :: ORDINAL2:13
for X being set st ( for x being set st x in X holds
x is Ordinal ) holds
meet X is Ordinal
proof
let X be set ; ::_thesis: ( ( for x being set st x in X holds
x is Ordinal ) implies meet X is Ordinal )
assume A1: for x being set st x in X holds
x is Ordinal ; ::_thesis: meet X is Ordinal
now__::_thesis:_(_X_<>_{}_implies_meet_X_is_Ordinal_)
defpred S1[ Ordinal] means $1 in X;
set x = the Element of X;
assume A2: X <> {} ; ::_thesis: meet X is Ordinal
then the Element of X is Ordinal by A1;
then A3: ex A being Ordinal st S1[A] by A2;
consider A being Ordinal such that
A4: ( S1[A] & ( for B being Ordinal st S1[B] holds
A c= B ) ) from ORDINAL1:sch_1(A3);
for x being set holds
( x in A iff for Y being set st Y in X holds
x in Y )
proof
let x be set ; ::_thesis: ( x in A iff for Y being set st Y in X holds
x in Y )
thus ( x in A implies for Y being set st Y in X holds
x in Y ) ::_thesis: ( ( for Y being set st Y in X holds
x in Y ) implies x in A )
proof
assume A5: x in A ; ::_thesis: for Y being set st Y in X holds
x in Y
let Y be set ; ::_thesis: ( Y in X implies x in Y )
assume A6: Y in X ; ::_thesis: x in Y
then reconsider B = Y as Ordinal by A1;
A c= B by A4, A6;
hence x in Y by A5; ::_thesis: verum
end;
assume for Y being set st Y in X holds
x in Y ; ::_thesis: x in A
hence x in A by A4; ::_thesis: verum
end;
hence meet X is Ordinal by A2, SETFAM_1:def_1; ::_thesis: verum
end;
hence meet X is Ordinal by SETFAM_1:def_1; ::_thesis: verum
end;
registration
cluster epsilon-transitive epsilon-connected ordinal limit_ordinal for set ;
existence
ex b1 being Ordinal st b1 is limit_ordinal
proof
take omega ; ::_thesis: omega is limit_ordinal
thus omega is limit_ordinal by ORDINAL1:def_11; ::_thesis: verum
end;
end;
definition
let X be set ;
func inf X -> Ordinal equals :: ORDINAL2:def 2
meet (On X);
coherence
meet (On X) is Ordinal
proof
for x being set st x in On X holds
x is Ordinal by ORDINAL1:def_9;
hence meet (On X) is Ordinal by Th13; ::_thesis: verum
end;
func sup X -> Ordinal means :Def3: :: ORDINAL2:def 3
( On X c= it & ( for A being Ordinal st On X c= A holds
it c= A ) );
existence
ex b1 being Ordinal st
( On X c= b1 & ( for A being Ordinal st On X c= A holds
b1 c= A ) )
proof
defpred S1[ Ordinal] means On X c= $1;
for x being set st x in On X holds
x is Ordinal by ORDINAL1:def_9;
then reconsider A = union (On X) as Ordinal by ORDINAL1:23;
On X c= succ A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in On X or x in succ A )
assume A1: x in On X ; ::_thesis: x in succ A
then reconsider B = x as Ordinal by ORDINAL1:def_9;
B c= A by A1, ZFMISC_1:74;
hence x in succ A by ORDINAL1:22; ::_thesis: verum
end;
then A2: ex A being Ordinal st S1[A] ;
thus ex F being Ordinal st
( S1[F] & ( for A being Ordinal st S1[A] holds
F c= A ) ) from ORDINAL1:sch_1(A2); ::_thesis: verum
end;
uniqueness
for b1, b2 being Ordinal st On X c= b1 & ( for A being Ordinal st On X c= A holds
b1 c= A ) & On X c= b2 & ( for A being Ordinal st On X c= A holds
b2 c= A ) holds
b1 = b2
proof
let B, C be Ordinal; ::_thesis: ( On X c= B & ( for A being Ordinal st On X c= A holds
B c= A ) & On X c= C & ( for A being Ordinal st On X c= A holds
C c= A ) implies B = C )
assume ( On X c= B & ( for A being Ordinal st On X c= A holds
B c= A ) & On X c= C & ( for A being Ordinal st On X c= A holds
C c= A ) ) ; ::_thesis: B = C
hence ( B c= C & C c= B ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
end;
:: deftheorem defines inf ORDINAL2:def_2_:_
for X being set holds inf X = meet (On X);
:: deftheorem Def3 defines sup ORDINAL2:def_3_:_
for X being set
for b2 being Ordinal holds
( b2 = sup X iff ( On X c= b2 & ( for A being Ordinal st On X c= A holds
b2 c= A ) ) );
theorem :: ORDINAL2:14
for A being Ordinal
for X being set st A in X holds
inf X c= A
proof
let A be Ordinal; ::_thesis: for X being set st A in X holds
inf X c= A
let X be set ; ::_thesis: ( A in X implies inf X c= A )
assume A in X ; ::_thesis: inf X c= A
then A in On X by ORDINAL1:def_9;
hence inf X c= A by SETFAM_1:3; ::_thesis: verum
end;
theorem :: ORDINAL2:15
for D being Ordinal
for X being set st On X <> {} & ( for A being Ordinal st A in X holds
D c= A ) holds
D c= inf X
proof
let D be Ordinal; ::_thesis: for X being set st On X <> {} & ( for A being Ordinal st A in X holds
D c= A ) holds
D c= inf X
let X be set ; ::_thesis: ( On X <> {} & ( for A being Ordinal st A in X holds
D c= A ) implies D c= inf X )
assume that
A1: On X <> {} and
A2: for A being Ordinal st A in X holds
D c= A ; ::_thesis: D c= inf X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in inf X )
assume A3: x in D ; ::_thesis: x in inf X
for Y being set st Y in On X holds
x in Y
proof
let Y be set ; ::_thesis: ( Y in On X implies x in Y )
assume A4: Y in On X ; ::_thesis: x in Y
then reconsider A = Y as Ordinal by ORDINAL1:def_9;
A in X by A4, ORDINAL1:def_9;
then D c= A by A2;
hence x in Y by A3; ::_thesis: verum
end;
hence x in inf X by A1, SETFAM_1:def_1; ::_thesis: verum
end;
theorem :: ORDINAL2:16
for A being Ordinal
for X, Y being set st A in X & X c= Y holds
inf Y c= inf X
proof
let A be Ordinal; ::_thesis: for X, Y being set st A in X & X c= Y holds
inf Y c= inf X
let X, Y be set ; ::_thesis: ( A in X & X c= Y implies inf Y c= inf X )
assume A in X ; ::_thesis: ( not X c= Y or inf Y c= inf X )
then A1: On X <> {} by ORDINAL1:def_9;
assume X c= Y ; ::_thesis: inf Y c= inf X
then On X c= On Y by Th9;
hence inf Y c= inf X by A1, SETFAM_1:6; ::_thesis: verum
end;
theorem :: ORDINAL2:17
for A being Ordinal
for X being set st A in X holds
inf X in X
proof
let A be Ordinal; ::_thesis: for X being set st A in X holds
inf X in X
let X be set ; ::_thesis: ( A in X implies inf X in X )
defpred S1[ Ordinal] means $1 in X;
assume A in X ; ::_thesis: inf X in X
then A1: ex A being Ordinal st S1[A] ;
consider A being Ordinal such that
A2: ( S1[A] & ( for B being Ordinal st S1[B] holds
A c= B ) ) from ORDINAL1:sch_1(A1);
A3: A in On X by A2, ORDINAL1:def_9;
A4: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_A_implies_for_Y_being_set_st_Y_in_On_X_holds_
x_in_Y_)_&_(_(_for_Y_being_set_st_Y_in_On_X_holds_
x_in_Y_)_implies_x_in_A_)_)
let x be set ; ::_thesis: ( ( x in A implies for Y being set st Y in On X holds
x in Y ) & ( ( for Y being set st Y in On X holds
x in Y ) implies x in A ) )
thus ( x in A implies for Y being set st Y in On X holds
x in Y ) ::_thesis: ( ( for Y being set st Y in On X holds
x in Y ) implies x in A )
proof
assume A5: x in A ; ::_thesis: for Y being set st Y in On X holds
x in Y
let Y be set ; ::_thesis: ( Y in On X implies x in Y )
assume A6: Y in On X ; ::_thesis: x in Y
then reconsider B = Y as Ordinal by ORDINAL1:def_9;
Y in X by A6, ORDINAL1:def_9;
then A c= B by A2;
hence x in Y by A5; ::_thesis: verum
end;
assume for Y being set st Y in On X holds
x in Y ; ::_thesis: x in A
hence x in A by A3; ::_thesis: verum
end;
On X <> {} by A2, ORDINAL1:def_9;
hence inf X in X by A2, A4, SETFAM_1:def_1; ::_thesis: verum
end;
theorem Th18: :: ORDINAL2:18
for A being Ordinal holds sup A = A
proof
let A be Ordinal; ::_thesis: sup A = A
( On A = A & ( for B being Ordinal st On A c= B holds
A c= B ) ) by Th8;
hence sup A = A by Def3; ::_thesis: verum
end;
theorem Th19: :: ORDINAL2:19
for A being Ordinal
for X being set st A in X holds
A in sup X
proof
let A be Ordinal; ::_thesis: for X being set st A in X holds
A in sup X
let X be set ; ::_thesis: ( A in X implies A in sup X )
assume A in X ; ::_thesis: A in sup X
then A1: A in On X by ORDINAL1:def_9;
On X c= sup X by Def3;
hence A in sup X by A1; ::_thesis: verum
end;
theorem Th20: :: ORDINAL2:20
for D being Ordinal
for X being set st ( for A being Ordinal st A in X holds
A in D ) holds
sup X c= D
proof
let D be Ordinal; ::_thesis: for X being set st ( for A being Ordinal st A in X holds
A in D ) holds
sup X c= D
let X be set ; ::_thesis: ( ( for A being Ordinal st A in X holds
A in D ) implies sup X c= D )
assume A1: for A being Ordinal st A in X holds
A in D ; ::_thesis: sup X c= D
On X c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in On X or x in D )
assume A2: x in On X ; ::_thesis: x in D
then reconsider A = x as Ordinal by ORDINAL1:def_9;
A in X by A2, ORDINAL1:def_9;
hence x in D by A1; ::_thesis: verum
end;
hence sup X c= D by Def3; ::_thesis: verum
end;
theorem :: ORDINAL2:21
for A being Ordinal
for X being set st A in sup X holds
ex B being Ordinal st
( B in X & A c= B )
proof
let A be Ordinal; ::_thesis: for X being set st A in sup X holds
ex B being Ordinal st
( B in X & A c= B )
let X be set ; ::_thesis: ( A in sup X implies ex B being Ordinal st
( B in X & A c= B ) )
assume that
A1: A in sup X and
A2: for B being Ordinal st B in X holds
not A c= B ; ::_thesis: contradiction
for B being Ordinal st B in X holds
B in A by A2, ORDINAL1:16;
then sup X c= A by Th20;
hence contradiction by A1, ORDINAL1:5; ::_thesis: verum
end;
theorem :: ORDINAL2:22
for X, Y being set st X c= Y holds
sup X c= sup Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies sup X c= sup Y )
assume X c= Y ; ::_thesis: sup X c= sup Y
then A1: On X c= On Y by Th9;
On Y c= sup Y by Def3;
then On X c= sup Y by A1, XBOOLE_1:1;
hence sup X c= sup Y by Def3; ::_thesis: verum
end;
theorem :: ORDINAL2:23
for A being Ordinal holds sup {A} = succ A
proof
let A be Ordinal; ::_thesis: sup {A} = succ A
A1: On {A} c= succ A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in On {A} or x in succ A )
assume x in On {A} ; ::_thesis: x in succ A
then x in {A} by ORDINAL1:def_9;
then x = A by TARSKI:def_1;
hence x in succ A by ORDINAL1:6; ::_thesis: verum
end;
now__::_thesis:_for_B_being_Ordinal_st_On_{A}_c=_B_holds_
succ_A_c=_B
A in {A} by TARSKI:def_1;
then A2: A in On {A} by ORDINAL1:def_9;
let B be Ordinal; ::_thesis: ( On {A} c= B implies succ A c= B )
assume On {A} c= B ; ::_thesis: succ A c= B
hence succ A c= B by A2, ORDINAL1:21; ::_thesis: verum
end;
hence sup {A} = succ A by A1, Def3; ::_thesis: verum
end;
theorem :: ORDINAL2:24
for X being set holds inf X c= sup X
proof
let X be set ; ::_thesis: inf X c= sup X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in inf X or x in sup X )
set y = the Element of On X;
assume A1: x in inf X ; ::_thesis: x in sup X
then reconsider y = the Element of On X as Ordinal by ORDINAL1:def_9, SETFAM_1:1;
On X c= sup X by Def3;
then y in sup X by A1, SETFAM_1:1, TARSKI:def_3;
then A2: y c= sup X by ORDINAL1:def_2;
x in y by A1, SETFAM_1:1, SETFAM_1:def_1;
hence x in sup X by A2; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 2
TSLambda{ F1() -> Ordinal, F2( Ordinal) -> set } :
ex L being T-Sequence st
( dom L = F1() & ( for A being Ordinal st A in F1() holds
L . A = F2(A) ) )
proof
deffunc H1( set ) -> set = F2((sup (union {$1})));
consider f being Function such that
A1: ( dom f = F1() & ( for x being set st x in F1() holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
reconsider f = f as T-Sequence by A1, ORDINAL1:def_7;
take L = f; ::_thesis: ( dom L = F1() & ( for A being Ordinal st A in F1() holds
L . A = F2(A) ) )
thus dom L = F1() by A1; ::_thesis: for A being Ordinal st A in F1() holds
L . A = F2(A)
let A be Ordinal; ::_thesis: ( A in F1() implies L . A = F2(A) )
assume A in F1() ; ::_thesis: L . A = F2(A)
hence L . A = F2((sup (union {A}))) by A1
.= F2((sup A)) by ZFMISC_1:25
.= F2(A) by Th18 ;
::_thesis: verum
end;
definition
let f be Function;
attrf is Ordinal-yielding means :Def4: :: ORDINAL2:def 4
ex A being Ordinal st rng f c= A;
end;
:: deftheorem Def4 defines Ordinal-yielding ORDINAL2:def_4_:_
for f being Function holds
( f is Ordinal-yielding iff ex A being Ordinal st rng f c= A );
registration
cluster T-Sequence-like Relation-like Function-like Ordinal-yielding for set ;
existence
ex b1 being T-Sequence st b1 is Ordinal-yielding
proof
set A = the Ordinal;
set L = the T-Sequence of ;
take the T-Sequence of ; ::_thesis: the T-Sequence of is Ordinal-yielding
take the Ordinal ; :: according to ORDINAL2:def_4 ::_thesis: rng the T-Sequence of c= the Ordinal
thus rng the T-Sequence of c= the Ordinal by RELAT_1:def_19; ::_thesis: verum
end;
end;
definition
mode Ordinal-Sequence is Ordinal-yielding T-Sequence;
end;
registration
let A be Ordinal;
cluster T-Sequence-like Relation-like A -valued Function-like -> Ordinal-yielding for set ;
coherence
for b1 being T-Sequence of holds b1 is Ordinal-yielding
proof
let L be T-Sequence of ; ::_thesis: L is Ordinal-yielding
take A ; :: according to ORDINAL2:def_4 ::_thesis: rng L c= A
thus rng L c= A by RELAT_1:def_19; ::_thesis: verum
end;
end;
registration
let L be Ordinal-Sequence;
let A be Ordinal;
clusterL | A -> Ordinal-yielding ;
coherence
L | A is Ordinal-yielding
proof
consider B being Ordinal such that
A1: rng L c= B by Def4;
L | A is Ordinal-yielding
proof
take B ; :: according to ORDINAL2:def_4 ::_thesis: rng (L | A) c= B
rng (L | A) c= rng L by RELAT_1:70;
hence rng (L | A) c= B by A1, XBOOLE_1:1; ::_thesis: verum
end;
hence L | A is Ordinal-yielding ; ::_thesis: verum
end;
end;
theorem Th25: :: ORDINAL2:25
for A being Ordinal
for fi being Ordinal-Sequence st A in dom fi holds
fi . A is Ordinal
proof
let A be Ordinal; ::_thesis: for fi being Ordinal-Sequence st A in dom fi holds
fi . A is Ordinal
let fi be Ordinal-Sequence; ::_thesis: ( A in dom fi implies fi . A is Ordinal )
assume A in dom fi ; ::_thesis: fi . A is Ordinal
then A1: fi . A in rng fi by FUNCT_1:def_3;
ex B being Ordinal st rng fi c= B by Def4;
hence fi . A is Ordinal by A1; ::_thesis: verum
end;
registration
let f be Ordinal-Sequence;
let a be Ordinal;
clusterf . a -> ordinal ;
coherence
f . a is ordinal
proof
( a in dom f or not a in dom f ) ;
hence f . a is ordinal by Th25, FUNCT_1:def_2; ::_thesis: verum
end;
end;
scheme :: ORDINAL2:sch 3
OSLambda{ F1() -> Ordinal, F2( Ordinal) -> Ordinal } :
ex fi being Ordinal-Sequence st
( dom fi = F1() & ( for A being Ordinal st A in F1() holds
fi . A = F2(A) ) )
proof
consider L being T-Sequence such that
A1: ( dom L = F1() & ( for A being Ordinal st A in F1() holds
L . A = F2(A) ) ) from ORDINAL2:sch_2();
L is Ordinal-yielding
proof
take sup (rng L) ; :: according to ORDINAL2:def_4 ::_thesis: rng L c= sup (rng L)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng L or x in sup (rng L) )
assume A2: x in rng L ; ::_thesis: x in sup (rng L)
then consider y being set such that
A3: y in dom L and
A4: x = L . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A3;
L . y = F2(y) by A1, A3;
then A5: x in On (rng L) by A2, A4, ORDINAL1:def_9;
On (rng L) c= sup (rng L) by Def3;
hence x in sup (rng L) by A5; ::_thesis: verum
end;
then reconsider L = L as Ordinal-Sequence ;
take fi = L; ::_thesis: ( dom fi = F1() & ( for A being Ordinal st A in F1() holds
fi . A = F2(A) ) )
thus dom fi = F1() by A1; ::_thesis: for A being Ordinal st A in F1() holds
fi . A = F2(A)
let A be Ordinal; ::_thesis: ( A in F1() implies fi . A = F2(A) )
assume A in F1() ; ::_thesis: fi . A = F2(A)
hence fi . A = F2(A) by A1; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 4
TSUniq1{ F1() -> Ordinal, F2() -> set , F3( Ordinal, set ) -> set , F4( Ordinal, T-Sequence) -> set , F5() -> T-Sequence, F6() -> T-Sequence } :
F5() = F6()
provided
A1: dom F5() = F1() and
A2: ( {} in F1() implies F5() . {} = F2() ) and
A3: for A being Ordinal st succ A in F1() holds
F5() . (succ A) = F3(A,(F5() . A)) and
A4: for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
F5() . A = F4(A,(F5() | A)) and
A5: dom F6() = F1() and
A6: ( {} in F1() implies F6() . {} = F2() ) and
A7: for A being Ordinal st succ A in F1() holds
F6() . (succ A) = F3(A,(F6() . A)) and
A8: for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
F6() . A = F4(A,(F6() | A))
proof
defpred S1[ set ] means F5() . $1 <> F6() . $1;
consider X being set such that
A9: for Y being set holds
( Y in X iff ( Y in F1() & S1[Y] ) ) from XBOOLE_0:sch_1();
for b being set st b in X holds
b in F1() by A9;
then A10: X c= F1() by TARSKI:def_3;
assume F5() <> F6() ; ::_thesis: contradiction
then ex a being set st
( a in F1() & F5() . a <> F6() . a ) by A1, A5, FUNCT_1:2;
then X <> {} by A9;
then consider B being Ordinal such that
A11: B in X and
A12: for C being Ordinal st C in X holds
B c= C by A10, ORDINAL1:20;
A13: B in F1() by A9, A11;
then A14: B c= F1() by ORDINAL1:def_2;
then A15: ( dom (F5() | B) = B & dom (F6() | B) = B ) by A1, A5, RELAT_1:62;
A16: now__::_thesis:_for_C_being_Ordinal_st_C_in_B_holds_
F5()_._C_=_F6()_._C
let C be Ordinal; ::_thesis: ( C in B implies F5() . C = F6() . C )
assume A17: C in B ; ::_thesis: F5() . C = F6() . C
then not C in X by A12, ORDINAL1:5;
hence F5() . C = F6() . C by A9, A14, A17; ::_thesis: verum
end;
A18: now__::_thesis:_for_a_being_set_st_a_in_B_holds_
(F5()_|_B)_._a_=_(F6()_|_B)_._a
let a be set ; ::_thesis: ( a in B implies (F5() | B) . a = (F6() | B) . a )
assume A19: a in B ; ::_thesis: (F5() | B) . a = (F6() | B) . a
( (F5() | B) . a = F5() . a & (F6() | B) . a = F6() . a ) by A15, A19, FUNCT_1:47;
hence (F5() | B) . a = (F6() | B) . a by A16, A19; ::_thesis: verum
end;
A20: now__::_thesis:_(_ex_C_being_Ordinal_st_B_=_succ_C_implies_F5()_._B_=_F6()_._B_)
given C being Ordinal such that A21: B = succ C ; ::_thesis: F5() . B = F6() . B
A22: ( F5() . C = (F5() | B) . C & F6() . C = (F6() | B) . C ) by A21, FUNCT_1:49, ORDINAL1:6;
( F5() . B = F3(C,(F5() . C)) & F6() . B = F3(C,(F6() . C)) ) by A3, A7, A13, A21;
hence F5() . B = F6() . B by A18, A21, A22, ORDINAL1:6; ::_thesis: verum
end;
now__::_thesis:_(_B_<>_{}_&_(_for_C_being_Ordinal_holds_B_<>_succ_C_)_implies_F5()_._B_=_F6()_._B_)
assume that
A23: B <> {} and
A24: for C being Ordinal holds B <> succ C ; ::_thesis: F5() . B = F6() . B
B is limit_ordinal by A24, ORDINAL1:29;
then ( F5() . B = F4(B,(F5() | B)) & F6() . B = F4(B,(F6() | B)) ) by A4, A8, A13, A23;
hence F5() . B = F6() . B by A15, A18, FUNCT_1:2; ::_thesis: verum
end;
hence contradiction by A2, A6, A9, A11, A20; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 5
TSExist1{ F1() -> Ordinal, F2() -> set , F3( Ordinal, set ) -> set , F4( Ordinal, T-Sequence) -> set } :
ex L being T-Sequence st
( dom L = F1() & ( {} in F1() implies L . {} = F2() ) & ( for A being Ordinal st succ A in F1() holds
L . (succ A) = F3(A,(L . A)) ) & ( for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A)) ) )
proof
defpred S1[ Ordinal, T-Sequence] means ( dom $2 = $1 & ( {} in $1 implies $2 . {} = F2() ) & ( for A being Ordinal st succ A in $1 holds
$2 . (succ A) = F3(A,($2 . A)) ) & ( for A being Ordinal st A in $1 & A <> {} & A is limit_ordinal holds
$2 . A = F4(A,($2 | A)) ) );
defpred S2[ Ordinal] means ex L being T-Sequence st S1[$1,L];
A1: for B being Ordinal st ( for C being Ordinal st C in B holds
S2[C] ) holds
S2[B]
proof
defpred S3[ set , set ] means ( $1 is Ordinal & $2 is T-Sequence & ( for A being Ordinal
for L being T-Sequence st A = $1 & L = $2 holds
S1[A,L] ) );
let B be Ordinal; ::_thesis: ( ( for C being Ordinal st C in B holds
S2[C] ) implies S2[B] )
assume A2: for C being Ordinal st C in B holds
ex L being T-Sequence st S1[C,L] ; ::_thesis: S2[B]
A3: for a, b, c being set st S3[a,b] & S3[a,c] holds
b = c
proof
let a, b, c be set ; ::_thesis: ( S3[a,b] & S3[a,c] implies b = c )
assume that
A4: a is Ordinal and
A5: b is T-Sequence and
A6: for A being Ordinal
for L being T-Sequence st A = a & L = b holds
S1[A,L] and
a is Ordinal and
A7: c is T-Sequence and
A8: for A being Ordinal
for L being T-Sequence st A = a & L = c holds
S1[A,L] ; ::_thesis: b = c
reconsider a = a as Ordinal by A4;
reconsider c = c as T-Sequence by A7;
A9: dom c = a by A8;
A10: for A being Ordinal st A in a & A <> {} & A is limit_ordinal holds
c . A = F4(A,(c | A)) by A8;
A11: for A being Ordinal st succ A in a holds
c . (succ A) = F3(A,(c . A)) by A8;
A12: ( {} in a implies c . {} = F2() ) by A8;
reconsider b = b as T-Sequence by A5;
A13: ( {} in a implies b . {} = F2() ) by A6;
A14: for A being Ordinal st succ A in a holds
b . (succ A) = F3(A,(b . A)) by A6;
A15: for A being Ordinal st A in a & A <> {} & A is limit_ordinal holds
b . A = F4(A,(b | A)) by A6;
A16: dom b = a by A6;
b = c from ORDINAL2:sch_4(A16, A13, A14, A15, A9, A12, A11, A10);
hence b = c ; ::_thesis: verum
end;
consider G being Function such that
A17: for a, b being set holds
( [a,b] in G iff ( a in B & S3[a,b] ) ) from FUNCT_1:sch_1(A3);
defpred S4[ set , set ] means ex A being Ordinal ex L being T-Sequence st
( A = $1 & L = G . $1 & ( ( A = {} & $2 = F2() ) or ex B being Ordinal st
( A = succ B & $2 = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & $2 = F4(A,L) ) ) );
A18: dom G = B
proof
thus for a being set st a in dom G holds
a in B :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: B c= dom G
proof
let a be set ; ::_thesis: ( a in dom G implies a in B )
assume a in dom G ; ::_thesis: a in B
then ex b being set st [a,b] in G by XTUPLE_0:def_12;
hence a in B by A17; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B or a in dom G )
assume A19: a in B ; ::_thesis: a in dom G
then reconsider a9 = a as Ordinal ;
consider L being T-Sequence such that
A20: S1[a9,L] by A2, A19;
for A being Ordinal
for K being T-Sequence st A = a9 & K = L holds
S1[A,K] by A20;
then [a9,L] in G by A17, A19;
hence a in dom G by XTUPLE_0:def_12; ::_thesis: verum
end;
A21: for a being set st a in B holds
ex b being set st S4[a,b]
proof
let a be set ; ::_thesis: ( a in B implies ex b being set st S4[a,b] )
assume A22: a in B ; ::_thesis: ex b being set st S4[a,b]
then reconsider A = a as Ordinal ;
consider c being set such that
A23: [a,c] in G by A18, A22, XTUPLE_0:def_12;
reconsider L = c as T-Sequence by A17, A23;
A24: now__::_thesis:_(_ex_C_being_Ordinal_st_A_=_succ_C_implies_ex_b_being_set_st_S4[a,b]_)
given C being Ordinal such that A25: A = succ C ; ::_thesis: ex b being set st S4[a,b]
thus ex b being set st S4[a,b] ::_thesis: verum
proof
take F3(C,(L . C)) ; ::_thesis: S4[a,F3(C,(L . C))]
take A ; ::_thesis: ex L being T-Sequence st
( A = a & L = G . a & ( ( A = {} & F3(C,(L . C)) = F2() ) or ex B being Ordinal st
( A = succ B & F3(C,(L . C)) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F3(C,(L . C)) = F4(A,L) ) ) )
take L ; ::_thesis: ( A = a & L = G . a & ( ( A = {} & F3(C,(L . C)) = F2() ) or ex B being Ordinal st
( A = succ B & F3(C,(L . C)) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F3(C,(L . C)) = F4(A,L) ) ) )
thus ( A = a & L = G . a ) by A23, FUNCT_1:1; ::_thesis: ( ( A = {} & F3(C,(L . C)) = F2() ) or ex B being Ordinal st
( A = succ B & F3(C,(L . C)) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F3(C,(L . C)) = F4(A,L) ) )
thus ( ( A = {} & F3(C,(L . C)) = F2() ) or ex B being Ordinal st
( A = succ B & F3(C,(L . C)) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F3(C,(L . C)) = F4(A,L) ) ) by A25; ::_thesis: verum
end;
end;
A26: now__::_thesis:_(_A_<>_{}_&_(_for_C_being_Ordinal_holds_A_<>_succ_C_)_implies_S4[a,F4(A,L)]_)
assume A27: ( A <> {} & ( for C being Ordinal holds A <> succ C ) ) ; ::_thesis: S4[a,F4(A,L)]
thus S4[a,F4(A,L)] ::_thesis: verum
proof
take A ; ::_thesis: ex L being T-Sequence st
( A = a & L = G . a & ( ( A = {} & F4(A,L) = F2() ) or ex B being Ordinal st
( A = succ B & F4(A,L) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F4(A,L) = F4(A,L) ) ) )
take L ; ::_thesis: ( A = a & L = G . a & ( ( A = {} & F4(A,L) = F2() ) or ex B being Ordinal st
( A = succ B & F4(A,L) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F4(A,L) = F4(A,L) ) ) )
thus ( A = a & L = G . a ) by A23, FUNCT_1:1; ::_thesis: ( ( A = {} & F4(A,L) = F2() ) or ex B being Ordinal st
( A = succ B & F4(A,L) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F4(A,L) = F4(A,L) ) )
thus ( ( A = {} & F4(A,L) = F2() ) or ex B being Ordinal st
( A = succ B & F4(A,L) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F4(A,L) = F4(A,L) ) ) by A27, ORDINAL1:29; ::_thesis: verum
end;
end;
now__::_thesis:_(_A_=_{}_implies_S4[a,F2()]_)
assume A28: A = {} ; ::_thesis: S4[a,F2()]
thus S4[a,F2()] ::_thesis: verum
proof
take A ; ::_thesis: ex L being T-Sequence st
( A = a & L = G . a & ( ( A = {} & F2() = F2() ) or ex B being Ordinal st
( A = succ B & F2() = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F2() = F4(A,L) ) ) )
take L ; ::_thesis: ( A = a & L = G . a & ( ( A = {} & F2() = F2() ) or ex B being Ordinal st
( A = succ B & F2() = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F2() = F4(A,L) ) ) )
thus ( A = a & L = G . a ) by A23, FUNCT_1:1; ::_thesis: ( ( A = {} & F2() = F2() ) or ex B being Ordinal st
( A = succ B & F2() = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F2() = F4(A,L) ) )
thus ( ( A = {} & F2() = F2() ) or ex B being Ordinal st
( A = succ B & F2() = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F2() = F4(A,L) ) ) by A28; ::_thesis: verum
end;
end;
hence ex b being set st S4[a,b] by A24, A26; ::_thesis: verum
end;
A29: for a, b, c being set st a in B & S4[a,b] & S4[a,c] holds
b = c
proof
let a, b, c be set ; ::_thesis: ( a in B & S4[a,b] & S4[a,c] implies b = c )
assume a in B ; ::_thesis: ( not S4[a,b] or not S4[a,c] or b = c )
given Ab being Ordinal, Lb being T-Sequence such that A30: Ab = a and
A31: Lb = G . a and
A32: ( ( Ab = {} & b = F2() ) or ex B being Ordinal st
( Ab = succ B & b = F3(B,(Lb . B)) ) or ( Ab <> {} & Ab is limit_ordinal & b = F4(Ab,Lb) ) ) ; ::_thesis: ( not S4[a,c] or b = c )
given Ac being Ordinal, Lc being T-Sequence such that A33: Ac = a and
A34: Lc = G . a and
A35: ( ( Ac = {} & c = F2() ) or ex B being Ordinal st
( Ac = succ B & c = F3(B,(Lc . B)) ) or ( Ac <> {} & Ac is limit_ordinal & c = F4(Ac,Lc) ) ) ; ::_thesis: b = c
now__::_thesis:_(_ex_C_being_Ordinal_st_Ab_=_succ_C_implies_b_=_c_)
given C being Ordinal such that A36: Ab = succ C ; ::_thesis: b = c
consider A being Ordinal such that
A37: Ab = succ A and
A38: b = F3(A,(Lb . A)) by A32, A36, ORDINAL1:29;
consider D being Ordinal such that
A39: Ac = succ D and
A40: c = F3(D,(Lc . D)) by A30, A33, A35, A36, ORDINAL1:29;
A = D by A30, A33, A37, A39, ORDINAL1:7;
hence b = c by A31, A34, A38, A40; ::_thesis: verum
end;
hence b = c by A30, A31, A32, A33, A34, A35; ::_thesis: verum
end;
consider F being Function such that
A41: ( dom F = B & ( for a being set st a in B holds
S4[a,F . a] ) ) from FUNCT_1:sch_2(A29, A21);
reconsider L = F as T-Sequence by A41, ORDINAL1:def_7;
take L ; ::_thesis: S1[B,L]
thus dom L = B by A41; ::_thesis: ( ( {} in B implies L . {} = F2() ) & ( for A being Ordinal st succ A in B holds
L . (succ A) = F3(A,(L . A)) ) & ( for A being Ordinal st A in B & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A)) ) )
thus ( {} in B implies L . {} = F2() ) ::_thesis: ( ( for A being Ordinal st succ A in B holds
L . (succ A) = F3(A,(L . A)) ) & ( for A being Ordinal st A in B & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A)) ) )
proof
assume {} in B ; ::_thesis: L . {} = F2()
then ex A being Ordinal ex K being T-Sequence st
( A = {} & K = G . {} & ( ( A = {} & F . {} = F2() ) or ex B being Ordinal st
( A = succ B & F . {} = F3(B,(K . B)) ) or ( A <> {} & A is limit_ordinal & F . {} = F4(A,K) ) ) ) by A41;
hence L . {} = F2() ; ::_thesis: verum
end;
A42: for A being Ordinal
for L1 being T-Sequence st A in B & L1 = G . A holds
L | A = L1
proof
defpred S5[ Ordinal] means for L1 being T-Sequence st $1 in B & L1 = G . $1 holds
L | $1 = L1;
A43: for A being Ordinal st ( for C being Ordinal st C in A holds
S5[C] ) holds
S5[A]
proof
let A be Ordinal; ::_thesis: ( ( for C being Ordinal st C in A holds
S5[C] ) implies S5[A] )
assume for C being Ordinal st C in A holds
for L1 being T-Sequence st C in B & L1 = G . C holds
L | C = L1 ; ::_thesis: S5[A]
let L1 be T-Sequence; ::_thesis: ( A in B & L1 = G . A implies L | A = L1 )
assume that
A44: A in B and
A45: L1 = G . A ; ::_thesis: L | A = L1
A46: [A,L1] in G by A18, A44, A45, FUNCT_1:1;
then A47: S1[A,L1] by A17;
A48: now__::_thesis:_for_x_being_set_st_x_in_A_holds_
L1_._x_=_(L_|_A)_._x
let x be set ; ::_thesis: ( x in A implies L1 . x = (L | A) . x )
assume A49: x in A ; ::_thesis: L1 . x = (L | A) . x
then reconsider x9 = x as Ordinal ;
A50: x9 in B by A44, A49, ORDINAL1:10;
then consider A1 being Ordinal, L2 being T-Sequence such that
A51: A1 = x9 and
A52: L2 = G . x9 and
A53: ( ( A1 = {} & L . x9 = F2() ) or ex B being Ordinal st
( A1 = succ B & L . x9 = F3(B,(L2 . B)) ) or ( A1 <> {} & A1 is limit_ordinal & L . x9 = F4(A1,L2) ) ) by A41;
for D being Ordinal
for L3 being T-Sequence st D = x9 & L3 = L1 | x9 holds
S1[D,L3]
proof
let D be Ordinal; ::_thesis: for L3 being T-Sequence st D = x9 & L3 = L1 | x9 holds
S1[D,L3]
let L3 be T-Sequence; ::_thesis: ( D = x9 & L3 = L1 | x9 implies S1[D,L3] )
assume that
A54: D = x9 and
A55: L3 = L1 | x9 ; ::_thesis: S1[D,L3]
x9 c= A by A49, ORDINAL1:def_2;
hence dom L3 = D by A47, A54, A55, RELAT_1:62; ::_thesis: ( ( {} in D implies L3 . {} = F2() ) & ( for A being Ordinal st succ A in D holds
L3 . (succ A) = F3(A,(L3 . A)) ) & ( for A being Ordinal st A in D & A <> {} & A is limit_ordinal holds
L3 . A = F4(A,(L3 | A)) ) )
thus ( {} in D implies L3 . {} = F2() ) by A47, A49, A54, A55, FUNCT_1:49, ORDINAL1:10; ::_thesis: ( ( for A being Ordinal st succ A in D holds
L3 . (succ A) = F3(A,(L3 . A)) ) & ( for A being Ordinal st A in D & A <> {} & A is limit_ordinal holds
L3 . A = F4(A,(L3 | A)) ) )
thus for C being Ordinal st succ C in D holds
L3 . (succ C) = F3(C,(L3 . C)) ::_thesis: for A being Ordinal st A in D & A <> {} & A is limit_ordinal holds
L3 . A = F4(A,(L3 | A))
proof
let C be Ordinal; ::_thesis: ( succ C in D implies L3 . (succ C) = F3(C,(L3 . C)) )
assume A56: succ C in D ; ::_thesis: L3 . (succ C) = F3(C,(L3 . C))
C in succ C by ORDINAL1:6;
then A57: (L1 | x9) . C = L1 . C by A54, A56, FUNCT_1:49, ORDINAL1:10;
( succ C in A & (L1 | x9) . (succ C) = L1 . (succ C) ) by A49, A54, A56, FUNCT_1:49, ORDINAL1:10;
hence L3 . (succ C) = F3(C,(L3 . C)) by A17, A46, A55, A57; ::_thesis: verum
end;
let C be Ordinal; ::_thesis: ( C in D & C <> {} & C is limit_ordinal implies L3 . C = F4(C,(L3 | C)) )
assume that
A58: C in D and
A59: ( C <> {} & C is limit_ordinal ) ; ::_thesis: L3 . C = F4(C,(L3 | C))
C c= x9 by A54, A58, ORDINAL1:def_2;
then A60: L1 | C = L3 | C by A55, FUNCT_1:51;
C in A by A49, A54, A58, ORDINAL1:10;
then L1 . C = F4(C,(L3 | C)) by A17, A46, A59, A60;
hence L3 . C = F4(C,(L3 | C)) by A54, A55, A58, FUNCT_1:49; ::_thesis: verum
end;
then [x9,(L1 | x9)] in G by A17, A50;
then A61: L1 | x9 = L2 by A52, FUNCT_1:1;
A62: (L | A) . x = L . x by A49, FUNCT_1:49;
now__::_thesis:_(_ex_D_being_Ordinal_st_x9_=_succ_D_implies_L1_._x_=_(L_|_A)_._x_)
given D being Ordinal such that A63: x9 = succ D ; ::_thesis: L1 . x = (L | A) . x
A64: L1 . x = F3(D,(L1 . D)) by A17, A46, A49, A63;
consider C being Ordinal such that
A65: A1 = succ C and
A66: L . x9 = F3(C,(L2 . C)) by A51, A53, A63, ORDINAL1:29;
C = D by A51, A63, A65, ORDINAL1:7;
hence L1 . x = (L | A) . x by A62, A61, A63, A66, A64, FUNCT_1:49, ORDINAL1:6; ::_thesis: verum
end;
hence L1 . x = (L | A) . x by A17, A46, A49, A51, A53, A62, A61; ::_thesis: verum
end;
A c= dom L by A41, A44, ORDINAL1:def_2;
then dom (L | A) = A by RELAT_1:62;
hence L | A = L1 by A47, A48, FUNCT_1:2; ::_thesis: verum
end;
thus for A being Ordinal holds S5[A] from ORDINAL1:sch_2(A43); ::_thesis: verum
end;
thus for A being Ordinal st succ A in B holds
L . (succ A) = F3(A,(L . A)) ::_thesis: for A being Ordinal st A in B & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A))
proof
let A be Ordinal; ::_thesis: ( succ A in B implies L . (succ A) = F3(A,(L . A)) )
assume A67: succ A in B ; ::_thesis: L . (succ A) = F3(A,(L . A))
then consider C being Ordinal, K being T-Sequence such that
A68: C = succ A and
A69: K = G . (succ A) and
A70: ( ( C = {} & F . (succ A) = F2() ) or ex B being Ordinal st
( C = succ B & F . (succ A) = F3(B,(K . B)) ) or ( C <> {} & C is limit_ordinal & F . (succ A) = F4(C,K) ) ) by A41;
A71: K = L | (succ A) by A42, A67, A69;
consider D being Ordinal such that
A72: C = succ D and
A73: F . (succ A) = F3(D,(K . D)) by A68, A70, ORDINAL1:29;
A = D by A68, A72, ORDINAL1:7;
hence L . (succ A) = F3(A,(L . A)) by A73, A71, FUNCT_1:49, ORDINAL1:6; ::_thesis: verum
end;
let D be Ordinal; ::_thesis: ( D in B & D <> {} & D is limit_ordinal implies L . D = F4(D,(L | D)) )
assume that
A74: D in B and
A75: ( D <> {} & D is limit_ordinal ) ; ::_thesis: L . D = F4(D,(L | D))
ex A being Ordinal ex K being T-Sequence st
( A = D & K = G . D & ( ( A = {} & F . D = F2() ) or ex B being Ordinal st
( A = succ B & F . D = F3(B,(K . B)) ) or ( A <> {} & A is limit_ordinal & F . D = F4(A,K) ) ) ) by A41, A74;
hence L . D = F4(D,(L | D)) by A42, A74, A75, ORDINAL1:29; ::_thesis: verum
end;
for A being Ordinal holds S2[A] from ORDINAL1:sch_2(A1);
hence ex L being T-Sequence st
( dom L = F1() & ( {} in F1() implies L . {} = F2() ) & ( for A being Ordinal st succ A in F1() holds
L . (succ A) = F3(A,(L . A)) ) & ( for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A)) ) ) ; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 6
TSResult{ F1() -> T-Sequence, F2( Ordinal) -> set , F3() -> Ordinal, F4() -> set , F5( Ordinal, set ) -> set , F6( Ordinal, T-Sequence) -> set } :
for A being Ordinal st A in dom F1() holds
F1() . A = F2(A)
provided
A1: for A being Ordinal
for x being set holds
( x = F2(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F4() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F5(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F6(C,(L | C)) ) ) ) and
A2: dom F1() = F3() and
A3: ( {} in F3() implies F1() . {} = F4() ) and
A4: for A being Ordinal st succ A in F3() holds
F1() . (succ A) = F5(A,(F1() . A)) and
A5: for A being Ordinal st A in F3() & A <> {} & A is limit_ordinal holds
F1() . A = F6(A,(F1() | A))
proof
let A be Ordinal; ::_thesis: ( A in dom F1() implies F1() . A = F2(A) )
set L = F1() | (succ A);
assume A in dom F1() ; ::_thesis: F1() . A = F2(A)
then A6: succ A c= dom F1() by ORDINAL1:21;
A7: for C being Ordinal st succ C in succ A holds
(F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C))
proof
let C be Ordinal; ::_thesis: ( succ C in succ A implies (F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C)) )
assume A8: succ C in succ A ; ::_thesis: (F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C))
C in succ C by ORDINAL1:6;
then A9: (F1() | (succ A)) . C = F1() . C by A8, FUNCT_1:49, ORDINAL1:10;
(F1() | (succ A)) . (succ C) = F1() . (succ C) by A8, FUNCT_1:49;
hence (F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C)) by A2, A4, A6, A8, A9; ::_thesis: verum
end;
A10: for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
(F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C))
proof
let C be Ordinal; ::_thesis: ( C in succ A & C <> {} & C is limit_ordinal implies (F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C)) )
assume that
A11: C in succ A and
A12: ( C <> {} & C is limit_ordinal ) ; ::_thesis: (F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C))
C c= succ A by A11, ORDINAL1:def_2;
then A13: (F1() | (succ A)) | C = F1() | C by FUNCT_1:51;
(F1() | (succ A)) . C = F1() . C by A11, FUNCT_1:49;
hence (F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C)) by A2, A5, A6, A11, A12, A13; ::_thesis: verum
end;
{} c= succ A ;
then {} c< succ A by XBOOLE_0:def_8;
then A14: ( {} in succ A & (F1() | (succ A)) . {} = F1() . {} ) by FUNCT_1:49, ORDINAL1:11;
A15: dom (F1() | (succ A)) = succ A by A6, RELAT_1:62;
then ( A in succ A & last (F1() | (succ A)) = (F1() | (succ A)) . A ) by Th2, ORDINAL1:21;
then last (F1() | (succ A)) = F1() . A by FUNCT_1:49;
hence F1() . A = F2(A) by A1, A2, A3, A6, A15, A14, A7, A10; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 7
TSDef{ F1() -> Ordinal, F2() -> set , F3( Ordinal, set ) -> set , F4( Ordinal, T-Sequence) -> set } :
( ex x being set ex L being T-Sequence st
( x = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) & ( for x1, x2 being set st ex L being T-Sequence st
( x1 = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) & ex L being T-Sequence st
( x2 = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) holds
x1 = x2 ) )
proof
consider L being T-Sequence such that
A1: ( dom L = succ F1() & ( {} in succ F1() implies L . {} = F2() ) & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) from ORDINAL2:sch_5();
thus ex x being set ex L being T-Sequence st
( x = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) ::_thesis: for x1, x2 being set st ex L being T-Sequence st
( x1 = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) & ex L being T-Sequence st
( x2 = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) holds
x1 = x2
proof
take x = last L; ::_thesis: ex L being T-Sequence st
( x = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) )
take L ; ::_thesis: ( x = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) )
thus ( x = last L & dom L = succ F1() ) by A1; ::_thesis: ( L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) )
{} c= succ F1() ;
then {} c< succ F1() by XBOOLE_0:def_8;
hence ( L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) by A1, ORDINAL1:11; ::_thesis: verum
end;
let x1, x2 be set ; ::_thesis: ( ex L being T-Sequence st
( x1 = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) & ex L being T-Sequence st
( x2 = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) implies x1 = x2 )
given L1 being T-Sequence such that A2: x1 = last L1 and
A3: dom L1 = succ F1() and
A4: L1 . {} = F2() and
A5: for C being Ordinal st succ C in succ F1() holds
L1 . (succ C) = F3(C,(L1 . C)) and
A6: for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L1 . C = F4(C,(L1 | C)) ; ::_thesis: ( for L being T-Sequence holds
( not x2 = last L or not dom L = succ F1() or not L . {} = F2() or ex C being Ordinal st
( succ C in succ F1() & not L . (succ C) = F3(C,(L . C)) ) or ex C being Ordinal st
( C in succ F1() & C <> {} & C is limit_ordinal & not L . C = F4(C,(L | C)) ) ) or x1 = x2 )
A7: ( {} in succ F1() implies L1 . {} = F2() ) by A4;
given L2 being T-Sequence such that A8: x2 = last L2 and
A9: dom L2 = succ F1() and
A10: L2 . {} = F2() and
A11: for C being Ordinal st succ C in succ F1() holds
L2 . (succ C) = F3(C,(L2 . C)) and
A12: for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L2 . C = F4(C,(L2 | C)) ; ::_thesis: x1 = x2
A13: ( {} in succ F1() implies L2 . {} = F2() ) by A10;
L1 = L2 from ORDINAL2:sch_4(A3, A7, A5, A6, A9, A13, A11, A12);
hence x1 = x2 by A2, A8; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 8
TSResult0{ F1( Ordinal) -> set , F2() -> set , F3( Ordinal, set ) -> set , F4( Ordinal, T-Sequence) -> set } :
F1({}) = F2()
provided
A1: for A being Ordinal
for x being set holds
( x = F1(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F2() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) )
proof
consider L being T-Sequence such that
A2: ( dom L = succ {} & ( {} in succ {} implies L . {} = F2() ) & ( for A being Ordinal st succ A in succ {} holds
L . (succ A) = F3(A,(L . A)) ) & ( for A being Ordinal st A in succ {} & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A)) ) ) from ORDINAL2:sch_5();
F2() = last L by A2, Th2, ORDINAL1:6;
hence F1({}) = F2() by A1, A2, ORDINAL1:6; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 9
TSResultS{ F1() -> set , F2( Ordinal, set ) -> set , F3( Ordinal, T-Sequence) -> set , F4( Ordinal) -> set } :
for A being Ordinal holds F4((succ A)) = F2(A,F4(A))
provided
A1: for A being Ordinal
for x being set holds
( x = F4(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F1() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F2(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F3(C,(L | C)) ) ) )
proof
let A be Ordinal; ::_thesis: F4((succ A)) = F2(A,F4(A))
consider L being T-Sequence such that
A2: dom L = succ (succ A) and
A3: ( {} in succ (succ A) implies L . {} = F1() ) and
A4: for C being Ordinal st succ C in succ (succ A) holds
L . (succ C) = F2(C,(L . C)) and
A5: for C being Ordinal st C in succ (succ A) & C <> {} & C is limit_ordinal holds
L . C = F3(C,(L | C)) from ORDINAL2:sch_5();
A6: for A being Ordinal
for x being set holds
( x = F4(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F1() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F2(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F3(C,(L | C)) ) ) ) by A1;
A7: for B being Ordinal st B in dom L holds
L . B = F4(B) from ORDINAL2:sch_6(A6, A2, A3, A4, A5);
then A8: L . (succ A) = F4((succ A)) by A2, ORDINAL1:6;
( A in succ A & succ A in succ (succ A) ) by ORDINAL1:6;
then L . A = F4(A) by A2, A7, ORDINAL1:10;
hence F4((succ A)) = F2(A,F4(A)) by A4, A8, ORDINAL1:6; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 10
TSResultL{ F1() -> T-Sequence, F2() -> Ordinal, F3( Ordinal) -> set , F4() -> set , F5( Ordinal, set ) -> set , F6( Ordinal, T-Sequence) -> set } :
F3(F2()) = F6(F2(),F1())
provided
A1: for A being Ordinal
for x being set holds
( x = F3(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F4() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F5(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F6(C,(L | C)) ) ) ) and
A2: ( F2() <> {} & F2() is limit_ordinal ) and
A3: dom F1() = F2() and
A4: for A being Ordinal st A in F2() holds
F1() . A = F3(A)
proof
A5: F2() in succ F2() by ORDINAL1:6;
consider L being T-Sequence such that
A6: dom L = succ F2() and
A7: ( {} in succ F2() implies L . {} = F4() ) and
A8: for C being Ordinal st succ C in succ F2() holds
L . (succ C) = F5(C,(L . C)) and
A9: for C being Ordinal st C in succ F2() & C <> {} & C is limit_ordinal holds
L . C = F6(C,(L | C)) from ORDINAL2:sch_5();
set L1 = L | F2();
A10: for A being Ordinal
for x being set holds
( x = F3(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F4() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F5(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F6(C,(L | C)) ) ) ) by A1;
A11: for B being Ordinal st B in dom L holds
L . B = F3(B) from ORDINAL2:sch_6(A10, A6, A7, A8, A9);
A12: now__::_thesis:_for_x_being_set_st_x_in_F2()_holds_
(L_|_F2())_._x_=_F1()_._x
let x be set ; ::_thesis: ( x in F2() implies (L | F2()) . x = F1() . x )
assume A13: x in F2() ; ::_thesis: (L | F2()) . x = F1() . x
then reconsider x9 = x as Ordinal ;
thus (L | F2()) . x = L . x9 by A13, FUNCT_1:49
.= F3(x9) by A6, A11, A5, A13, ORDINAL1:10
.= F1() . x by A4, A13 ; ::_thesis: verum
end;
F2() c= dom L by A6, A5, ORDINAL1:def_2;
then dom (L | F2()) = F2() by RELAT_1:62;
then L | F2() = F1() by A3, A12, FUNCT_1:2;
then L . F2() = F6(F2(),F1()) by A2, A9, ORDINAL1:6;
hence F3(F2()) = F6(F2(),F1()) by A6, A11, ORDINAL1:6; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 11
OSExist{ F1() -> Ordinal, F2() -> Ordinal, F3( Ordinal, Ordinal) -> Ordinal, F4( Ordinal, T-Sequence) -> Ordinal } :
ex fi being Ordinal-Sequence st
( dom fi = F1() & ( {} in F1() implies fi . {} = F2() ) & ( for A being Ordinal st succ A in F1() holds
fi . (succ A) = F3(A,(fi . A)) ) & ( for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
fi . A = F4(A,(fi | A)) ) )
proof
deffunc H1( Ordinal, set ) -> Ordinal = F3($1,(sup (union {$2})));
consider L being T-Sequence such that
A1: dom L = F1() and
A2: ( {} in F1() implies L . {} = F2() ) and
A3: for A being Ordinal st succ A in F1() holds
L . (succ A) = H1(A,L . A) and
A4: for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A)) from ORDINAL2:sch_5();
L is Ordinal-yielding
proof
take sup (rng L) ; :: according to ORDINAL2:def_4 ::_thesis: rng L c= sup (rng L)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng L or x in sup (rng L) )
assume A5: x in rng L ; ::_thesis: x in sup (rng L)
then consider y being set such that
A6: y in dom L and
A7: x = L . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A6;
A8: now__::_thesis:_(_y_<>_{}_&_(_for_B_being_Ordinal_holds_y_<>_succ_B_)_implies_x_is_Ordinal_)
assume that
A9: y <> {} and
A10: for B being Ordinal holds y <> succ B ; ::_thesis: x is Ordinal
y is limit_ordinal by A10, ORDINAL1:29;
then L . y = F4(y,(L | y)) by A1, A4, A6, A9;
hence x is Ordinal by A7; ::_thesis: verum
end;
A11: On (rng L) c= sup (rng L) by Def3;
now__::_thesis:_(_ex_B_being_Ordinal_st_y_=_succ_B_implies_x_is_Ordinal_)
given B being Ordinal such that A12: y = succ B ; ::_thesis: x is Ordinal
L . y = F3(B,(sup (union {(L . B)}))) by A1, A3, A6, A12;
hence x is Ordinal by A7; ::_thesis: verum
end;
then x in On (rng L) by A1, A2, A5, A6, A7, A8, ORDINAL1:def_9;
hence x in sup (rng L) by A11; ::_thesis: verum
end;
then reconsider L = L as Ordinal-Sequence ;
take fi = L; ::_thesis: ( dom fi = F1() & ( {} in F1() implies fi . {} = F2() ) & ( for A being Ordinal st succ A in F1() holds
fi . (succ A) = F3(A,(fi . A)) ) & ( for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
fi . A = F4(A,(fi | A)) ) )
thus ( dom fi = F1() & ( {} in F1() implies fi . {} = F2() ) ) by A1, A2; ::_thesis: ( ( for A being Ordinal st succ A in F1() holds
fi . (succ A) = F3(A,(fi . A)) ) & ( for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
fi . A = F4(A,(fi | A)) ) )
thus for A being Ordinal st succ A in F1() holds
fi . (succ A) = F3(A,(fi . A)) ::_thesis: for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
fi . A = F4(A,(fi | A))
proof
let A be Ordinal; ::_thesis: ( succ A in F1() implies fi . (succ A) = F3(A,(fi . A)) )
reconsider B = fi . A as Ordinal ;
sup (union {B}) = sup B by ZFMISC_1:25
.= B by Th18 ;
hence ( succ A in F1() implies fi . (succ A) = F3(A,(fi . A)) ) by A3; ::_thesis: verum
end;
thus for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
fi . A = F4(A,(fi | A)) by A4; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 12
OSResult{ F1() -> Ordinal-Sequence, F2( Ordinal) -> Ordinal, F3() -> Ordinal, F4() -> Ordinal, F5( Ordinal, Ordinal) -> Ordinal, F6( Ordinal, T-Sequence) -> Ordinal } :
for A being Ordinal st A in dom F1() holds
F1() . A = F2(A)
provided
A1: for A, B being Ordinal holds
( B = F2(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F4() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F5(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F6(C,(fi | C)) ) ) ) and
A2: dom F1() = F3() and
A3: ( {} in F3() implies F1() . {} = F4() ) and
A4: for A being Ordinal st succ A in F3() holds
F1() . (succ A) = F5(A,(F1() . A)) and
A5: for A being Ordinal st A in F3() & A <> {} & A is limit_ordinal holds
F1() . A = F6(A,(F1() | A))
proof
let A be Ordinal; ::_thesis: ( A in dom F1() implies F1() . A = F2(A) )
set fi = F1() | (succ A);
assume A in dom F1() ; ::_thesis: F1() . A = F2(A)
then A6: succ A c= dom F1() by ORDINAL1:21;
A7: for C being Ordinal st succ C in succ A holds
(F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C))
proof
let C be Ordinal; ::_thesis: ( succ C in succ A implies (F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C)) )
assume A8: succ C in succ A ; ::_thesis: (F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C))
C in succ C by ORDINAL1:6;
then A9: (F1() | (succ A)) . C = F1() . C by A8, FUNCT_1:49, ORDINAL1:10;
(F1() | (succ A)) . (succ C) = F1() . (succ C) by A8, FUNCT_1:49;
hence (F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C)) by A2, A4, A6, A8, A9; ::_thesis: verum
end;
A10: for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
(F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C))
proof
let C be Ordinal; ::_thesis: ( C in succ A & C <> {} & C is limit_ordinal implies (F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C)) )
assume that
A11: C in succ A and
A12: ( C <> {} & C is limit_ordinal ) ; ::_thesis: (F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C))
C c= succ A by A11, ORDINAL1:def_2;
then A13: (F1() | (succ A)) | C = F1() | C by FUNCT_1:51;
(F1() | (succ A)) . C = F1() . C by A11, FUNCT_1:49;
hence (F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C)) by A2, A5, A6, A11, A12, A13; ::_thesis: verum
end;
{} c= succ A ;
then {} c< succ A by XBOOLE_0:def_8;
then A14: ( {} in succ A & (F1() | (succ A)) . {} = F1() . {} ) by FUNCT_1:49, ORDINAL1:11;
A15: dom (F1() | (succ A)) = succ A by A6, RELAT_1:62;
then ( A in succ A & last (F1() | (succ A)) = (F1() | (succ A)) . A ) by Th2, ORDINAL1:21;
then last (F1() | (succ A)) = F1() . A by FUNCT_1:49;
hence F1() . A = F2(A) by A1, A2, A3, A6, A15, A14, A7, A10; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 13
OSDef{ F1() -> Ordinal, F2() -> Ordinal, F3( Ordinal, Ordinal) -> Ordinal, F4( Ordinal, T-Sequence) -> Ordinal } :
( ex A being Ordinal ex fi being Ordinal-Sequence st
( A = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) holds
A1 = A2 ) )
proof
consider fi being Ordinal-Sequence such that
A1: ( dom fi = succ F1() & ( {} in succ F1() implies fi . {} = F2() ) & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) from ORDINAL2:sch_11();
reconsider A = last fi as Ordinal ;
thus ex A being Ordinal ex fi being Ordinal-Sequence st
( A = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) ::_thesis: for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) holds
A1 = A2
proof
take A ; ::_thesis: ex fi being Ordinal-Sequence st
( A = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) )
take fi ; ::_thesis: ( A = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) )
thus ( A = last fi & dom fi = succ F1() ) by A1; ::_thesis: ( fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) )
{} c= succ F1() ;
then {} c< succ F1() by XBOOLE_0:def_8;
hence ( fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) by A1, ORDINAL1:11; ::_thesis: verum
end;
deffunc H1( Ordinal, Ordinal) -> Ordinal = F3($1,(sup (union {$2})));
let A1, A2 be Ordinal; ::_thesis: ( ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) implies A1 = A2 )
given L1 being Ordinal-Sequence such that A2: A1 = last L1 and
A3: dom L1 = succ F1() and
A4: L1 . {} = F2() and
A5: for C being Ordinal st succ C in succ F1() holds
L1 . (succ C) = F3(C,(L1 . C)) and
A6: for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L1 . C = F4(C,(L1 | C)) ; ::_thesis: ( for fi being Ordinal-Sequence holds
( not A2 = last fi or not dom fi = succ F1() or not fi . {} = F2() or ex C being Ordinal st
( succ C in succ F1() & not fi . (succ C) = F3(C,(fi . C)) ) or ex C being Ordinal st
( C in succ F1() & C <> {} & C is limit_ordinal & not fi . C = F4(C,(fi | C)) ) ) or A1 = A2 )
A7: ( {} in succ F1() implies L1 . {} = F2() ) by A4;
A8: for C being Ordinal st succ C in succ F1() holds
L1 . (succ C) = H1(C,L1 . C)
proof
let C be Ordinal; ::_thesis: ( succ C in succ F1() implies L1 . (succ C) = H1(C,L1 . C) )
assume A9: succ C in succ F1() ; ::_thesis: L1 . (succ C) = H1(C,L1 . C)
reconsider x9 = L1 . C as Ordinal ;
sup (union {(L1 . C)}) = sup x9 by ZFMISC_1:25
.= x9 by Th18 ;
hence L1 . (succ C) = H1(C,L1 . C) by A5, A9; ::_thesis: verum
end;
given L2 being Ordinal-Sequence such that A10: A2 = last L2 and
A11: dom L2 = succ F1() and
A12: L2 . {} = F2() and
A13: for C being Ordinal st succ C in succ F1() holds
L2 . (succ C) = F3(C,(L2 . C)) and
A14: for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L2 . C = F4(C,(L2 | C)) ; ::_thesis: A1 = A2
A15: for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L2 . C = F4(C,(L2 | C)) by A14;
A16: for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L1 . C = F4(C,(L1 | C)) by A6;
A17: for C being Ordinal st succ C in succ F1() holds
L2 . (succ C) = H1(C,L2 . C)
proof
let C be Ordinal; ::_thesis: ( succ C in succ F1() implies L2 . (succ C) = H1(C,L2 . C) )
assume A18: succ C in succ F1() ; ::_thesis: L2 . (succ C) = H1(C,L2 . C)
reconsider x9 = L2 . C as Ordinal ;
sup (union {(L2 . C)}) = sup x9 by ZFMISC_1:25
.= x9 by Th18 ;
hence L2 . (succ C) = H1(C,L2 . C) by A13, A18; ::_thesis: verum
end;
A19: ( {} in succ F1() implies L2 . {} = F2() ) by A12;
L1 = L2 from ORDINAL2:sch_4(A3, A7, A8, A16, A11, A19, A17, A15);
hence A1 = A2 by A2, A10; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 14
OSResult0{ F1( Ordinal) -> Ordinal, F2() -> Ordinal, F3( Ordinal, Ordinal) -> Ordinal, F4( Ordinal, T-Sequence) -> Ordinal } :
F1({}) = F2()
provided
A1: for A, B being Ordinal holds
( B = F1(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F2() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) )
proof
consider fi being Ordinal-Sequence such that
A2: ( dom fi = succ {} & ( {} in succ {} implies fi . {} = F2() ) & ( for A being Ordinal st succ A in succ {} holds
fi . (succ A) = F3(A,(fi . A)) ) & ( for A being Ordinal st A in succ {} & A <> {} & A is limit_ordinal holds
fi . A = F4(A,(fi | A)) ) ) from ORDINAL2:sch_11();
F2() = last fi by A2, Th2, ORDINAL1:6;
hence F1({}) = F2() by A1, A2, ORDINAL1:6; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 15
OSResultS{ F1() -> Ordinal, F2( Ordinal, Ordinal) -> Ordinal, F3( Ordinal, T-Sequence) -> Ordinal, F4( Ordinal) -> Ordinal } :
for A being Ordinal holds F4((succ A)) = F2(A,F4(A))
provided
A1: for A, B being Ordinal holds
( B = F4(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F1() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F2(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F3(C,(fi | C)) ) ) )
proof
let A be Ordinal; ::_thesis: F4((succ A)) = F2(A,F4(A))
consider fi being Ordinal-Sequence such that
A2: dom fi = succ (succ A) and
A3: ( {} in succ (succ A) implies fi . {} = F1() ) and
A4: for C being Ordinal st succ C in succ (succ A) holds
fi . (succ C) = F2(C,(fi . C)) and
A5: for C being Ordinal st C in succ (succ A) & C <> {} & C is limit_ordinal holds
fi . C = F3(C,(fi | C)) from ORDINAL2:sch_11();
A6: for A, B being Ordinal holds
( B = F4(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F1() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F2(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F3(C,(fi | C)) ) ) ) by A1;
A7: for B being Ordinal st B in dom fi holds
fi . B = F4(B) from ORDINAL2:sch_12(A6, A2, A3, A4, A5);
then A8: fi . (succ A) = F4((succ A)) by A2, ORDINAL1:6;
( A in succ A & succ A in succ (succ A) ) by ORDINAL1:6;
then fi . A = F4(A) by A2, A7, ORDINAL1:10;
hence F4((succ A)) = F2(A,F4(A)) by A4, A8, ORDINAL1:6; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 16
OSResultL{ F1() -> Ordinal-Sequence, F2() -> Ordinal, F3( Ordinal) -> Ordinal, F4() -> Ordinal, F5( Ordinal, Ordinal) -> Ordinal, F6( Ordinal, T-Sequence) -> Ordinal } :
F3(F2()) = F6(F2(),F1())
provided
A1: for A, B being Ordinal holds
( B = F3(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F4() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F5(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F6(C,(fi | C)) ) ) ) and
A2: ( F2() <> {} & F2() is limit_ordinal ) and
A3: dom F1() = F2() and
A4: for A being Ordinal st A in F2() holds
F1() . A = F3(A)
proof
A5: F2() in succ F2() by ORDINAL1:6;
consider fi being Ordinal-Sequence such that
A6: dom fi = succ F2() and
A7: ( {} in succ F2() implies fi . {} = F4() ) and
A8: for C being Ordinal st succ C in succ F2() holds
fi . (succ C) = F5(C,(fi . C)) and
A9: for C being Ordinal st C in succ F2() & C <> {} & C is limit_ordinal holds
fi . C = F6(C,(fi | C)) from ORDINAL2:sch_11();
set psi = fi | F2();
A10: for A, B being Ordinal holds
( B = F3(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F4() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F5(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F6(C,(fi | C)) ) ) ) by A1;
A11: for B being Ordinal st B in dom fi holds
fi . B = F3(B) from ORDINAL2:sch_12(A10, A6, A7, A8, A9);
A12: now__::_thesis:_for_x_being_set_st_x_in_F2()_holds_
(fi_|_F2())_._x_=_F1()_._x
let x be set ; ::_thesis: ( x in F2() implies (fi | F2()) . x = F1() . x )
assume A13: x in F2() ; ::_thesis: (fi | F2()) . x = F1() . x
then reconsider x9 = x as Ordinal ;
thus (fi | F2()) . x = fi . x9 by A13, FUNCT_1:49
.= F3(x9) by A6, A11, A5, A13, ORDINAL1:10
.= F1() . x by A4, A13 ; ::_thesis: verum
end;
F2() c= dom fi by A6, A5, ORDINAL1:def_2;
then dom (fi | F2()) = F2() by RELAT_1:62;
then fi | F2() = F1() by A3, A12, FUNCT_1:2;
then fi . F2() = F6(F2(),F1()) by A2, A9, ORDINAL1:6;
hence F3(F2()) = F6(F2(),F1()) by A6, A11, ORDINAL1:6; ::_thesis: verum
end;
definition
let L be T-Sequence;
func sup L -> Ordinal equals :: ORDINAL2:def 5
sup (rng L);
correctness
coherence
sup (rng L) is Ordinal;
;
func inf L -> Ordinal equals :: ORDINAL2:def 6
inf (rng L);
correctness
coherence
inf (rng L) is Ordinal;
;
end;
:: deftheorem defines sup ORDINAL2:def_5_:_
for L being T-Sequence holds sup L = sup (rng L);
:: deftheorem defines inf ORDINAL2:def_6_:_
for L being T-Sequence holds inf L = inf (rng L);
theorem :: ORDINAL2:26
for L being T-Sequence holds
( sup L = sup (rng L) & inf L = inf (rng L) ) ;
definition
let L be T-Sequence;
func lim_sup L -> Ordinal means :: ORDINAL2:def 7
ex fi being Ordinal-Sequence st
( it = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) );
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) )
proof
deffunc H1( Ordinal) -> Ordinal = sup (rng (L | ((dom L) \ $1)));
consider fi being Ordinal-Sequence such that
A1: ( dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = H1(A) ) ) from ORDINAL2:sch_3();
take inf fi ; ::_thesis: ex fi being Ordinal-Sequence st
( inf fi = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) )
take fi ; ::_thesis: ( inf fi = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) )
thus ( inf fi = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) & ex fi being Ordinal-Sequence st
( b2 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) holds
b1 = b2
proof
let A1, A2 be Ordinal; ::_thesis: ( ex fi being Ordinal-Sequence st
( A1 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) & ex fi being Ordinal-Sequence st
( A2 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) implies A1 = A2 )
given fi being Ordinal-Sequence such that A2: ( A1 = inf fi & dom fi = dom L ) and
A3: for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ; ::_thesis: ( for fi being Ordinal-Sequence holds
( not A2 = inf fi or not dom fi = dom L or ex A being Ordinal st
( A in dom L & not fi . A = sup (rng (L | ((dom L) \ A))) ) ) or A1 = A2 )
given psi being Ordinal-Sequence such that A4: ( A2 = inf psi & dom psi = dom L ) and
A5: for A being Ordinal st A in dom L holds
psi . A = sup (rng (L | ((dom L) \ A))) ; ::_thesis: A1 = A2
now__::_thesis:_for_x_being_set_st_x_in_dom_L_holds_
fi_._x_=_psi_._x
let x be set ; ::_thesis: ( x in dom L implies fi . x = psi . x )
assume A6: x in dom L ; ::_thesis: fi . x = psi . x
then reconsider A = x as Ordinal ;
fi . A = sup (rng (L | ((dom L) \ A))) by A3, A6;
hence fi . x = psi . x by A5, A6; ::_thesis: verum
end;
hence A1 = A2 by A2, A4, FUNCT_1:2; ::_thesis: verum
end;
func lim_inf L -> Ordinal means :: ORDINAL2:def 8
ex fi being Ordinal-Sequence st
( it = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) );
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) )
proof
deffunc H1( Ordinal) -> Ordinal = inf (rng (L | ((dom L) \ $1)));
consider fi being Ordinal-Sequence such that
A7: ( dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = H1(A) ) ) from ORDINAL2:sch_3();
take sup fi ; ::_thesis: ex fi being Ordinal-Sequence st
( sup fi = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) )
take fi ; ::_thesis: ( sup fi = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) )
thus ( sup fi = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) by A7; ::_thesis: verum
end;
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) & ex fi being Ordinal-Sequence st
( b2 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) holds
b1 = b2
proof
let A1, A2 be Ordinal; ::_thesis: ( ex fi being Ordinal-Sequence st
( A1 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) & ex fi being Ordinal-Sequence st
( A2 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) implies A1 = A2 )
given fi being Ordinal-Sequence such that A8: ( A1 = sup fi & dom fi = dom L ) and
A9: for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ; ::_thesis: ( for fi being Ordinal-Sequence holds
( not A2 = sup fi or not dom fi = dom L or ex A being Ordinal st
( A in dom L & not fi . A = inf (rng (L | ((dom L) \ A))) ) ) or A1 = A2 )
given psi being Ordinal-Sequence such that A10: ( A2 = sup psi & dom psi = dom L ) and
A11: for A being Ordinal st A in dom L holds
psi . A = inf (rng (L | ((dom L) \ A))) ; ::_thesis: A1 = A2
now__::_thesis:_for_x_being_set_st_x_in_dom_L_holds_
fi_._x_=_psi_._x
let x be set ; ::_thesis: ( x in dom L implies fi . x = psi . x )
assume A12: x in dom L ; ::_thesis: fi . x = psi . x
then reconsider A = x as Ordinal ;
fi . A = inf (rng (L | ((dom L) \ A))) by A9, A12;
hence fi . x = psi . x by A11, A12; ::_thesis: verum
end;
hence A1 = A2 by A8, A10, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem defines lim_sup ORDINAL2:def_7_:_
for L being T-Sequence
for b2 being Ordinal holds
( b2 = lim_sup L iff ex fi being Ordinal-Sequence st
( b2 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) );
:: deftheorem defines lim_inf ORDINAL2:def_8_:_
for L being T-Sequence
for b2 being Ordinal holds
( b2 = lim_inf L iff ex fi being Ordinal-Sequence st
( b2 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) );
definition
let A be Ordinal;
let fi be Ordinal-Sequence;
predA is_limes_of fi means :Def9: :: ORDINAL2:def 9
ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) if A = {}
otherwise for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) );
consistency
verum ;
end;
:: deftheorem Def9 defines is_limes_of ORDINAL2:def_9_:_
for A being Ordinal
for fi being Ordinal-Sequence holds
( ( A = {} implies ( A is_limes_of fi iff ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) ) ) & ( not A = {} implies ( A is_limes_of fi iff for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) ) ) ) );
definition
let fi be Ordinal-Sequence;
given A being Ordinal such that A1: A is_limes_of fi ;
func lim fi -> Ordinal means :Def10: :: ORDINAL2:def 10
it is_limes_of fi;
existence
ex b1 being Ordinal st b1 is_limes_of fi by A1;
uniqueness
for b1, b2 being Ordinal st b1 is_limes_of fi & b2 is_limes_of fi holds
b1 = b2
proof
let A1, A2 be Ordinal; ::_thesis: ( A1 is_limes_of fi & A2 is_limes_of fi implies A1 = A2 )
assume that
A2: ( ( A1 = {} & ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) ) or ( A1 <> {} & ( for B, C being Ordinal st B in A1 & A1 in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) ) ) ) ) and
A3: ( ( A2 = {} & ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) ) or ( A2 <> {} & ( for B, C being Ordinal st B in A2 & A2 in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) ) ) ) ) ; :: according to ORDINAL2:def_9 ::_thesis: A1 = A2
A4: now__::_thesis:_not_A1_in_A2
set x = the Element of A1;
reconsider x = the Element of A1 as Ordinal ;
assume A1 in A2 ; ::_thesis: contradiction
then consider D being Ordinal such that
A5: D in dom fi and
A6: for A being Ordinal st D c= A & A in dom fi holds
( A1 in fi . A & fi . A in succ A2 ) by A3, ORDINAL1:6;
now__::_thesis:_not_A1_=_{}
assume A1 = {} ; ::_thesis: contradiction
then consider B being Ordinal such that
A7: B in dom fi and
A8: for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} by A2;
( B c= D or D c= B ) ;
then consider E being Ordinal such that
A9: ( ( E = D & B c= D ) or ( E = B & D c= B ) ) ;
fi . E = {} by A5, A7, A8, A9;
hence contradiction by A5, A6, A7, A9; ::_thesis: verum
end;
then consider C being Ordinal such that
A10: C in dom fi and
A11: for A being Ordinal st C c= A & A in dom fi holds
( x in fi . A & fi . A in succ A1 ) by A2, ORDINAL1:6;
( C c= D or D c= C ) ;
then consider E being Ordinal such that
A12: ( ( E = D & C c= D ) or ( E = C & D c= C ) ) ;
fi . E in succ A1 by A5, A10, A11, A12;
then A13: ( fi . E in A1 or fi . E = A1 ) by ORDINAL1:8;
A1 in fi . E by A5, A6, A10, A12;
hence contradiction by A13; ::_thesis: verum
end;
set x = the Element of A2;
reconsider x = the Element of A2 as Ordinal ;
assume A1 <> A2 ; ::_thesis: contradiction
then ( A1 in A2 or A2 in A1 ) by ORDINAL1:14;
then consider D being Ordinal such that
A14: D in dom fi and
A15: for A being Ordinal st D c= A & A in dom fi holds
( A2 in fi . A & fi . A in succ A1 ) by A2, A4, ORDINAL1:6;
now__::_thesis:_not_A2_=_{}
assume A2 = {} ; ::_thesis: contradiction
then consider B being Ordinal such that
A16: B in dom fi and
A17: for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} by A3;
( B c= D or D c= B ) ;
then consider E being Ordinal such that
A18: ( ( E = D & B c= D ) or ( E = B & D c= B ) ) ;
fi . E = {} by A14, A16, A17, A18;
hence contradiction by A14, A15, A16, A18; ::_thesis: verum
end;
then consider C being Ordinal such that
A19: C in dom fi and
A20: for A being Ordinal st C c= A & A in dom fi holds
( x in fi . A & fi . A in succ A2 ) by A3, ORDINAL1:6;
( C c= D or D c= C ) ;
then consider E being Ordinal such that
A21: ( ( E = D & C c= D ) or ( E = C & D c= C ) ) ;
fi . E in succ A2 by A14, A19, A20, A21;
then A22: ( fi . E in A2 or fi . E = A2 ) by ORDINAL1:8;
A2 in fi . E by A14, A15, A19, A21;
hence contradiction by A22; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines lim ORDINAL2:def_10_:_
for fi being Ordinal-Sequence st ex A being Ordinal st A is_limes_of fi holds
for b2 being Ordinal holds
( b2 = lim fi iff b2 is_limes_of fi );
definition
let A be Ordinal;
let fi be Ordinal-Sequence;
func lim (A,fi) -> Ordinal equals :: ORDINAL2:def 11
lim (fi | A);
correctness
coherence
lim (fi | A) is Ordinal;
;
end;
:: deftheorem defines lim ORDINAL2:def_11_:_
for A being Ordinal
for fi being Ordinal-Sequence holds lim (A,fi) = lim (fi | A);
definition
let L be Ordinal-Sequence;
attrL is increasing means :: ORDINAL2:def 12
for A, B being Ordinal st A in B & B in dom L holds
L . A in L . B;
attrL is continuous means :: ORDINAL2:def 13
for A, B being Ordinal st A in dom L & A <> {} & A is limit_ordinal & B = L . A holds
B is_limes_of L | A;
end;
:: deftheorem defines increasing ORDINAL2:def_12_:_
for L being Ordinal-Sequence holds
( L is increasing iff for A, B being Ordinal st A in B & B in dom L holds
L . A in L . B );
:: deftheorem defines continuous ORDINAL2:def_13_:_
for L being Ordinal-Sequence holds
( L is continuous iff for A, B being Ordinal st A in dom L & A <> {} & A is limit_ordinal & B = L . A holds
B is_limes_of L | A );
definition
let A, B be Ordinal;
funcA +^ B -> Ordinal means :Def14: :: ORDINAL2:def 14
ex fi being Ordinal-Sequence st
( it = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) );
correctness
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) );
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) holds
b1 = b2;
proof
deffunc H1( Ordinal, T-Sequence) -> Ordinal = sup $2;
deffunc H2( Ordinal, Ordinal) -> set = succ $2;
( ex F being Ordinal ex fi being Ordinal-Sequence st
( F = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) holds
A1 = A2 ) ) from ORDINAL2:sch_13();
hence ( ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) & ( for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def14 defines +^ ORDINAL2:def_14_:_
for A, B, b3 being Ordinal holds
( b3 = A +^ B iff ex fi being Ordinal-Sequence st
( b3 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) );
definition
let A, B be Ordinal;
funcA *^ B -> Ordinal means :Def15: :: ORDINAL2:def 15
ex fi being Ordinal-Sequence st
( it = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) );
correctness
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) );
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) holds
b1 = b2;
proof
deffunc H1( Ordinal, Ordinal-Sequence) -> set = union (sup $2);
deffunc H2( Ordinal, Ordinal) -> Ordinal = $2 +^ B;
( ex F being Ordinal ex fi being Ordinal-Sequence st
( F = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) holds
A1 = A2 ) ) from ORDINAL2:sch_13();
hence ( ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) & ( for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def15 defines *^ ORDINAL2:def_15_:_
for A, B, b3 being Ordinal holds
( b3 = A *^ B iff ex fi being Ordinal-Sequence st
( b3 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) );
registration
let O be Ordinal;
cluster -> ordinal for Element of O;
coherence
for b1 being Element of O holds b1 is ordinal ;
end;
definition
let A, B be Ordinal;
func exp (A,B) -> Ordinal means :Def16: :: ORDINAL2:def 16
ex fi being Ordinal-Sequence st
( it = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) );
correctness
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) );
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) holds
b1 = b2;
proof
deffunc H1( Ordinal, Ordinal-Sequence) -> Ordinal = lim $2;
deffunc H2( Ordinal, Ordinal) -> Ordinal = A *^ $2;
( ex F being Ordinal ex fi being Ordinal-Sequence st
( F = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) holds
A1 = A2 ) ) from ORDINAL2:sch_13();
hence ( ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) & ( for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def16 defines exp ORDINAL2:def_16_:_
for A, B, b3 being Ordinal holds
( b3 = exp (A,B) iff ex fi being Ordinal-Sequence st
( b3 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) );
theorem Th27: :: ORDINAL2:27
for A being Ordinal holds A +^ {} = A
proof
let A be Ordinal; ::_thesis: A +^ {} = A
deffunc H1( Ordinal, Ordinal) -> set = succ $2;
deffunc H2( Ordinal, T-Sequence) -> Ordinal = sup $2;
deffunc H3( Ordinal) -> Ordinal = A +^ $1;
A1: for B, C being Ordinal holds
( C = H3(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H1(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H2(C,fi | C) ) ) ) by Def14;
thus H3( {} ) = A from ORDINAL2:sch_14(A1); ::_thesis: verum
end;
theorem Th28: :: ORDINAL2:28
for A, B being Ordinal holds A +^ (succ B) = succ (A +^ B)
proof
let A, B be Ordinal; ::_thesis: A +^ (succ B) = succ (A +^ B)
deffunc H1( Ordinal, Ordinal) -> set = succ $2;
deffunc H2( Ordinal, T-Sequence) -> Ordinal = sup $2;
deffunc H3( Ordinal) -> Ordinal = A +^ $1;
A1: for B, C being Ordinal holds
( C = H3(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H1(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H2(C,fi | C) ) ) ) by Def14;
for B being Ordinal holds H3( succ B) = H1(B,H3(B)) from ORDINAL2:sch_15(A1);
hence A +^ (succ B) = succ (A +^ B) ; ::_thesis: verum
end;
theorem Th29: :: ORDINAL2:29
for B, A being Ordinal st B <> {} & B is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = A +^ C ) holds
A +^ B = sup fi
proof
let B, A be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal implies for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = A +^ C ) holds
A +^ B = sup fi )
deffunc H1( Ordinal, Ordinal) -> set = succ $2;
deffunc H2( Ordinal, Ordinal-Sequence) -> Ordinal = sup $2;
assume A1: ( B <> {} & B is limit_ordinal ) ; ::_thesis: for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = A +^ C ) holds
A +^ B = sup fi
deffunc H3( Ordinal) -> Ordinal = A +^ $1;
let fi be Ordinal-Sequence; ::_thesis: ( dom fi = B & ( for C being Ordinal st C in B holds
fi . C = A +^ C ) implies A +^ B = sup fi )
assume that
A2: dom fi = B and
A3: for C being Ordinal st C in B holds
fi . C = H3(C) ; ::_thesis: A +^ B = sup fi
A4: for B, C being Ordinal holds
( C = H3(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H1(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H2(C,fi | C) ) ) ) by Def14;
thus H3(B) = H2(B,fi) from ORDINAL2:sch_16(A4, A1, A2, A3); ::_thesis: verum
end;
theorem Th30: :: ORDINAL2:30
for A being Ordinal holds {} +^ A = A
proof
let A be Ordinal; ::_thesis: {} +^ A = A
defpred S1[ Ordinal] means {} +^ $1 = $1;
A1: for A being Ordinal st S1[A] holds
S1[ succ A] by Th28;
A2: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
deffunc H1( Ordinal) -> Ordinal = {} +^ $1;
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
A3: ( A <> {} & A is limit_ordinal ) and
A4: for B being Ordinal st B in A holds
{} +^ B = B ; ::_thesis: S1[A]
consider fi being Ordinal-Sequence such that
A5: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H1(B) ) ) from ORDINAL2:sch_3();
A6: rng fi = A
proof
thus for x being set st x in rng fi holds
x in A :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A c= rng fi
proof
let x be set ; ::_thesis: ( x in rng fi implies x in A )
assume x in rng fi ; ::_thesis: x in A
then consider y being set such that
A7: y in dom fi and
A8: x = fi . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A7;
x = {} +^ y by A5, A7, A8
.= y by A4, A5, A7 ;
hence x in A by A5, A7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in rng fi )
assume A9: x in A ; ::_thesis: x in rng fi
then reconsider B = x as Ordinal ;
( {} +^ B = B & fi . B = {} +^ B ) by A4, A5, A9;
hence x in rng fi by A5, A9, FUNCT_1:def_3; ::_thesis: verum
end;
{} +^ A = sup fi by A3, A5, Th29
.= sup (rng fi) ;
hence S1[A] by A6, Th18; ::_thesis: verum
end;
A10: S1[ {} ] by Th27;
for A being Ordinal holds S1[A] from ORDINAL2:sch_1(A10, A1, A2);
hence {} +^ A = A ; ::_thesis: verum
end;
Lm1: 1 = succ {}
;
theorem :: ORDINAL2:31
for A being Ordinal holds A +^ 1 = succ A
proof
let A be Ordinal; ::_thesis: A +^ 1 = succ A
thus A +^ 1 = succ (A +^ {}) by Lm1, Th28
.= succ A by Th27 ; ::_thesis: verum
end;
theorem Th32: :: ORDINAL2:32
for A, B, C being Ordinal st A in B holds
C +^ A in C +^ B
proof
let A, B, C be Ordinal; ::_thesis: ( A in B implies C +^ A in C +^ B )
defpred S1[ Ordinal] means ( A in $1 implies C +^ A in C +^ $1 );
A1: for B being Ordinal st ( for D being Ordinal st D in B holds
S1[D] ) holds
S1[B]
proof
let B be Ordinal; ::_thesis: ( ( for D being Ordinal st D in B holds
S1[D] ) implies S1[B] )
assume that
A2: for D being Ordinal st D in B & A in D holds
C +^ A in C +^ D and
A3: A in B ; ::_thesis: C +^ A in C +^ B
A4: now__::_thesis:_(_ex_D_being_Ordinal_st_B_=_succ_D_implies_C_+^_A_in_C_+^_B_)
given D being Ordinal such that A5: B = succ D ; ::_thesis: C +^ A in C +^ B
A6: now__::_thesis:_(_A_in_D_implies_C_+^_A_in_C_+^_B_)
assume A in D ; ::_thesis: C +^ A in C +^ B
then A7: C +^ A in C +^ D by A2, A5, ORDINAL1:6;
( succ (C +^ D) = C +^ (succ D) & C +^ D in succ (C +^ D) ) by Th28, ORDINAL1:6;
hence C +^ A in C +^ B by A5, A7, ORDINAL1:10; ::_thesis: verum
end;
now__::_thesis:_(_not_A_in_D_implies_C_+^_A_in_C_+^_B_)
assume A8: not A in D ; ::_thesis: C +^ A in C +^ B
( A c< D iff ( A c= D & A <> D ) ) by XBOOLE_0:def_8;
then C +^ A in succ (C +^ D) by A3, A5, A8, ORDINAL1:11, ORDINAL1:22;
hence C +^ A in C +^ B by A5, Th28; ::_thesis: verum
end;
hence C +^ A in C +^ B by A6; ::_thesis: verum
end;
now__::_thesis:_(_(_for_D_being_Ordinal_holds_B_<>_succ_D_)_implies_C_+^_A_in_C_+^_B_)
deffunc H1( Ordinal) -> Ordinal = C +^ $1;
consider fi being Ordinal-Sequence such that
A9: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H1(D) ) ) from ORDINAL2:sch_3();
fi . A = C +^ A by A3, A9;
then A10: C +^ A in rng fi by A3, A9, FUNCT_1:def_3;
assume for D being Ordinal holds B <> succ D ; ::_thesis: C +^ A in C +^ B
then B is limit_ordinal by ORDINAL1:29;
then C +^ B = sup fi by A3, A9, Th29
.= sup (rng fi) ;
hence C +^ A in C +^ B by A10, Th19; ::_thesis: verum
end;
hence C +^ A in C +^ B by A4; ::_thesis: verum
end;
for B being Ordinal holds S1[B] from ORDINAL1:sch_2(A1);
hence ( A in B implies C +^ A in C +^ B ) ; ::_thesis: verum
end;
theorem Th33: :: ORDINAL2:33
for A, B, C being Ordinal st A c= B holds
C +^ A c= C +^ B
proof
let A, B, C be Ordinal; ::_thesis: ( A c= B implies C +^ A c= C +^ B )
assume A1: A c= B ; ::_thesis: C +^ A c= C +^ B
now__::_thesis:_(_A_<>_B_implies_C_+^_A_c=_C_+^_B_)
assume A <> B ; ::_thesis: C +^ A c= C +^ B
then A c< B by A1, XBOOLE_0:def_8;
then C +^ A in C +^ B by Th32, ORDINAL1:11;
hence C +^ A c= C +^ B by ORDINAL1:def_2; ::_thesis: verum
end;
hence C +^ A c= C +^ B ; ::_thesis: verum
end;
theorem Th34: :: ORDINAL2:34
for A, B, C being Ordinal st A c= B holds
A +^ C c= B +^ C
proof
let A, B, C be Ordinal; ::_thesis: ( A c= B implies A +^ C c= B +^ C )
defpred S1[ Ordinal] means A +^ $1 c= B +^ $1;
assume A1: A c= B ; ::_thesis: A +^ C c= B +^ C
A2: for C being Ordinal st ( for D being Ordinal st D in C holds
S1[D] ) holds
S1[C]
proof
let C be Ordinal; ::_thesis: ( ( for D being Ordinal st D in C holds
S1[D] ) implies S1[C] )
assume A3: for D being Ordinal st D in C holds
A +^ D c= B +^ D ; ::_thesis: S1[C]
A4: now__::_thesis:_(_ex_D_being_Ordinal_st_C_=_succ_D_implies_S1[C]_)
given D being Ordinal such that A5: C = succ D ; ::_thesis: S1[C]
A6: B +^ C = succ (B +^ D) by A5, Th28;
( A +^ D c= B +^ D & A +^ C = succ (A +^ D) ) by A3, A5, Th28, ORDINAL1:6;
hence S1[C] by A6, Th1; ::_thesis: verum
end;
A7: now__::_thesis:_(_C_<>_{}_&_(_for_D_being_Ordinal_holds_C_<>_succ_D_)_implies_S1[C]_)
deffunc H1( Ordinal) -> Ordinal = A +^ $1;
assume that
A8: C <> {} and
A9: for D being Ordinal holds C <> succ D ; ::_thesis: S1[C]
consider fi being Ordinal-Sequence such that
A10: ( dom fi = C & ( for D being Ordinal st D in C holds
fi . D = H1(D) ) ) from ORDINAL2:sch_3();
A11: now__::_thesis:_for_D_being_Ordinal_st_D_in_rng_fi_holds_
D_in_B_+^_C
let D be Ordinal; ::_thesis: ( D in rng fi implies D in B +^ C )
assume D in rng fi ; ::_thesis: D in B +^ C
then consider x being set such that
A12: x in dom fi and
A13: D = fi . x by FUNCT_1:def_3;
reconsider x = x as Ordinal by A12;
A14: B +^ x in B +^ C by A10, A12, Th32;
( D = A +^ x & A +^ x c= B +^ x ) by A3, A10, A12, A13;
hence D in B +^ C by A14, ORDINAL1:12; ::_thesis: verum
end;
C is limit_ordinal by A9, ORDINAL1:29;
then A +^ C = sup fi by A8, A10, Th29
.= sup (rng fi) ;
hence S1[C] by A11, Th20; ::_thesis: verum
end;
now__::_thesis:_(_C_=_{}_implies_S1[C]_)
assume A15: C = {} ; ::_thesis: S1[C]
then A +^ C = A by Th27;
hence S1[C] by A1, A15, Th27; ::_thesis: verum
end;
hence S1[C] by A4, A7; ::_thesis: verum
end;
for C being Ordinal holds S1[C] from ORDINAL1:sch_2(A2);
hence A +^ C c= B +^ C ; ::_thesis: verum
end;
theorem Th35: :: ORDINAL2:35
for A being Ordinal holds {} *^ A = {}
proof
let A be Ordinal; ::_thesis: {} *^ A = {}
deffunc H1( Ordinal, T-Sequence) -> set = union (sup $2);
deffunc H2( Ordinal) -> Ordinal = $1 *^ A;
deffunc H3( Ordinal, Ordinal) -> Ordinal = $2 +^ A;
A1: for B, C being Ordinal holds
( C = H2(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = {} & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H3(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) ) by Def15;
thus H2( {} ) = {} from ORDINAL2:sch_14(A1); ::_thesis: verum
end;
theorem Th36: :: ORDINAL2:36
for B, A being Ordinal holds (succ B) *^ A = (B *^ A) +^ A
proof
let B, A be Ordinal; ::_thesis: (succ B) *^ A = (B *^ A) +^ A
deffunc H1( Ordinal, T-Sequence) -> set = union (sup $2);
deffunc H2( Ordinal) -> Ordinal = $1 *^ A;
deffunc H3( Ordinal, Ordinal) -> Ordinal = $2 +^ A;
A1: for B, C being Ordinal holds
( C = H2(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = {} & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H3(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) ) by Def15;
for B being Ordinal holds H2( succ B) = H3(B,H2(B)) from ORDINAL2:sch_15(A1);
hence (succ B) *^ A = (B *^ A) +^ A ; ::_thesis: verum
end;
theorem Th37: :: ORDINAL2:37
for B, A being Ordinal st B <> {} & B is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = C *^ A ) holds
B *^ A = union (sup fi)
proof
let B, A be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal implies for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = C *^ A ) holds
B *^ A = union (sup fi) )
deffunc H1( Ordinal, Ordinal-Sequence) -> set = union (sup $2);
assume A1: ( B <> {} & B is limit_ordinal ) ; ::_thesis: for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = C *^ A ) holds
B *^ A = union (sup fi)
deffunc H2( Ordinal, Ordinal) -> Ordinal = $2 +^ A;
deffunc H3( Ordinal) -> Ordinal = $1 *^ A;
let fi be Ordinal-Sequence; ::_thesis: ( dom fi = B & ( for C being Ordinal st C in B holds
fi . C = C *^ A ) implies B *^ A = union (sup fi) )
assume that
A2: dom fi = B and
A3: for C being Ordinal st C in B holds
fi . C = H3(C) ; ::_thesis: B *^ A = union (sup fi)
A4: for B, C being Ordinal holds
( C = H3(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = {} & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) ) by Def15;
thus H3(B) = H1(B,fi) from ORDINAL2:sch_16(A4, A1, A2, A3); ::_thesis: verum
end;
theorem Th38: :: ORDINAL2:38
for A being Ordinal holds A *^ {} = {}
proof
let A be Ordinal; ::_thesis: A *^ {} = {}
defpred S1[ Ordinal] means $1 *^ {} = {} ;
A1: for A being Ordinal st S1[A] holds
S1[ succ A]
proof
let A be Ordinal; ::_thesis: ( S1[A] implies S1[ succ A] )
assume A *^ {} = {} ; ::_thesis: S1[ succ A]
hence (succ A) *^ {} = {} +^ {} by Th36
.= {} by Th27 ;
::_thesis: verum
end;
A2: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
deffunc H1( Ordinal) -> Ordinal = $1 *^ {};
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
A3: A <> {} and
A4: A is limit_ordinal and
A5: for B being Ordinal st B in A holds
B *^ {} = {} ; ::_thesis: S1[A]
consider fi being Ordinal-Sequence such that
A6: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H1(B) ) ) from ORDINAL2:sch_3();
rng fi = succ {}
proof
thus for x being set st x in rng fi holds
x in succ {} :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: succ {} c= rng fi
proof
let x be set ; ::_thesis: ( x in rng fi implies x in succ {} )
assume x in rng fi ; ::_thesis: x in succ {}
then consider y being set such that
A7: y in dom fi and
A8: x = fi . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A7;
x = y *^ {} by A6, A7, A8
.= {} by A5, A6, A7 ;
hence x in succ {} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in succ {} or x in rng fi )
assume x in succ {} ; ::_thesis: x in rng fi
then A9: x = {} by TARSKI:def_1;
{} c= A ;
then A10: {} c< A by A3, XBOOLE_0:def_8;
then A11: {} in A by ORDINAL1:11;
{} *^ {} = {} by Th35;
then fi . x = x by A6, A10, A9, ORDINAL1:11;
hence x in rng fi by A6, A11, A9, FUNCT_1:def_3; ::_thesis: verum
end;
then A12: sup (rng fi) = succ {} by Th18;
A *^ {} = union (sup fi) by A3, A4, A6, Th37
.= union (sup (rng fi)) ;
hence S1[A] by A12, Th2; ::_thesis: verum
end;
A13: S1[ {} ] by Th35;
for A being Ordinal holds S1[A] from ORDINAL2:sch_1(A13, A1, A2);
hence A *^ {} = {} ; ::_thesis: verum
end;
theorem Th39: :: ORDINAL2:39
for A being Ordinal holds
( 1 *^ A = A & A *^ 1 = A )
proof
let A be Ordinal; ::_thesis: ( 1 *^ A = A & A *^ 1 = A )
defpred S1[ Ordinal] means $1 *^ (succ {}) = $1;
thus 1 *^ A = ({} *^ A) +^ A by Lm1, Th36
.= {} +^ A by Th35
.= A by Th30 ; ::_thesis: A *^ 1 = A
A1: for A being Ordinal st ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume A2: for B being Ordinal st B in A holds
B *^ (succ {}) = B ; ::_thesis: S1[A]
A3: now__::_thesis:_(_A_<>_{}_&_(_for_B_being_Ordinal_holds_A_<>_succ_B_)_implies_A_*^_(succ_{})_=_A_)
deffunc H1( Ordinal) -> Ordinal = $1 *^ (succ {});
assume that
A4: A <> {} and
A5: for B being Ordinal holds A <> succ B ; ::_thesis: A *^ (succ {}) = A
consider fi being Ordinal-Sequence such that
A6: ( dom fi = A & ( for D being Ordinal st D in A holds
fi . D = H1(D) ) ) from ORDINAL2:sch_3();
A7: A = rng fi
proof
thus A c= rng fi :: according to XBOOLE_0:def_10 ::_thesis: rng fi c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in rng fi )
assume A8: x in A ; ::_thesis: x in rng fi
then reconsider B = x as Ordinal ;
x = B *^ (succ {}) by A2, A8
.= fi . x by A6, A8 ;
hence x in rng fi by A6, A8, FUNCT_1:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng fi or x in A )
assume x in rng fi ; ::_thesis: x in A
then consider y being set such that
A9: y in dom fi and
A10: x = fi . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A9;
fi . y = y *^ (succ {}) by A6, A9
.= y by A2, A6, A9 ;
hence x in A by A6, A9, A10; ::_thesis: verum
end;
A11: A is limit_ordinal by A5, ORDINAL1:29;
then A *^ (succ {}) = union (sup fi) by A4, A6, Th37
.= union (sup (rng fi)) ;
hence A *^ (succ {}) = union A by A7, Th18
.= A by A11, ORDINAL1:def_6 ;
::_thesis: verum
end;
now__::_thesis:_(_ex_B_being_Ordinal_st_A_=_succ_B_implies_A_*^_(succ_{})_=_A_)
given B being Ordinal such that A12: A = succ B ; ::_thesis: A *^ (succ {}) = A
thus A *^ (succ {}) = (B *^ (succ {})) +^ (succ {}) by A12, Th36
.= B +^ (succ {}) by A2, A12, ORDINAL1:6
.= succ (B +^ {}) by Th28
.= A by A12, Th27 ; ::_thesis: verum
end;
hence S1[A] by A3, Th35; ::_thesis: verum
end;
for A being Ordinal holds S1[A] from ORDINAL1:sch_2(A1);
hence A *^ 1 = A ; ::_thesis: verum
end;
theorem Th40: :: ORDINAL2:40
for C, A, B being Ordinal st C <> {} & A in B holds
A *^ C in B *^ C
proof
let C, A, B be Ordinal; ::_thesis: ( C <> {} & A in B implies A *^ C in B *^ C )
A1: {} c= C ;
defpred S1[ Ordinal] means ( A in $1 implies A *^ C in $1 *^ C );
assume C <> {} ; ::_thesis: ( not A in B or A *^ C in B *^ C )
then A2: {} c< C by A1, XBOOLE_0:def_8;
then A3: {} in C by ORDINAL1:11;
A4: for B being Ordinal st ( for D being Ordinal st D in B holds
S1[D] ) holds
S1[B]
proof
let B be Ordinal; ::_thesis: ( ( for D being Ordinal st D in B holds
S1[D] ) implies S1[B] )
assume that
A5: for D being Ordinal st D in B & A in D holds
A *^ C in D *^ C and
A6: A in B ; ::_thesis: A *^ C in B *^ C
A7: now__::_thesis:_(_ex_D_being_Ordinal_st_B_=_succ_D_implies_A_*^_C_in_B_*^_C_)
given D being Ordinal such that A8: B = succ D ; ::_thesis: A *^ C in B *^ C
A9: now__::_thesis:_(_A_in_D_implies_A_*^_C_in_B_*^_C_)
assume A in D ; ::_thesis: A *^ C in B *^ C
then A10: A *^ C in D *^ C by A5, A8, ORDINAL1:6;
A11: (D *^ C) +^ {} in (D *^ C) +^ C by A2, Th32, ORDINAL1:11;
( (D *^ C) +^ C = (succ D) *^ C & (D *^ C) +^ {} = D *^ C ) by Th27, Th36;
hence A *^ C in B *^ C by A8, A10, A11, ORDINAL1:10; ::_thesis: verum
end;
now__::_thesis:_(_not_A_in_D_implies_A_*^_C_in_B_*^_C_)
A12: (A *^ C) +^ {} = A *^ C by Th27;
assume A13: not A in D ; ::_thesis: A *^ C in B *^ C
( A c< D iff ( A c= D & A <> D ) ) by XBOOLE_0:def_8;
then (A *^ C) +^ {} in (D *^ C) +^ C by A3, A6, A8, A13, Th32, ORDINAL1:11, ORDINAL1:22;
hence A *^ C in B *^ C by A8, A12, Th36; ::_thesis: verum
end;
hence A *^ C in B *^ C by A9; ::_thesis: verum
end;
now__::_thesis:_(_(_for_D_being_Ordinal_holds_B_<>_succ_D_)_implies_A_*^_C_in_B_*^_C_)
A14: ( (A *^ C) +^ {} = A *^ C & (A *^ C) +^ {} in (A *^ C) +^ C ) by A2, Th27, Th32, ORDINAL1:11;
A15: (succ A) *^ C = (A *^ C) +^ C by Th36;
deffunc H1( Ordinal) -> Ordinal = $1 *^ C;
consider fi being Ordinal-Sequence such that
A16: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H1(D) ) ) from ORDINAL2:sch_3();
assume for D being Ordinal holds B <> succ D ; ::_thesis: A *^ C in B *^ C
then A17: B is limit_ordinal by ORDINAL1:29;
then A18: succ A in B by A6, ORDINAL1:28;
then fi . (succ A) = (succ A) *^ C by A16;
then (succ A) *^ C in rng fi by A16, A18, FUNCT_1:def_3;
then A19: (succ A) *^ C c= union (sup (rng fi)) by Th19, ZFMISC_1:74;
B *^ C = union (sup fi) by A6, A17, A16, Th37
.= union (sup (rng fi)) ;
hence A *^ C in B *^ C by A19, A14, A15; ::_thesis: verum
end;
hence A *^ C in B *^ C by A7; ::_thesis: verum
end;
for B being Ordinal holds S1[B] from ORDINAL1:sch_2(A4);
hence ( not A in B or A *^ C in B *^ C ) ; ::_thesis: verum
end;
theorem :: ORDINAL2:41
for A, B, C being Ordinal st A c= B holds
A *^ C c= B *^ C
proof
let A, B, C be Ordinal; ::_thesis: ( A c= B implies A *^ C c= B *^ C )
assume A1: A c= B ; ::_thesis: A *^ C c= B *^ C
A2: now__::_thesis:_(_C_<>_{}_implies_A_*^_C_c=_B_*^_C_)
assume A3: C <> {} ; ::_thesis: A *^ C c= B *^ C
now__::_thesis:_(_A_<>_B_implies_A_*^_C_c=_B_*^_C_)
assume A <> B ; ::_thesis: A *^ C c= B *^ C
then A c< B by A1, XBOOLE_0:def_8;
then A *^ C in B *^ C by A3, Th40, ORDINAL1:11;
hence A *^ C c= B *^ C by ORDINAL1:def_2; ::_thesis: verum
end;
hence A *^ C c= B *^ C ; ::_thesis: verum
end;
now__::_thesis:_(_C_=_{}_implies_A_*^_C_c=_B_*^_C_)
assume C = {} ; ::_thesis: A *^ C c= B *^ C
then A *^ C = {} by Th38;
hence A *^ C c= B *^ C ; ::_thesis: verum
end;
hence A *^ C c= B *^ C by A2; ::_thesis: verum
end;
theorem :: ORDINAL2:42
for A, B, C being Ordinal st A c= B holds
C *^ A c= C *^ B
proof
let A, B, C be Ordinal; ::_thesis: ( A c= B implies C *^ A c= C *^ B )
assume A1: A c= B ; ::_thesis: C *^ A c= C *^ B
now__::_thesis:_(_B_<>_{}_implies_C_*^_A_c=_C_*^_B_)
defpred S1[ Ordinal] means $1 *^ A c= $1 *^ B;
assume A2: B <> {} ; ::_thesis: C *^ A c= C *^ B
A3: for C being Ordinal st ( for D being Ordinal st D in C holds
S1[D] ) holds
S1[C]
proof
let C be Ordinal; ::_thesis: ( ( for D being Ordinal st D in C holds
S1[D] ) implies S1[C] )
assume A4: for D being Ordinal st D in C holds
D *^ A c= D *^ B ; ::_thesis: S1[C]
A5: now__::_thesis:_(_ex_D_being_Ordinal_st_C_=_succ_D_implies_S1[C]_)
given D being Ordinal such that A6: C = succ D ; ::_thesis: S1[C]
D *^ A c= D *^ B by A4, A6, ORDINAL1:6;
then A7: (D *^ A) +^ A c= (D *^ B) +^ A by Th34;
A8: ( C *^ A = (D *^ A) +^ A & C *^ B = (D *^ B) +^ B ) by A6, Th36;
(D *^ B) +^ A c= (D *^ B) +^ B by A1, Th33;
hence S1[C] by A7, A8, XBOOLE_1:1; ::_thesis: verum
end;
A9: now__::_thesis:_(_C_<>_{}_&_(_for_D_being_Ordinal_holds_C_<>_succ_D_)_implies_S1[C]_)
deffunc H1( Ordinal) -> Ordinal = $1 *^ A;
assume that
A10: C <> {} and
A11: for D being Ordinal holds C <> succ D ; ::_thesis: S1[C]
consider fi being Ordinal-Sequence such that
A12: ( dom fi = C & ( for D being Ordinal st D in C holds
fi . D = H1(D) ) ) from ORDINAL2:sch_3();
now__::_thesis:_for_D_being_Ordinal_st_D_in_rng_fi_holds_
D_in_C_*^_B
let D be Ordinal; ::_thesis: ( D in rng fi implies D in C *^ B )
assume D in rng fi ; ::_thesis: D in C *^ B
then consider x being set such that
A13: x in dom fi and
A14: D = fi . x by FUNCT_1:def_3;
reconsider x = x as Ordinal by A13;
A15: x *^ B in C *^ B by A2, A12, A13, Th40;
( D = x *^ A & x *^ A c= x *^ B ) by A4, A12, A13, A14;
hence D in C *^ B by A15, ORDINAL1:12; ::_thesis: verum
end;
then A16: sup (rng fi) c= C *^ B by Th20;
C is limit_ordinal by A11, ORDINAL1:29;
then A17: C *^ A = union (sup fi) by A10, A12, Th37
.= union (sup (rng fi)) ;
union (sup (rng fi)) c= sup (rng fi) by Th5;
hence S1[C] by A17, A16, XBOOLE_1:1; ::_thesis: verum
end;
now__::_thesis:_(_C_=_{}_implies_S1[C]_)
assume C = {} ; ::_thesis: S1[C]
then C *^ A = {} by Th35;
hence S1[C] ; ::_thesis: verum
end;
hence S1[C] by A5, A9; ::_thesis: verum
end;
for C being Ordinal holds S1[C] from ORDINAL1:sch_2(A3);
hence C *^ A c= C *^ B ; ::_thesis: verum
end;
hence C *^ A c= C *^ B by A1; ::_thesis: verum
end;
theorem Th43: :: ORDINAL2:43
for A being Ordinal holds exp (A,{}) = 1
proof
let A be Ordinal; ::_thesis: exp (A,{}) = 1
deffunc H1( Ordinal, Ordinal-Sequence) -> Ordinal = lim $2;
deffunc H2( Ordinal) -> Ordinal = exp (A,$1);
deffunc H3( Ordinal, Ordinal) -> Ordinal = A *^ $2;
A1: for B, C being Ordinal holds
( C = H2(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H3(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) ) by Def16;
thus H2( {} ) = 1 from ORDINAL2:sch_14(A1); ::_thesis: verum
end;
theorem Th44: :: ORDINAL2:44
for A, B being Ordinal holds exp (A,(succ B)) = A *^ (exp (A,B))
proof
let A, B be Ordinal; ::_thesis: exp (A,(succ B)) = A *^ (exp (A,B))
deffunc H1( Ordinal, Ordinal-Sequence) -> Ordinal = lim $2;
deffunc H2( Ordinal) -> Ordinal = exp (A,$1);
deffunc H3( Ordinal, Ordinal) -> Ordinal = A *^ $2;
A1: for B, C being Ordinal holds
( C = H2(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H3(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) ) by Def16;
for B being Ordinal holds H2( succ B) = H3(B,H2(B)) from ORDINAL2:sch_15(A1);
hence exp (A,(succ B)) = A *^ (exp (A,B)) ; ::_thesis: verum
end;
theorem Th45: :: ORDINAL2:45
for B, A being Ordinal st B <> {} & B is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = exp (A,C) ) holds
exp (A,B) = lim fi
proof
let B, A be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal implies for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = exp (A,C) ) holds
exp (A,B) = lim fi )
deffunc H1( Ordinal, Ordinal-Sequence) -> Ordinal = lim $2;
assume A1: ( B <> {} & B is limit_ordinal ) ; ::_thesis: for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = exp (A,C) ) holds
exp (A,B) = lim fi
deffunc H2( Ordinal, Ordinal) -> Ordinal = A *^ $2;
deffunc H3( Ordinal) -> Ordinal = exp (A,$1);
let fi be Ordinal-Sequence; ::_thesis: ( dom fi = B & ( for C being Ordinal st C in B holds
fi . C = exp (A,C) ) implies exp (A,B) = lim fi )
assume that
A2: dom fi = B and
A3: for C being Ordinal st C in B holds
fi . C = H3(C) ; ::_thesis: exp (A,B) = lim fi
A4: for B, C being Ordinal holds
( C = H3(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) ) by Def16;
thus H3(B) = H1(B,fi) from ORDINAL2:sch_16(A4, A1, A2, A3); ::_thesis: verum
end;
theorem :: ORDINAL2:46
for A being Ordinal holds
( exp (A,1) = A & exp (1,A) = 1 )
proof
let A be Ordinal; ::_thesis: ( exp (A,1) = A & exp (1,A) = 1 )
defpred S1[ Ordinal] means exp (1,$1) = 1;
A1: for A being Ordinal st S1[A] holds
S1[ succ A]
proof
let A be Ordinal; ::_thesis: ( S1[A] implies S1[ succ A] )
assume exp (1,A) = 1 ; ::_thesis: S1[ succ A]
hence exp (1,(succ A)) = 1 *^ 1 by Th44
.= 1 by Th39 ;
::_thesis: verum
end;
thus exp (A,1) = A *^ (exp (A,{})) by Lm1, Th44
.= A *^ 1 by Th43
.= A by Th39 ; ::_thesis: exp (1,A) = 1
A2: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
deffunc H1( Ordinal) -> Ordinal = exp (1,$1);
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
A3: A <> {} and
A4: A is limit_ordinal and
A5: for B being Ordinal st B in A holds
exp (1,B) = 1 ; ::_thesis: S1[A]
consider fi being Ordinal-Sequence such that
A6: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H1(B) ) ) from ORDINAL2:sch_3();
A7: rng fi c= {1}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng fi or x in {1} )
assume x in rng fi ; ::_thesis: x in {1}
then consider y being set such that
A8: y in dom fi and
A9: x = fi . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A8;
x = exp (1,y) by A6, A8, A9
.= 1 by A5, A6, A8 ;
hence x in {1} by TARSKI:def_1; ::_thesis: verum
end;
now__::_thesis:_(_{}_<>_1_&_(_for_B,_C_being_Ordinal_st_B_in_1_&_1_in_C_holds_
ex_D_being_Ordinal_st_
(_D_in_dom_fi_&_(_for_E_being_Ordinal_st_D_c=_E_&_E_in_dom_fi_holds_
(_B_in_fi_._E_&_fi_._E_in_C_)_)_)_)_)
set x = the Element of A;
thus {} <> 1 ; ::_thesis: for B, C being Ordinal st B in 1 & 1 in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) )
let B, C be Ordinal; ::_thesis: ( B in 1 & 1 in C implies ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) ) )
assume A10: ( B in 1 & 1 in C ) ; ::_thesis: ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) )
reconsider x = the Element of A as Ordinal ;
take D = x; ::_thesis: ( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) )
thus D in dom fi by A3, A6; ::_thesis: for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C )
let E be Ordinal; ::_thesis: ( D c= E & E in dom fi implies ( B in fi . E & fi . E in C ) )
assume that
D c= E and
A11: E in dom fi ; ::_thesis: ( B in fi . E & fi . E in C )
fi . E in rng fi by A11, FUNCT_1:def_3;
hence ( B in fi . E & fi . E in C ) by A7, A10, TARSKI:def_1; ::_thesis: verum
end;
then A12: 1 is_limes_of fi by Def9;
exp (1,A) = lim fi by A3, A4, A6, Th45;
hence S1[A] by A12, Def10; ::_thesis: verum
end;
A13: S1[ {} ] by Th43;
for A being Ordinal holds S1[A] from ORDINAL2:sch_1(A13, A1, A2);
hence exp (1,A) = 1 ; ::_thesis: verum
end;
theorem :: ORDINAL2:47
for A being Ordinal ex B, C being Ordinal st
( B is limit_ordinal & C is natural & A = B +^ C )
proof
defpred S1[ Ordinal] means ex B, C being Ordinal st
( B is limit_ordinal & C is natural & $1 = B +^ C );
A1: for A being Ordinal st ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume A2: for B being Ordinal st B in A holds
S1[B] ; ::_thesis: S1[A]
A3: ( ex B being Ordinal st A = succ B implies S1[A] )
proof
given B being Ordinal such that A4: A = succ B ; ::_thesis: S1[A]
consider C, D being Ordinal such that
A5: C is limit_ordinal and
A6: D is natural and
A7: B = C +^ D by A2, A4, ORDINAL1:6;
take C ; ::_thesis: ex C being Ordinal st
( C is limit_ordinal & C is natural & A = C +^ C )
take E = succ D; ::_thesis: ( C is limit_ordinal & E is natural & A = C +^ E )
thus C is limit_ordinal by A5; ::_thesis: ( E is natural & A = C +^ E )
thus E in omega by A6, ORDINAL1:def_12; :: according to ORDINAL1:def_12 ::_thesis: A = C +^ E
thus A = C +^ E by A4, A7, Th28; ::_thesis: verum
end;
( ( for B being Ordinal holds A <> succ B ) implies S1[A] )
proof
assume A8: for D being Ordinal holds A <> succ D ; ::_thesis: S1[A]
take B = A; ::_thesis: ex C being Ordinal st
( B is limit_ordinal & C is natural & A = B +^ C )
take C = {} ; ::_thesis: ( B is limit_ordinal & C is natural & A = B +^ C )
thus B is limit_ordinal by A8, ORDINAL1:29; ::_thesis: ( C is natural & A = B +^ C )
thus C in omega by ORDINAL1:def_11; :: according to ORDINAL1:def_12 ::_thesis: A = B +^ C
thus A = B +^ C by Th27; ::_thesis: verum
end;
hence S1[A] by A3; ::_thesis: verum
end;
thus for A being Ordinal holds S1[A] from ORDINAL1:sch_2(A1); ::_thesis: verum
end;
registration
let X be set ;
let o be Ordinal;
clusterX --> o -> Ordinal-yielding ;
coherence
X --> o is Ordinal-yielding
proof
( rng (X --> o) c= {o} & {o} c= succ o ) by FUNCOP_1:13, XBOOLE_1:7;
then rng (X --> o) c= succ o by XBOOLE_1:1;
hence X --> o is Ordinal-yielding by Def4; ::_thesis: verum
end;
end;
registration
let O be Ordinal;
let x be set ;
clusterO --> x -> T-Sequence-like ;
coherence
O --> x is T-Sequence-like
proof
dom (O --> x) = O by FUNCOP_1:13;
hence O --> x is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum
end;
end;
definition
let A, B be Ordinal;
predA is_cofinal_with B means :: ORDINAL2:def 17
ex xi being Ordinal-Sequence st
( dom xi = B & rng xi c= A & xi is increasing & A = sup xi );
reflexivity
for A being Ordinal ex xi being Ordinal-Sequence st
( dom xi = A & rng xi c= A & xi is increasing & A = sup xi )
proof
let A be Ordinal; ::_thesis: ex xi being Ordinal-Sequence st
( dom xi = A & rng xi c= A & xi is increasing & A = sup xi )
A1: dom (id A) = A by RELAT_1:45;
then reconsider xi = id A as T-Sequence by ORDINAL1:def_7;
A2: rng (id A) = A by RELAT_1:45;
then reconsider xi = xi as Ordinal-Sequence by Def4;
take xi ; ::_thesis: ( dom xi = A & rng xi c= A & xi is increasing & A = sup xi )
thus ( dom xi = A & rng xi c= A ) by RELAT_1:45; ::_thesis: ( xi is increasing & A = sup xi )
thus xi is increasing ::_thesis: A = sup xi
proof
let B be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for B being Ordinal st B in B & B in dom xi holds
xi . B in xi . B
let C be Ordinal; ::_thesis: ( B in C & C in dom xi implies xi . B in xi . C )
assume that
A3: B in C and
A4: C in dom xi ; ::_thesis: xi . B in xi . C
xi . C = C by A1, A4, FUNCT_1:18;
hence xi . B in xi . C by A1, A3, A4, FUNCT_1:18, ORDINAL1:10; ::_thesis: verum
end;
thus A = sup xi by A2, Th18; ::_thesis: verum
end;
end;
:: deftheorem defines is_cofinal_with ORDINAL2:def_17_:_
for A, B being Ordinal holds
( A is_cofinal_with B iff ex xi being Ordinal-Sequence st
( dom xi = B & rng xi c= A & xi is increasing & A = sup xi ) );
theorem Th48: :: ORDINAL2:48
for psi being Ordinal-Sequence
for e being set st e in rng psi holds
e is Ordinal
proof
let psi be Ordinal-Sequence; ::_thesis: for e being set st e in rng psi holds
e is Ordinal
let e be set ; ::_thesis: ( e in rng psi implies e is Ordinal )
assume e in rng psi ; ::_thesis: e is Ordinal
then ex u being set st
( u in dom psi & e = psi . u ) by FUNCT_1:def_3;
hence e is Ordinal ; ::_thesis: verum
end;
theorem :: ORDINAL2:49
for psi being Ordinal-Sequence holds rng psi c= sup psi
proof
let psi be Ordinal-Sequence; ::_thesis: rng psi c= sup psi
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng psi or e in sup psi )
assume A1: e in rng psi ; ::_thesis: e in sup psi
then e is Ordinal by Th48;
hence e in sup psi by A1, Th19; ::_thesis: verum
end;
theorem :: ORDINAL2:50
for A being Ordinal st A is_cofinal_with {} holds
A = {}
proof
let A be Ordinal; ::_thesis: ( A is_cofinal_with {} implies A = {} )
given psi being Ordinal-Sequence such that A1: dom psi = {} and
rng psi c= A and
psi is increasing and
A2: A = sup psi ; :: according to ORDINAL2:def_17 ::_thesis: A = {}
thus A = sup {} by A1, A2, RELAT_1:42
.= {} by Th18 ; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 17
OmegaInd{ F1() -> Nat, P1[ set ] } :
P1[F1()]
provided
A1: P1[ {} ] and
A2: for a being Nat st P1[a] holds
P1[ succ a]
proof
defpred S1[ Ordinal] means ( $1 is natural implies P1[$1] );
A3: now__::_thesis:_for_A_being_Ordinal_st_S1[A]_holds_
S1[_succ_A]
let A be Ordinal; ::_thesis: ( S1[A] implies S1[ succ A] )
assume A4: S1[A] ; ::_thesis: S1[ succ A]
now__::_thesis:_(_succ_A_is_natural_implies_S1[_succ_A]_)
assume succ A is natural ; ::_thesis: S1[ succ A]
then A5: succ A in omega by ORDINAL1:def_12;
A in succ A by ORDINAL1:6;
then A is Element of omega by A5, ORDINAL1:10;
hence S1[ succ A] by A2, A4; ::_thesis: verum
end;
hence S1[ succ A] ; ::_thesis: verum
end;
A6: now__::_thesis:_for_A_being_Ordinal_st_A_<>_{}_&_A_is_limit_ordinal_&_(_for_B_being_Ordinal_st_B_in_A_holds_
S1[B]_)_holds_
S1[A]
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume A7: A <> {} ; ::_thesis: ( A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
{} c= A ;
then {} c< A by A7, XBOOLE_0:def_8;
then A8: {} in A by ORDINAL1:11;
A9: not A in A ;
assume A is limit_ordinal ; ::_thesis: ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
then omega c= A by A8, ORDINAL1:def_11;
then not A in omega by A9;
hence ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] ) by ORDINAL1:def_12; ::_thesis: verum
end;
A10: S1[ {} ] by A1;
for A being Ordinal holds S1[A] from ORDINAL2:sch_1(A10, A3, A6);
hence P1[F1()] ; ::_thesis: verum
end;
registration
let a, b be Nat;
clustera +^ b -> natural ;
coherence
a +^ b is natural
proof
defpred S1[ Nat] means a +^ a is natural ;
A1: now__::_thesis:_for_b_being_Nat_st_S1[b]_holds_
S1[_succ_b]
let b be Nat; ::_thesis: ( S1[b] implies S1[ succ b] )
assume S1[b] ; ::_thesis: S1[ succ b]
then reconsider c = a +^ b as Nat ;
a +^ (succ b) = succ c by Th28;
hence S1[ succ b] ; ::_thesis: verum
end;
A2: S1[ {} ] by Th27;
thus S1[b] from ORDINAL2:sch_17(A2, A1); ::_thesis: verum
end;
end;
registration
let x, y be set ;
let a, b be Nat;
cluster IFEQ (x,y,a,b) -> natural ;
coherence
IFEQ (x,y,a,b) is natural
proof
percases ( x = y or x <> y ) ;
suppose x = y ; ::_thesis: IFEQ (x,y,a,b) is natural
hence IFEQ (x,y,a,b) is natural by FUNCOP_1:def_8; ::_thesis: verum
end;
suppose x <> y ; ::_thesis: IFEQ (x,y,a,b) is natural
hence IFEQ (x,y,a,b) is natural by FUNCOP_1:def_8; ::_thesis: verum
end;
end;
end;
end;
scheme :: ORDINAL2:sch 18
LambdaRecEx{ F1() -> set , F2( set , set ) -> set } :
ex f being Function st
( dom f = omega & f . {} = F1() & ( for n being Nat holds f . (succ n) = F2(n,(f . n)) ) )
proof
deffunc H1( set , set ) -> set = {} ;
consider L being T-Sequence such that
A1: dom L = omega and
A2: ( {} in omega implies L . {} = F1() ) and
A3: for A being Ordinal st succ A in omega holds
L . (succ A) = F2(A,(L . A)) and
for A being Ordinal st A in omega & A <> {} & A is limit_ordinal holds
L . A = H1(A,L | A) from ORDINAL2:sch_5();
take L ; ::_thesis: ( dom L = omega & L . {} = F1() & ( for n being Nat holds L . (succ n) = F2(n,(L . n)) ) )
thus dom L = omega by A1; ::_thesis: ( L . {} = F1() & ( for n being Nat holds L . (succ n) = F2(n,(L . n)) ) )
{} in omega by ORDINAL1:def_12;
hence L . {} = F1() by A2; ::_thesis: for n being Nat holds L . (succ n) = F2(n,(L . n))
let n be Nat; ::_thesis: L . (succ n) = F2(n,(L . n))
succ n in omega by ORDINAL1:def_12;
hence L . (succ n) = F2(n,(L . n)) by A3; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 19
RecUn{ F1() -> set , F2() -> Function, F3() -> Function, P1[ set , set , set ] } :
F2() = F3()
provided
A1: dom F2() = omega and
A2: F2() . {} = F1() and
A3: for n being Nat holds P1[n,F2() . n,F2() . (succ n)] and
A4: dom F3() = omega and
A5: F3() . {} = F1() and
A6: for n being Nat holds P1[n,F3() . n,F3() . (succ n)] and
A7: for n being Nat
for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
proof
defpred S1[ Nat] means F2() . $1 = F3() . $1;
A8: for n being Nat st S1[n] holds
S1[ succ n]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[ succ n] )
assume F2() . n = F3() . n ; ::_thesis: S1[ succ n]
then A9: P1[n,F2() . n,F3() . (succ n)] by A6;
P1[n,F2() . n,F2() . (succ n)] by A3;
hence S1[ succ n] by A7, A9; ::_thesis: verum
end;
A10: S1[ {} ] by A2, A5;
for n being Nat holds S1[n]
proof
let n be Nat; ::_thesis: S1[n]
thus S1[n] from ORDINAL2:sch_17(A10, A8); ::_thesis: verum
end;
then for x being set st x in omega holds
F2() . x = F3() . x ;
hence F2() = F3() by A1, A4, FUNCT_1:2; ::_thesis: verum
end;
scheme :: ORDINAL2:sch 20
LambdaRecUn{ F1() -> set , F2( set , set ) -> set , F3() -> Function, F4() -> Function } :
F3() = F4()
provided
A1: dom F3() = omega and
A2: F3() . {} = F1() and
A3: for n being Nat holds F3() . (succ n) = F2(n,(F3() . n)) and
A4: dom F4() = omega and
A5: F4() . {} = F1() and
A6: for n being Nat holds F4() . (succ n) = F2(n,(F4() . n))
proof
defpred S1[ Nat, set , set ] means $3 = F2($1,$2);
A7: for n being Nat holds S1[n,F4() . n,F4() . (succ n)] by A6;
A8: for n being Nat
for x, y1, y2 being set st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2 ;
A9: for n being Nat holds S1[n,F3() . n,F3() . (succ n)] by A3;
thus F3() = F4() from ORDINAL2:sch_19(A1, A2, A9, A4, A5, A7, A8); ::_thesis: verum
end;