:: ORDINAL1 semantic presentation
begin
theorem :: ORDINAL1:1
canceled;
theorem :: ORDINAL1:2
canceled;
theorem :: ORDINAL1:3
canceled;
theorem :: ORDINAL1:4
canceled;
theorem Th5: :: ORDINAL1:5
for Y, X being set st Y in X holds
not X c= Y
proof
let Y, X be set ; ::_thesis: ( Y in X implies not X c= Y )
assume A1: Y in X ; ::_thesis: not X c= Y
assume X c= Y ; ::_thesis: contradiction
then Y in Y by A1;
hence contradiction ; ::_thesis: verum
end;
definition
let X be set ;
func succ X -> set equals :: ORDINAL1:def 1
X \/ {X};
coherence
X \/ {X} is set ;
end;
:: deftheorem defines succ ORDINAL1:def_1_:_
for X being set holds succ X = X \/ {X};
registration
let X be set ;
cluster succ X -> non empty ;
coherence
not succ X is empty ;
end;
theorem Th6: :: ORDINAL1:6
for X being set holds X in succ X
proof
let X be set ; ::_thesis: X in succ X
X in {X} by TARSKI:def_1;
hence X in succ X by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem :: ORDINAL1:7
for X, Y being set st succ X = succ Y holds
X = Y
proof
let X, Y be set ; ::_thesis: ( succ X = succ Y implies X = Y )
assume that
A1: succ X = succ Y and
A2: X <> Y ; ::_thesis: contradiction
Y in X \/ {X} by A1, Th6;
then A3: ( Y in X or Y in {X} ) by XBOOLE_0:def_3;
X in Y \/ {Y} by A1, Th6;
then ( X in Y or X in {Y} ) by XBOOLE_0:def_3;
hence contradiction by A2, A3, TARSKI:def_1; ::_thesis: verum
end;
theorem Th8: :: ORDINAL1:8
for x, X being set holds
( x in succ X iff ( x in X or x = X ) )
proof
let x, X be set ; ::_thesis: ( x in succ X iff ( x in X or x = X ) )
thus ( not x in succ X or x in X or x = X ) ::_thesis: ( ( x in X or x = X ) implies x in succ X )
proof
assume x in succ X ; ::_thesis: ( x in X or x = X )
then ( x in X or x in {X} ) by XBOOLE_0:def_3;
hence ( x in X or x = X ) by TARSKI:def_1; ::_thesis: verum
end;
assume ( x in X or x = X ) ; ::_thesis: x in succ X
then ( x in X or x in {X} ) by TARSKI:def_1;
hence x in succ X by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th9: :: ORDINAL1:9
for X being set holds X <> succ X
proof
let X be set ; ::_thesis: X <> succ X
assume A1: X = succ X ; ::_thesis: contradiction
X in succ X by Th6;
hence contradiction by A1; ::_thesis: verum
end;
definition
let X be set ;
attrX is epsilon-transitive means :Def2: :: ORDINAL1:def 2
for x being set st x in X holds
x c= X;
attrX is epsilon-connected means :Def3: :: ORDINAL1:def 3
for x, y being set st x in X & y in X & not x in y & not x = y holds
y in x;
end;
:: deftheorem Def2 defines epsilon-transitive ORDINAL1:def_2_:_
for X being set holds
( X is epsilon-transitive iff for x being set st x in X holds
x c= X );
:: deftheorem Def3 defines epsilon-connected ORDINAL1:def_3_:_
for X being set holds
( X is epsilon-connected iff for x, y being set st x in X & y in X & not x in y & not x = y holds
y in x );
Lm1: ( {} is epsilon-transitive & {} is epsilon-connected )
proof
thus for x being set st x in {} holds
x c= {} ; :: according to ORDINAL1:def_2 ::_thesis: {} is epsilon-connected
thus for x, y being set st x in {} & y in {} & not x in y & not x = y holds
y in x ; :: according to ORDINAL1:def_3 ::_thesis: verum
end;
definition
let IT be set ;
attrIT is ordinal means :Def4: :: ORDINAL1:def 4
( IT is epsilon-transitive & IT is epsilon-connected );
end;
:: deftheorem Def4 defines ordinal ORDINAL1:def_4_:_
for IT being set holds
( IT is ordinal iff ( IT is epsilon-transitive & IT is epsilon-connected ) );
registration
cluster ordinal -> epsilon-transitive epsilon-connected for number ;
coherence
for b1 being set st b1 is ordinal holds
( b1 is epsilon-transitive & b1 is epsilon-connected ) by Def4;
cluster epsilon-transitive epsilon-connected -> ordinal for number ;
coherence
for b1 being set st b1 is epsilon-transitive & b1 is epsilon-connected holds
b1 is ordinal by Def4;
end;
notation
synonym number for set ;
end;
registration
cluster ordinal for number ;
existence
ex b1 being number st b1 is ordinal by Lm1;
end;
definition
mode Ordinal is ordinal number ;
end;
theorem Th10: :: ORDINAL1:10
for A, B being set
for C being epsilon-transitive set st A in B & B in C holds
A in C
proof
let A, B be set ; ::_thesis: for C being epsilon-transitive set st A in B & B in C holds
A in C
let C be epsilon-transitive set ; ::_thesis: ( A in B & B in C implies A in C )
assume that
A1: A in B and
A2: B in C ; ::_thesis: A in C
B c= C by A2, Def2;
hence A in C by A1; ::_thesis: verum
end;
theorem Th11: :: ORDINAL1:11
for x being epsilon-transitive set
for A being Ordinal st x c< A holds
x in A
proof
let x be epsilon-transitive set ; ::_thesis: for A being Ordinal st x c< A holds
x in A
let A be Ordinal; ::_thesis: ( x c< A implies x in A )
set a = the Element of A \ x;
assume A1: x c< A ; ::_thesis: x in A
then A2: x c= A by XBOOLE_0:def_8;
A \ x <> {}
proof
assume A \ x = {} ; ::_thesis: contradiction
then A c= x by XBOOLE_1:37;
hence contradiction by A1, XBOOLE_1:60; ::_thesis: verum
end;
then the Element of A \ x in A \ x ;
then consider y being set such that
A3: y in A \ x and
A4: for a being set holds
( not a in A \ x or not a in y ) by TARSKI:2;
A5: not y in x by A3, XBOOLE_0:def_5;
now__::_thesis:_for_a_being_set_st_a_in_x_holds_
a_in_y
let a be set ; ::_thesis: ( a in x implies a in y )
assume a in x ; ::_thesis: a in y
then consider z being set such that
A6: z = a and
A7: z in x ;
z c= x by A7, Def2;
then not y in z by A3, XBOOLE_0:def_5;
hence a in y by A2, A3, A5, A6, A7, Def3; ::_thesis: verum
end;
then A8: x c= y by TARSKI:def_3;
A9: y c= A by A3, Def2;
now__::_thesis:_for_a_being_set_st_a_in_y_holds_
a_in_x
let a be set ; ::_thesis: ( a in y implies a in x )
assume A10: a in y ; ::_thesis: a in x
then not a in A \ x by A4;
hence a in x by A9, A10, XBOOLE_0:def_5; ::_thesis: verum
end;
then A11: y c= x by TARSKI:def_3;
y in A by A3;
hence x in A by A11, A8, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: ORDINAL1:12
for A being epsilon-transitive set
for B, C being Ordinal st A c= B & B in C holds
A in C
proof
let A be epsilon-transitive set ; ::_thesis: for B, C being Ordinal st A c= B & B in C holds
A in C
let B, C be Ordinal; ::_thesis: ( A c= B & B in C implies A in C )
assume that
A1: A c= B and
A2: B in C ; ::_thesis: A in C
B c= C by A2, Def2;
then A3: A c= C by A1, XBOOLE_1:1;
A <> C by A1, A2, Th5;
then A c< C by A3, XBOOLE_0:def_8;
hence A in C by Th11; ::_thesis: verum
end;
theorem Th13: :: ORDINAL1:13
for a being set
for A being Ordinal st a in A holds
a is Ordinal
proof
let a be set ; ::_thesis: for A being Ordinal st a in A holds
a is Ordinal
let A be Ordinal; ::_thesis: ( a in A implies a is Ordinal )
assume A1: a in A ; ::_thesis: a is Ordinal
then A2: a c= A by Def2;
now__::_thesis:_for_y_being_set_st_y_in_a_holds_
y_c=_a
let y be set ; ::_thesis: ( y in a implies y c= a )
assume A3: y in a ; ::_thesis: y c= a
then A4: y c= A by A2, Def2;
assume not y c= a ; ::_thesis: contradiction
then consider b being set such that
A5: ( b in y & not b in a ) by TARSKI:def_3;
b in y \ a by A5, XBOOLE_0:def_5;
then consider z being set such that
A6: z in y \ a and
for c being set holds
( not c in y \ a or not c in z ) by TARSKI:2;
z in y by A6;
then ( z in a or z = a or a in z ) by A1, A4, Def3;
hence contradiction by A3, A6, XREGULAR:7, XBOOLE_0:def_5; ::_thesis: verum
end;
then A7: a is epsilon-transitive by Def2;
for y, z being set st y in a & z in a & not y in z & not y = z holds
z in y by A2, Def3;
then a is epsilon-connected by Def3;
hence a is Ordinal by A7; ::_thesis: verum
end;
theorem Th14: :: ORDINAL1:14
for A, B being Ordinal holds
( A in B or A = B or B in A )
proof
let A, B be Ordinal; ::_thesis: ( A in B or A = B or B in A )
assume that
A1: not A in B and
A2: A <> B ; ::_thesis: B in A
not A c< B by A1, Th11;
then not A c= B by A2, XBOOLE_0:def_8;
then consider a being set such that
A3: ( a in A & not a in B ) by TARSKI:def_3;
a in A \ B by A3, XBOOLE_0:def_5;
then consider X being set such that
A4: X in A \ B and
A5: for a being set holds
( not a in A \ B or not a in X ) by TARSKI:2;
A6: X c= A by A4, Def2;
now__::_thesis:_for_b_being_set_st_b_in_X_holds_
b_in_B
let b be set ; ::_thesis: ( b in X implies b in B )
assume A7: b in X ; ::_thesis: b in B
then not b in A \ B by A5;
hence b in B by A6, A7, XBOOLE_0:def_5; ::_thesis: verum
end;
then X c= B by TARSKI:def_3;
then A8: ( X c< B or X = B ) by XBOOLE_0:def_8;
( not X in B & X is Ordinal ) by A4, Th13, XBOOLE_0:def_5;
hence B in A by A4, A8, Th11; ::_thesis: verum
end;
definition
let A, B be Ordinal;
:: original: c=
redefine predA c= B means :: ORDINAL1:def 5
for C being Ordinal st C in A holds
C in B;
compatibility
( A c= B iff for C being Ordinal st C in A holds
C in B )
proof
thus ( A c= B implies for C being Ordinal st C in A holds
C in B ) ; ::_thesis: ( ( for C being Ordinal st C in A holds
C in B ) implies A c= B )
assume A1: for C being Ordinal st C in A holds
C in B ; ::_thesis: A c= B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume A2: x in A ; ::_thesis: x in B
then reconsider C = x as Ordinal by Th13;
C in B by A1, A2;
hence x in B ; ::_thesis: verum
end;
connectedness
for A, B being Ordinal st ex C being Ordinal st
( C in A & not C in B ) holds
for C being Ordinal st C in B holds
C in A
proof
let A, B be Ordinal; ::_thesis: ( ex C being Ordinal st
( C in A & not C in B ) implies for C being Ordinal st C in B holds
C in A )
given C being Ordinal such that A3: ( C in A & not C in B ) ; ::_thesis: for C being Ordinal st C in B holds
C in A
let D be Ordinal; ::_thesis: ( D in B implies D in A )
( A in B or A = B or B in A ) by Th14;
hence ( D in B implies D in A ) by A3, Th10; ::_thesis: verum
end;
end;
:: deftheorem defines c= ORDINAL1:def_5_:_
for A, B being Ordinal holds
( A c= B iff for C being Ordinal st C in A holds
C in B );
theorem :: ORDINAL1:15
for A, B being Ordinal holds A,B are_c=-comparable
proof
let A, B be Ordinal; ::_thesis: A,B are_c=-comparable
( A c= B or B c= A ) ;
hence A,B are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum
end;
theorem Th16: :: ORDINAL1:16
for A, B being Ordinal holds
( A c= B or B in A )
proof
let A, B be Ordinal; ::_thesis: ( A c= B or B in A )
( A in B or A = B or B in A ) by Th14;
hence ( A c= B or B in A ) by Def2; ::_thesis: verum
end;
registration
cluster empty -> ordinal for number ;
coherence
for b1 being number st b1 is empty holds
b1 is ordinal by Lm1;
end;
theorem Th17: :: ORDINAL1:17
for x being set st x is Ordinal holds
succ x is Ordinal
proof
let x be set ; ::_thesis: ( x is Ordinal implies succ x is Ordinal )
A1: now__::_thesis:_for_y_being_set_holds_
(_not_y_in_succ_x_or_y_in_x_or_y_=_x_)
let y be set ; ::_thesis: ( not y in succ x or y in x or y = x )
A2: ( y in {x} implies y = x ) by TARSKI:def_1;
assume y in succ x ; ::_thesis: ( y in x or y = x )
hence ( y in x or y = x ) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
assume A3: x is Ordinal ; ::_thesis: succ x is Ordinal
now__::_thesis:_for_y_being_set_st_y_in_succ_x_holds_
y_c=_succ_x
let y be set ; ::_thesis: ( y in succ x implies y c= succ x )
A4: ( y = x implies y c= succ x ) by XBOOLE_1:7;
A5: now__::_thesis:_(_y_in_x_implies_y_c=_succ_x_)
assume y in x ; ::_thesis: y c= succ x
then A6: y c= x by A3, Def2;
x c= x \/ {x} by XBOOLE_1:7;
hence y c= succ x by A6, XBOOLE_1:1; ::_thesis: verum
end;
assume y in succ x ; ::_thesis: y c= succ x
hence y c= succ x by A1, A5, A4; ::_thesis: verum
end;
then A7: succ x is epsilon-transitive by Def2;
now__::_thesis:_for_y,_z_being_set_st_y_in_succ_x_&_z_in_succ_x_&_not_y_in_z_&_not_y_=_z_holds_
z_in_y
let y, z be set ; ::_thesis: ( y in succ x & z in succ x & not y in z & not y = z implies z in y )
assume that
A8: y in succ x and
A9: z in succ x ; ::_thesis: ( y in z or y = z or z in y )
A10: ( z in x or z = x ) by A1, A9;
( y in x or y = x ) by A1, A8;
hence ( y in z or y = z or z in y ) by A3, A10, Def3; ::_thesis: verum
end;
then succ x is epsilon-connected by Def3;
hence succ x is Ordinal by A7; ::_thesis: verum
end;
theorem Th18: :: ORDINAL1:18
for x being set st x is ordinal holds
union x is ordinal
proof
let x be set ; ::_thesis: ( x is ordinal implies union x is ordinal )
assume ( x is epsilon-transitive & x is epsilon-connected ) ; :: according to ORDINAL1:def_4 ::_thesis: union x is ordinal
then reconsider A = x as Ordinal ;
thus for y being set st y in union x holds
y c= union x :: according to ORDINAL1:def_2,ORDINAL1:def_4 ::_thesis: union x is epsilon-connected
proof
let y be set ; ::_thesis: ( y in union x implies y c= union x )
assume y in union x ; ::_thesis: y c= union x
then consider z being set such that
A1: y in z and
A2: z in x by TARSKI:def_4;
z in A by A2;
then reconsider z = z as Ordinal by Th13;
z c= A by A2, Def2;
hence y c= union x by A1, ZFMISC_1:74; ::_thesis: verum
end;
let y be set ; :: according to ORDINAL1:def_3 ::_thesis: for y being set st y in union x & y in union x & not y in y & not y = y holds
y in y
let z be set ; ::_thesis: ( y in union x & z in union x & not y in z & not y = z implies z in y )
assume that
A3: y in union x and
A4: z in union x ; ::_thesis: ( y in z or y = z or z in y )
consider X being set such that
A5: y in X and
A6: X in x by A3, TARSKI:def_4;
A7: X in A by A6;
consider Y being set such that
A8: z in Y and
A9: Y in x by A4, TARSKI:def_4;
reconsider X = X, Y = Y as Ordinal by A9, A7, Th13;
z in Y by A8;
then A10: z is Ordinal by Th13;
y in X by A5;
then y is Ordinal by Th13;
hence ( y in z or y = z or z in y ) by A10, Th14; ::_thesis: verum
end;
registration
cluster non empty epsilon-transitive epsilon-connected ordinal for number ;
existence
not for b1 being Ordinal holds b1 is empty
proof
reconsider A = succ {} as Ordinal by Th17;
take A ; ::_thesis: not A is empty
thus not A is empty ; ::_thesis: verum
end;
end;
registration
let A be Ordinal;
cluster succ A -> non empty ordinal ;
coherence
( not succ A is empty & succ A is ordinal ) by Th17;
cluster union A -> ordinal ;
coherence
union A is ordinal by Th18;
end;
theorem Th19: :: ORDINAL1:19
for X being set st ( for x being set st x in X holds
( x is Ordinal & x c= X ) ) holds
X is ordinal
proof
let X be set ; ::_thesis: ( ( for x being set st x in X holds
( x is Ordinal & x c= X ) ) implies X is ordinal )
assume A1: for x being set st x in X holds
( x is Ordinal & x c= X ) ; ::_thesis: X is ordinal
thus X is epsilon-transitive :: according to ORDINAL1:def_4 ::_thesis: X is epsilon-connected
proof
let x be set ; :: according to ORDINAL1:def_2 ::_thesis: ( x in X implies x c= X )
assume x in X ; ::_thesis: x c= X
hence x c= X by A1; ::_thesis: verum
end;
let x be set ; :: according to ORDINAL1:def_3 ::_thesis: for y being set st x in X & y in X & not x in y & not x = y holds
y in x
let y be set ; ::_thesis: ( x in X & y in X & not x in y & not x = y implies y in x )
assume ( x in X & y in X ) ; ::_thesis: ( x in y or x = y or y in x )
then ( x is Ordinal & y is Ordinal ) by A1;
hence ( x in y or x = y or y in x ) by Th14; ::_thesis: verum
end;
theorem Th20: :: ORDINAL1:20
for X being set
for A being Ordinal st X c= A & X <> {} holds
ex C being Ordinal st
( C in X & ( for B being Ordinal st B in X holds
C c= B ) )
proof
let X be set ; ::_thesis: for A being Ordinal st X c= A & X <> {} holds
ex C being Ordinal st
( C in X & ( for B being Ordinal st B in X holds
C c= B ) )
let A be Ordinal; ::_thesis: ( X c= A & X <> {} implies ex C being Ordinal st
( C in X & ( for B being Ordinal st B in X holds
C c= B ) ) )
set a = the Element of X;
assume that
A1: X c= A and
A2: X <> {} ; ::_thesis: ex C being Ordinal st
( C in X & ( for B being Ordinal st B in X holds
C c= B ) )
the Element of X in X by A2;
then consider Y being set such that
A3: Y in X and
A4: for a being set holds
( not a in X or not a in Y ) by TARSKI:2;
Y is Ordinal by A1, A3, Th13;
then consider C being Ordinal such that
A5: C = Y ;
take C ; ::_thesis: ( C in X & ( for B being Ordinal st B in X holds
C c= B ) )
thus C in X by A3, A5; ::_thesis: for B being Ordinal st B in X holds
C c= B
let B be Ordinal; ::_thesis: ( B in X implies C c= B )
assume B in X ; ::_thesis: C c= B
then not B in C by A4, A5;
then ( B = C or C in B ) by Th14;
hence C c= B by Def2; ::_thesis: verum
end;
theorem Th21: :: ORDINAL1:21
for A, B being Ordinal holds
( A in B iff succ A c= B )
proof
let A, B be Ordinal; ::_thesis: ( A in B iff succ A c= B )
thus ( A in B implies succ A c= B ) ::_thesis: ( succ A c= B implies A in B )
proof
assume A1: A in B ; ::_thesis: succ A c= B
then for a being set st a in {A} holds
a in B by TARSKI:def_1;
then A2: {A} c= B by TARSKI:def_3;
A c= B by A1, Def2;
hence succ A c= B by A2, XBOOLE_1:8; ::_thesis: verum
end;
assume A3: succ A c= B ; ::_thesis: A in B
A in succ A by Th6;
hence A in B by A3; ::_thesis: verum
end;
theorem Th22: :: ORDINAL1:22
for A, C being Ordinal holds
( A in succ C iff A c= C )
proof
let A, C be Ordinal; ::_thesis: ( A in succ C iff A c= C )
thus ( A in succ C implies A c= C ) ::_thesis: ( A c= C implies A in succ C )
proof
assume A in succ C ; ::_thesis: A c= C
then ( A in C or A in {C} ) by XBOOLE_0:def_3;
hence A c= C by Def2, TARSKI:def_1; ::_thesis: verum
end;
assume A1: A c= C ; ::_thesis: A in succ C
assume not A in succ C ; ::_thesis: contradiction
then ( A = succ C or succ C in A ) by Th14;
then A2: succ C c= C by A1, Def2;
C in succ C by Th6;
then C c= succ C by Def2;
then succ C = C by A2, XBOOLE_0:def_10;
hence contradiction by Th9; ::_thesis: verum
end;
scheme :: ORDINAL1:sch 1
OrdinalMin{ P1[ Ordinal] } :
ex A being Ordinal st
( P1[A] & ( for B being Ordinal st P1[B] holds
A c= B ) )
provided
A1: ex A being Ordinal st P1[A]
proof
consider A being Ordinal such that
A2: P1[A] by A1;
defpred S1[ set ] means ex B being Ordinal st
( $1 = B & P1[B] );
consider X being set such that
A3: for x being set holds
( x in X iff ( x in succ A & S1[x] ) ) from XBOOLE_0:sch_1();
for a being set st a in X holds
a in succ A by A3;
then A4: X c= succ A by TARSKI:def_3;
A in succ A by Th6;
then X <> {} by A2, A3;
then consider C being Ordinal such that
A5: C in X and
A6: for B being Ordinal st B in X holds
C c= B by A4, Th20;
C in succ A by A3, A5;
then A7: C c= succ A by Def2;
take C ; ::_thesis: ( P1[C] & ( for B being Ordinal st P1[B] holds
C c= B ) )
ex B being Ordinal st
( C = B & P1[B] ) by A3, A5;
hence P1[C] ; ::_thesis: for B being Ordinal st P1[B] holds
C c= B
let B be Ordinal; ::_thesis: ( P1[B] implies C c= B )
assume A8: P1[B] ; ::_thesis: C c= B
assume A9: not C c= B ; ::_thesis: contradiction
then B c< C by XBOOLE_0:def_8;
then B in C by Th11;
then B in X by A3, A8, A7;
hence contradiction by A6, A9; ::_thesis: verum
end;
scheme :: ORDINAL1:sch 2
TransfiniteInd{ P1[ Ordinal] } :
for A being Ordinal holds P1[A]
provided
A1: for A being Ordinal st ( for C being Ordinal st C in A holds
P1[C] ) holds
P1[A]
proof
defpred S1[ set ] means ex B being Ordinal st
( $1 = B & P1[B] );
let A be Ordinal; ::_thesis: P1[A]
set Y = succ A;
consider Z being set such that
A2: for x being set holds
( x in Z iff ( x in succ A & S1[x] ) ) from XBOOLE_0:sch_1();
now__::_thesis:_not_(succ_A)_\_Z_<>_{}
assume (succ A) \ Z <> {} ; ::_thesis: contradiction
then consider C being Ordinal such that
A3: C in (succ A) \ Z and
A4: for B being Ordinal st B in (succ A) \ Z holds
C c= B by Th20;
now__::_thesis:_for_B_being_Ordinal_st_B_in_C_holds_
P1[B]
let B be Ordinal; ::_thesis: ( B in C implies P1[B] )
assume A5: B in C ; ::_thesis: P1[B]
A6: C c= succ A by A3, Def2;
now__::_thesis:_B_in_Z
assume not B in Z ; ::_thesis: contradiction
then B in (succ A) \ Z by A5, A6, XBOOLE_0:def_5;
then A7: C c= B by A4;
C <> B by A5;
then C c< B by A7, XBOOLE_0:def_8;
hence contradiction by A5, Th11; ::_thesis: verum
end;
then ex B9 being Ordinal st
( B = B9 & P1[B9] ) by A2;
hence P1[B] ; ::_thesis: verum
end;
then A8: P1[C] by A1;
not C in Z by A3, XBOOLE_0:def_5;
hence contradiction by A2, A3, A8; ::_thesis: verum
end;
then ( not A in succ A or A in Z ) by XBOOLE_0:def_5;
then ex B being Ordinal st
( A = B & P1[B] ) by A2, Th6;
hence P1[A] ; ::_thesis: verum
end;
theorem Th23: :: ORDINAL1:23
for X being set st ( for a being set st a in X holds
a is Ordinal ) holds
union X is ordinal
proof
let X be set ; ::_thesis: ( ( for a being set st a in X holds
a is Ordinal ) implies union X is ordinal )
assume A1: for a being set st a in X holds
a is Ordinal ; ::_thesis: union X is ordinal
thus union X is epsilon-transitive :: according to ORDINAL1:def_4 ::_thesis: union X is epsilon-connected
proof
let x be set ; :: according to ORDINAL1:def_2 ::_thesis: ( x in union X implies x c= union X )
assume x in union X ; ::_thesis: x c= union X
then consider Y being set such that
A2: x in Y and
A3: Y in X by TARSKI:def_4;
Y is Ordinal by A1, A3;
then A4: x c= Y by A2, Def2;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in x or a in union X )
assume a in x ; ::_thesis: a in union X
hence a in union X by A3, A4, TARSKI:def_4; ::_thesis: verum
end;
let x be set ; :: according to ORDINAL1:def_3 ::_thesis: for y being set st x in union X & y in union X & not x in y & not x = y holds
y in x
let y be set ; ::_thesis: ( x in union X & y in union X & not x in y & not x = y implies y in x )
assume that
A5: x in union X and
A6: y in union X ; ::_thesis: ( x in y or x = y or y in x )
consider Z being set such that
A7: y in Z and
A8: Z in X by A6, TARSKI:def_4;
Z is Ordinal by A1, A8;
then A9: y is Ordinal by A7, Th13;
consider Y being set such that
A10: x in Y and
A11: Y in X by A5, TARSKI:def_4;
Y is Ordinal by A1, A11;
then x is Ordinal by A10, Th13;
hence ( x in y or x = y or y in x ) by A9, Th14; ::_thesis: verum
end;
theorem Th24: :: ORDINAL1:24
for X being set st ( for a being set st a in X holds
a is Ordinal ) holds
ex A being Ordinal st X c= A
proof
let X be set ; ::_thesis: ( ( for a being set st a in X holds
a is Ordinal ) implies ex A being Ordinal st X c= A )
assume A1: for a being set st a in X holds
a is Ordinal ; ::_thesis: ex A being Ordinal st X c= A
then A2: union X is Ordinal by Th23;
then reconsider A = succ (union X) as Ordinal ;
take A ; ::_thesis: X c= A
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in A )
assume A3: a in X ; ::_thesis: a in A
then reconsider B = a as Ordinal by A1;
for b being set st b in B holds
b in union X by A3, TARSKI:def_4;
then B c= union X by TARSKI:def_3;
hence a in A by A2, Th22; ::_thesis: verum
end;
theorem Th25: :: ORDINAL1:25
for X being set holds
not for x being set holds
( x in X iff x is Ordinal )
proof
given X being set such that A1: for x being set holds
( x in X iff x is Ordinal ) ; ::_thesis: contradiction
A2: X is epsilon-transitive
proof
let x be set ; :: according to ORDINAL1:def_2 ::_thesis: ( x in X implies x c= X )
assume x in X ; ::_thesis: x c= X
then A3: x is Ordinal by A1;
thus x c= X ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in x or a in X )
assume a in x ; ::_thesis: a in X
then a is Ordinal by A3, Th13;
hence a in X by A1; ::_thesis: verum
end;
end;
X is epsilon-connected
proof
let x be set ; :: according to ORDINAL1:def_3 ::_thesis: for y being set st x in X & y in X & not x in y & not x = y holds
y in x
let y be set ; ::_thesis: ( x in X & y in X & not x in y & not x = y implies y in x )
assume ( x in X & y in X ) ; ::_thesis: ( x in y or x = y or y in x )
then ( x is Ordinal & y is Ordinal ) by A1;
hence ( x in y or x = y or y in x ) by Th14; ::_thesis: verum
end;
then X in X by A1, A2;
hence contradiction ; ::_thesis: verum
end;
theorem Th26: :: ORDINAL1:26
for X being set holds
not for A being Ordinal holds A in X
proof
defpred S1[ set ] means $1 is Ordinal;
given X being set such that A1: for A being Ordinal holds A in X ; ::_thesis: contradiction
consider Y being set such that
A2: for a being set holds
( a in Y iff ( a in X & S1[a] ) ) from XBOOLE_0:sch_1();
now__::_thesis:_for_x_being_set_st_x_is_Ordinal_holds_
x_in_Y
let x be set ; ::_thesis: ( x is Ordinal implies x in Y )
assume A3: x is Ordinal ; ::_thesis: x in Y
then x in X by A1;
hence x in Y by A2, A3; ::_thesis: verum
end;
then for x being set holds
( x in Y iff x is Ordinal ) by A2;
hence contradiction by Th25; ::_thesis: verum
end;
theorem :: ORDINAL1:27
for X being set ex A being Ordinal st
( not A in X & ( for B being Ordinal st not B in X holds
A c= B ) )
proof
let X be set ; ::_thesis: ex A being Ordinal st
( not A in X & ( for B being Ordinal st not B in X holds
A c= B ) )
defpred S1[ set ] means not $1 in X;
consider B being Ordinal such that
A1: not B in X by Th26;
consider Y being set such that
A2: for a being set holds
( a in Y iff ( a in succ B & S1[a] ) ) from XBOOLE_0:sch_1();
for a being set st a in Y holds
a in succ B by A2;
then A3: Y c= succ B by TARSKI:def_3;
B in succ B by Th6;
then Y <> {} by A1, A2;
then consider A being Ordinal such that
A4: A in Y and
A5: for B being Ordinal st B in Y holds
A c= B by A3, Th20;
A in succ B by A2, A4;
then A6: A c= succ B by Def2;
take A ; ::_thesis: ( not A in X & ( for B being Ordinal st not B in X holds
A c= B ) )
thus not A in X by A2, A4; ::_thesis: for B being Ordinal st not B in X holds
A c= B
let C be Ordinal; ::_thesis: ( not C in X implies A c= C )
assume A7: not C in X ; ::_thesis: A c= C
assume A8: not A c= C ; ::_thesis: contradiction
then not A in C by Def2;
then C in A by A8, Th14;
then C in Y by A2, A7, A6;
hence contradiction by A5, A8; ::_thesis: verum
end;
definition
let A be set ;
attrA is limit_ordinal means :Def6: :: ORDINAL1:def 6
A = union A;
end;
:: deftheorem Def6 defines limit_ordinal ORDINAL1:def_6_:_
for A being set holds
( A is limit_ordinal iff A = union A );
theorem Th28: :: ORDINAL1:28
for A being Ordinal holds
( A is limit_ordinal iff for C being Ordinal st C in A holds
succ C in A )
proof
let A be Ordinal; ::_thesis: ( A is limit_ordinal iff for C being Ordinal st C in A holds
succ C in A )
thus ( A is limit_ordinal implies for C being Ordinal st C in A holds
succ C in A ) ::_thesis: ( ( for C being Ordinal st C in A holds
succ C in A ) implies A is limit_ordinal )
proof
assume A is limit_ordinal ; ::_thesis: for C being Ordinal st C in A holds
succ C in A
then A1: A = union A by Def6;
let C be Ordinal; ::_thesis: ( C in A implies succ C in A )
assume C in A ; ::_thesis: succ C in A
then consider z being set such that
A2: C in z and
A3: z in A by A1, TARSKI:def_4;
for b being set st b in {C} holds
b in z by A2, TARSKI:def_1;
then A4: {C} c= z by TARSKI:def_3;
A5: z is Ordinal by A3, Th13;
then C c= z by A2, Def2;
then succ C c= z by A4, XBOOLE_1:8;
then ( succ C = z or succ C c< z ) by XBOOLE_0:def_8;
then A6: ( succ C = z or succ C in z ) by A5, Th11;
z c= A by A3, Def2;
hence succ C in A by A3, A6; ::_thesis: verum
end;
assume A7: for C being Ordinal st C in A holds
succ C in A ; ::_thesis: A is limit_ordinal
now__::_thesis:_for_a_being_set_st_a_in_A_holds_
a_in_union_A
let a be set ; ::_thesis: ( a in A implies a in union A )
assume A8: a in A ; ::_thesis: a in union A
then a is Ordinal by Th13;
then A9: succ a in A by A7, A8;
a in succ a by Th6;
hence a in union A by A9, TARSKI:def_4; ::_thesis: verum
end;
then A10: A c= union A by TARSKI:def_3;
now__::_thesis:_for_a_being_set_st_a_in_union_A_holds_
a_in_A
let a be set ; ::_thesis: ( a in union A implies a in A )
assume a in union A ; ::_thesis: a in A
then consider z being set such that
A11: a in z and
A12: z in A by TARSKI:def_4;
z c= A by A12, Def2;
hence a in A by A11; ::_thesis: verum
end;
then union A c= A by TARSKI:def_3;
then A = union A by A10, XBOOLE_0:def_10;
hence A is limit_ordinal by Def6; ::_thesis: verum
end;
theorem :: ORDINAL1:29
for A being Ordinal holds
( not A is limit_ordinal iff ex B being Ordinal st A = succ B )
proof
let A be Ordinal; ::_thesis: ( not A is limit_ordinal iff ex B being Ordinal st A = succ B )
thus ( not A is limit_ordinal implies ex B being Ordinal st A = succ B ) ::_thesis: ( ex B being Ordinal st A = succ B implies not A is limit_ordinal )
proof
assume not A is limit_ordinal ; ::_thesis: ex B being Ordinal st A = succ B
then consider B being Ordinal such that
A1: B in A and
A2: not succ B in A by Th28;
take B ; ::_thesis: A = succ B
assume A3: A <> succ B ; ::_thesis: contradiction
succ B c= A by A1, Th21;
then succ B c< A by A3, XBOOLE_0:def_8;
hence contradiction by A2, Th11; ::_thesis: verum
end;
given B being Ordinal such that A4: A = succ B ; ::_thesis: not A is limit_ordinal
( B in A & not succ B in A ) by A4, Th6;
hence not A is limit_ordinal by Th28; ::_thesis: verum
end;
definition
let IT be set ;
attrIT is T-Sequence-like means :Def7: :: ORDINAL1:def 7
proj1 IT is ordinal ;
end;
:: deftheorem Def7 defines T-Sequence-like ORDINAL1:def_7_:_
for IT being set holds
( IT is T-Sequence-like iff proj1 IT is ordinal );
registration
cluster empty -> T-Sequence-like for number ;
coherence
for b1 being set st b1 is empty holds
b1 is T-Sequence-like
proof
let E be set ; ::_thesis: ( E is empty implies E is T-Sequence-like )
assume E is empty ; ::_thesis: E is T-Sequence-like
then proj1 E = {} ;
hence E is T-Sequence-like by Def7; ::_thesis: verum
end;
end;
definition
mode T-Sequence is T-Sequence-like Function;
end;
registration
let Z be set ;
cluster Relation-like Z -valued Function-like T-Sequence-like for number ;
existence
ex b1 being T-Sequence st b1 is Z -valued
proof
reconsider L = {} as T-Sequence ;
take L ; ::_thesis: L is Z -valued
rng {} = {} ;
hence rng L c= Z by XBOOLE_1:2; :: according to RELAT_1:def_19 ::_thesis: verum
end;
end;
definition
let Z be set ;
mode T-Sequence of Z is Z -valued T-Sequence;
end;
theorem :: ORDINAL1:30
for Z being set holds {} is T-Sequence of Z
proof
let Z be set ; ::_thesis: {} is T-Sequence of Z
reconsider L = {} as T-Sequence ;
rng L = {} ;
then rng L c= Z by XBOOLE_1:2;
hence {} is T-Sequence of Z by RELAT_1:def_19; ::_thesis: verum
end;
theorem :: ORDINAL1:31
for F being Function st dom F is Ordinal holds
F is T-Sequence of rng F by Def7, RELAT_1:def_19;
registration
let L be T-Sequence;
cluster proj1 L -> ordinal ;
coherence
dom L is ordinal by Def7;
end;
theorem :: ORDINAL1:32
for X, Y being set st X c= Y holds
for L being T-Sequence of X holds L is T-Sequence of Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies for L being T-Sequence of X holds L is T-Sequence of Y )
assume A1: X c= Y ; ::_thesis: for L being T-Sequence of X holds L is T-Sequence of Y
let L be T-Sequence of X; ::_thesis: L is T-Sequence of Y
rng L c= X by RELAT_1:def_19;
then rng L c= Y by A1, XBOOLE_1:1;
hence L is T-Sequence of Y by RELAT_1:def_19; ::_thesis: verum
end;
registration
let L be T-Sequence;
let A be Ordinal;
clusterL | A -> rng L -valued T-Sequence-like ;
coherence
( L | A is rng L -valued & L | A is T-Sequence-like )
proof
A1: rng (L | A) c= rng L by RELAT_1:70;
( A c= dom L implies dom (L | A) = A ) by RELAT_1:62;
hence ( L | A is rng L -valued & L | A is T-Sequence-like ) by A1, Def7, RELAT_1:68, RELAT_1:def_19; ::_thesis: verum
end;
end;
theorem :: ORDINAL1:33
for X being set
for L being T-Sequence of X
for A being Ordinal holds L | A is T-Sequence of X ;
definition
let IT be set ;
attrIT is c=-linear means :Def8: :: ORDINAL1:def 8
for x, y being set st x in IT & y in IT holds
x,y are_c=-comparable ;
end;
:: deftheorem Def8 defines c=-linear ORDINAL1:def_8_:_
for IT being set holds
( IT is c=-linear iff for x, y being set st x in IT & y in IT holds
x,y are_c=-comparable );
theorem :: ORDINAL1:34
for X being set st ( for a being set st a in X holds
a is T-Sequence ) & X is c=-linear holds
union X is T-Sequence
proof
let X be set ; ::_thesis: ( ( for a being set st a in X holds
a is T-Sequence ) & X is c=-linear implies union X is T-Sequence )
assume that
A1: for a being set st a in X holds
a is T-Sequence and
A2: X is c=-linear ; ::_thesis: union X is T-Sequence
( union X is Relation-like & union X is Function-like )
proof
thus for a being set st a in union X holds
ex b, c being set st [b,c] = a :: according to RELAT_1:def_1 ::_thesis: union X is Function-like
proof
let a be set ; ::_thesis: ( a in union X implies ex b, c being set st [b,c] = a )
assume a in union X ; ::_thesis: ex b, c being set st [b,c] = a
then consider x being set such that
A3: a in x and
A4: x in X by TARSKI:def_4;
reconsider x = x as T-Sequence by A1, A4;
for a being set st a in x holds
ex b, c being set st [b,c] = a by RELAT_1:def_1;
hence ex b, c being set st [b,c] = a by A3; ::_thesis: verum
end;
let a be set ; :: according to FUNCT_1:def_1 ::_thesis: for b1, b2 being number holds
( not [a,b1] in union X or not [a,b2] in union X or b1 = b2 )
let b, c be set ; ::_thesis: ( not [a,b] in union X or not [a,c] in union X or b = c )
assume that
A5: [a,b] in union X and
A6: [a,c] in union X ; ::_thesis: b = c
consider y being set such that
A7: [a,c] in y and
A8: y in X by A6, TARSKI:def_4;
reconsider y = y as T-Sequence by A1, A8;
consider x being set such that
A9: [a,b] in x and
A10: x in X by A5, TARSKI:def_4;
reconsider x = x as T-Sequence by A1, A10;
x,y are_c=-comparable by A2, A10, A8, Def8;
then ( x c= y or y c= x ) by XBOOLE_0:def_9;
hence b = c by A9, A7, FUNCT_1:def_1; ::_thesis: verum
end;
then reconsider F = union X as Function ;
defpred S1[ set , set ] means ( $1 in X & ( for L being T-Sequence st L = $1 holds
dom L = $2 ) );
A11: for a, b, c being set st S1[a,b] & S1[a,c] holds
b = c
proof
let a, b, c be set ; ::_thesis: ( S1[a,b] & S1[a,c] implies b = c )
assume that
A12: a in X and
A13: for L being T-Sequence st L = a holds
dom L = b and
a in X and
A14: for L being T-Sequence st L = a holds
dom L = c ; ::_thesis: b = c
reconsider a = a as T-Sequence by A1, A12;
dom a = b by A13;
hence b = c by A14; ::_thesis: verum
end;
consider G being Function such that
A15: for a, b being set holds
( [a,b] in G iff ( a in X & S1[a,b] ) ) from FUNCT_1:sch_1(A11);
A16: for a, b being set st [a,b] in G holds
b is Ordinal
proof
let a, b be set ; ::_thesis: ( [a,b] in G implies b is Ordinal )
assume A17: [a,b] in G ; ::_thesis: b is Ordinal
then a in X by A15;
then reconsider a = a as T-Sequence by A1;
dom a = b by A15, A17;
hence b is Ordinal ; ::_thesis: verum
end;
for a being set st a in rng G holds
a is Ordinal
proof
let a be set ; ::_thesis: ( a in rng G implies a is Ordinal )
assume a in rng G ; ::_thesis: a is Ordinal
then consider b being set such that
A18: ( b in dom G & a = G . b ) by FUNCT_1:def_3;
[b,a] in G by A18, FUNCT_1:1;
hence a is Ordinal by A16; ::_thesis: verum
end;
then consider A being Ordinal such that
A19: rng G c= A by Th24;
defpred S2[ Ordinal] means for B being Ordinal st B in rng G holds
B c= $1;
for B being Ordinal st B in rng G holds
B c= A by A19, Def2;
then A20: ex A being Ordinal st S2[A] ;
consider A being Ordinal such that
A21: ( S2[A] & ( for C being Ordinal st S2[C] holds
A c= C ) ) from ORDINAL1:sch_1(A20);
dom F = A
proof
thus for a being set st a in dom F holds
a in A :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A c= dom F
proof
let a be set ; ::_thesis: ( a in dom F implies a in A )
assume a in dom F ; ::_thesis: a in A
then consider b being set such that
A22: [a,b] in F by XTUPLE_0:def_12;
consider x being set such that
A23: [a,b] in x and
A24: x in X by A22, TARSKI:def_4;
reconsider x = x as T-Sequence by A1, A24;
for L being T-Sequence st L = x holds
dom L = dom x ;
then [x,(dom x)] in G by A15, A24;
then ( x in dom G & dom x = G . x ) by FUNCT_1:1;
then dom x in rng G by FUNCT_1:def_3;
then A25: dom x c= A by A21;
a in dom x by A23, XTUPLE_0:def_12;
hence a in A by A25; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in dom F )
assume A26: a in A ; ::_thesis: a in dom F
then reconsider a9 = a as Ordinal by Th13;
now__::_thesis:_ex_L_being_T-Sequence_st_
(_L_in_X_&_a9_in_dom_L_)
assume A27: for L being T-Sequence st L in X holds
not a9 in dom L ; ::_thesis: contradiction
now__::_thesis:_for_B_being_Ordinal_st_B_in_rng_G_holds_
B_c=_a9
let B be Ordinal; ::_thesis: ( B in rng G implies B c= a9 )
assume B in rng G ; ::_thesis: B c= a9
then consider c being set such that
A28: ( c in dom G & B = G . c ) by FUNCT_1:def_3;
A29: [c,B] in G by A28, FUNCT_1:1;
then c in X by A15;
then reconsider c = c as T-Sequence by A1;
( c in X & dom c = B ) by A15, A29;
hence B c= a9 by A27, Th16; ::_thesis: verum
end;
then A30: A c= a9 by A21;
a9 c= A by A26, Def2;
then A = a by A30, XBOOLE_0:def_10;
hence contradiction by A26; ::_thesis: verum
end;
then consider L being T-Sequence such that
A31: ( L in X & a in dom L ) ;
( L c= F & ex b being set st [a,b] in L ) by A31, XTUPLE_0:def_12, ZFMISC_1:74;
hence a in dom F by XTUPLE_0:def_12; ::_thesis: verum
end;
hence union X is T-Sequence by Def7; ::_thesis: verum
end;
scheme :: ORDINAL1:sch 3
TSUniq{ F1() -> Ordinal, F2( T-Sequence) -> set , F3() -> T-Sequence, F4() -> T-Sequence } :
F3() = F4()
provided
A1: ( dom F3() = F1() & ( for B being Ordinal
for L being T-Sequence st B in F1() & L = F3() | B holds
F3() . B = F2(L) ) ) and
A2: ( dom F4() = F1() & ( for B being Ordinal
for L being T-Sequence st B in F1() & L = F4() | B holds
F4() . B = F2(L) ) )
proof
defpred S1[ set ] means F3() . $1 <> F4() . $1;
consider X being set such that
A3: for x being set holds
( x in X iff ( x in F1() & S1[x] ) ) from XBOOLE_0:sch_1();
for b being set st b in X holds
b in F1() by A3;
then A4: X c= F1() by TARSKI:def_3;
assume F3() <> F4() ; ::_thesis: contradiction
then ex a being set st
( a in F1() & F3() . a <> F4() . a ) by A1, A2, FUNCT_1:2;
then X <> {} by A3;
then consider B being Ordinal such that
A5: B in X and
A6: for C being Ordinal st C in X holds
B c= C by A4, Th20;
A7: B in F1() by A3, A5;
then A8: B c= F1() by Def2;
then A9: dom (F3() | B) = B by A1, RELAT_1:62;
A10: dom (F4() | B) = B by A2, A8, RELAT_1:62;
A11: now__::_thesis:_for_C_being_Ordinal_st_C_in_B_holds_
F3()_._C_=_F4()_._C
let C be Ordinal; ::_thesis: ( C in B implies F3() . C = F4() . C )
assume A12: C in B ; ::_thesis: F3() . C = F4() . C
then not C in X by A6, Th5;
hence F3() . C = F4() . C by A3, A8, A12; ::_thesis: verum
end;
now__::_thesis:_for_a_being_set_st_a_in_B_holds_
(F3()_|_B)_._a_=_(F4()_|_B)_._a
let a be set ; ::_thesis: ( a in B implies (F3() | B) . a = (F4() | B) . a )
assume A13: a in B ; ::_thesis: (F3() | B) . a = (F4() | B) . a
then reconsider a9 = a as Ordinal by Th13;
( F3() . a9 = F4() . a9 & (F3() | B) . a = F3() . a ) by A11, A9, A13, FUNCT_1:47;
hence (F3() | B) . a = (F4() | B) . a by A10, A13, FUNCT_1:47; ::_thesis: verum
end;
then A14: F3() | B = F4() | B by A9, A10, FUNCT_1:2;
( F3() . B = F2((F3() | B)) & F4() . B = F2((F4() | B)) ) by A1, A2, A7;
hence contradiction by A3, A5, A14; ::_thesis: verum
end;
scheme :: ORDINAL1:sch 4
TSExist{ F1() -> Ordinal, F2( T-Sequence) -> set } :
ex L being T-Sequence st
( dom L = F1() & ( for B being Ordinal
for L1 being T-Sequence st B in F1() & L1 = L | B holds
L . B = F2(L1) ) )
proof
defpred S1[ Ordinal] means ex L being T-Sequence st
( dom L = $1 & ( for B being Ordinal st B in $1 holds
L . B = F2((L | B)) ) );
A1: for B being Ordinal st ( for C being Ordinal st C in B holds
S1[C] ) holds
S1[B]
proof
defpred S2[ 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
( dom L = A & ( for B being Ordinal st B in A holds
L . B = F2((L | B)) ) ) ) );
let B be Ordinal; ::_thesis: ( ( for C being Ordinal st C in B holds
S1[C] ) implies S1[B] )
assume A2: for C being Ordinal st C in B holds
ex L being T-Sequence st
( dom L = C & ( for D being Ordinal st D in C holds
L . D = F2((L | D)) ) ) ; ::_thesis: S1[B]
A3: for a, b, c being set st S2[a,b] & S2[a,c] holds
b = c
proof
let a, b, c be set ; ::_thesis: ( S2[a,b] & S2[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
( dom L = A & ( for B being Ordinal st B in A holds
L . B = F2((L | B)) ) ) 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
( dom L = A & ( for B being Ordinal st B in A holds
L . B = F2((L | B)) ) ) ; ::_thesis: b = c
reconsider c = c as T-Sequence by A7;
reconsider a = a as Ordinal by A4;
A9: ( dom c = a & ( for B being Ordinal
for L being T-Sequence st B in a & L = c | B holds
c . B = F2(L) ) ) by A8;
reconsider b = b as T-Sequence by A5;
A10: ( dom b = a & ( for B being Ordinal
for L being T-Sequence st B in a & L = b | B holds
b . B = F2(L) ) ) by A6;
b = c from ORDINAL1:sch_3(A10, A9);
hence b = c ; ::_thesis: verum
end;
consider G being Function such that
A11: for a, b being set holds
( [a,b] in G iff ( a in B & S2[a,b] ) ) from FUNCT_1:sch_1(A3);
defpred S3[ set , set ] means ex L being T-Sequence st
( L = G . $1 & $2 = F2(L) );
A12: 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 A11; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B or a in dom G )
assume A13: a in B ; ::_thesis: a in dom G
then reconsider a9 = a as Ordinal by Th13;
consider L being T-Sequence such that
A14: ( dom L = a9 & ( for D being Ordinal st D in a9 holds
L . D = F2((L | D)) ) ) by A2, A13;
for A being Ordinal
for K being T-Sequence st A = a9 & K = L holds
( dom K = A & ( for B being Ordinal st B in A holds
K . B = F2((K | B)) ) ) by A14;
then [a9,L] in G by A11, A13;
hence a in dom G by XTUPLE_0:def_12; ::_thesis: verum
end;
A15: for a being set st a in B holds
ex b being set st S3[a,b]
proof
let a be set ; ::_thesis: ( a in B implies ex b being set st S3[a,b] )
assume a in B ; ::_thesis: ex b being set st S3[a,b]
then consider c being set such that
A16: [a,c] in G by A12, XTUPLE_0:def_12;
reconsider L = c as T-Sequence by A11, A16;
take F2(L) ; ::_thesis: S3[a,F2(L)]
take L ; ::_thesis: ( L = G . a & F2(L) = F2(L) )
thus L = G . a by A16, FUNCT_1:1; ::_thesis: F2(L) = F2(L)
thus F2(L) = F2(L) ; ::_thesis: verum
end;
A17: for a, b, c being set st a in B & S3[a,b] & S3[a,c] holds
b = c ;
consider F being Function such that
A18: ( dom F = B & ( for a being set st a in B holds
S3[a,F . a] ) ) from FUNCT_1:sch_2(A17, A15);
reconsider L = F as T-Sequence by A18, Def7;
take L ; ::_thesis: ( dom L = B & ( for B being Ordinal st B in B holds
L . B = F2((L | B)) ) )
thus dom L = B by A18; ::_thesis: for B being Ordinal st B in B holds
L . B = F2((L | B))
let D be Ordinal; ::_thesis: ( D in B implies L . D = F2((L | D)) )
assume A19: D in B ; ::_thesis: L . D = F2((L | D))
then consider K being T-Sequence such that
A20: K = G . D and
A21: F . D = F2(K) by A18;
A22: [D,K] in G by A12, A19, A20, FUNCT_1:1;
then A23: dom K = D by A11;
A24: now__::_thesis:_for_C_being_Ordinal_st_C_in_D_holds_
G_._C_=_K_|_C
let C be Ordinal; ::_thesis: ( C in D implies G . C = K | C )
assume A25: C in D ; ::_thesis: G . C = K | C
A26: now__::_thesis:_for_A_being_Ordinal
for_L_being_T-Sequence_st_A_=_C_&_L_=_K_|_C_holds_
(_dom_L_=_A_&_(_for_B_being_Ordinal_st_B_in_A_holds_
L_._B_=_F2((L_|_B))_)_)
let A be Ordinal; ::_thesis: for L being T-Sequence st A = C & L = K | C holds
( dom L = A & ( for B being Ordinal st B in A holds
L . B = F2((L | B)) ) )
let L be T-Sequence; ::_thesis: ( A = C & L = K | C implies ( dom L = A & ( for B being Ordinal st B in A holds
L . B = F2((L | B)) ) ) )
assume that
A27: A = C and
A28: L = K | C ; ::_thesis: ( dom L = A & ( for B being Ordinal st B in A holds
L . B = F2((L | B)) ) )
A29: C c= D by A25, Def2;
hence A30: dom L = A by A23, A27, A28, RELAT_1:62; ::_thesis: for B being Ordinal st B in A holds
L . B = F2((L | B))
let B be Ordinal; ::_thesis: ( B in A implies L . B = F2((L | B)) )
assume A31: B in A ; ::_thesis: L . B = F2((L | B))
then B c= A by Def2;
then A32: K | B = L | B by A27, A28, FUNCT_1:51;
K . B = F2((K | B)) by A11, A22, A27, A29, A31;
hence L . B = F2((L | B)) by A28, A30, A31, A32, FUNCT_1:47; ::_thesis: verum
end;
C in B by A19, A25, Th10;
then [C,(K | C)] in G by A11, A26;
hence G . C = K | C by FUNCT_1:1; ::_thesis: verum
end;
A33: now__::_thesis:_for_a_being_set_st_a_in_D_holds_
(L_|_D)_._a_=_K_._a
let a be set ; ::_thesis: ( a in D implies (L | D) . a = K . a )
assume A34: a in D ; ::_thesis: (L | D) . a = K . a
then reconsider A = a as Ordinal by Th13;
A35: ( G . A = K | A & (L | D) . A = L . A ) by A24, A34, FUNCT_1:49;
ex J being T-Sequence st
( J = G . A & F . A = F2(J) ) by A18, A19, A34, Th10;
hence (L | D) . a = K . a by A11, A22, A34, A35; ::_thesis: verum
end;
D c= dom L by A18, A19, Def2;
then dom (L | D) = D by RELAT_1:62;
hence L . D = F2((L | D)) by A21, A23, A33, FUNCT_1:2; ::_thesis: verum
end;
for A being Ordinal holds S1[A] from ORDINAL1:sch_2(A1);
then consider L being T-Sequence such that
A36: dom L = F1() and
A37: for B being Ordinal st B in F1() holds
L . B = F2((L | B)) ;
take L ; ::_thesis: ( dom L = F1() & ( for B being Ordinal
for L1 being T-Sequence st B in F1() & L1 = L | B holds
L . B = F2(L1) ) )
thus dom L = F1() by A36; ::_thesis: for B being Ordinal
for L1 being T-Sequence st B in F1() & L1 = L | B holds
L . B = F2(L1)
let B be Ordinal; ::_thesis: for L1 being T-Sequence st B in F1() & L1 = L | B holds
L . B = F2(L1)
let L1 be T-Sequence; ::_thesis: ( B in F1() & L1 = L | B implies L . B = F2(L1) )
assume ( B in F1() & L1 = L | B ) ; ::_thesis: L . B = F2(L1)
hence L . B = F2(L1) by A37; ::_thesis: verum
end;
scheme :: ORDINAL1:sch 5
FuncTS{ F1() -> T-Sequence, F2( Ordinal) -> set , F3( T-Sequence) -> set } :
for B being Ordinal st B in dom F1() holds
F1() . B = F3((F1() | B))
provided
A1: for A being Ordinal
for a being set holds
( a = F2(A) iff ex L being T-Sequence st
( a = F3(L) & dom L = A & ( for B being Ordinal st B in A holds
L . B = F3((L | B)) ) ) ) and
A2: for A being Ordinal st A in dom F1() holds
F1() . A = F2(A)
proof
consider L being T-Sequence such that
F2((dom F1())) = F3(L) and
A3: dom L = dom F1() and
A4: for B being Ordinal st B in dom F1() holds
L . B = F3((L | B)) by A1;
now__::_thesis:_for_b_being_set_st_b_in_dom_L_holds_
F1()_._b_=_L_._b
let b be set ; ::_thesis: ( b in dom L implies F1() . b = L . b )
assume A5: b in dom L ; ::_thesis: F1() . b = L . b
then reconsider B = b as Ordinal by Th13;
now__::_thesis:_ex_K_being_number_st_
(_F3((L_|_B))_=_F3(K)_&_dom_K_=_B_&_(_for_C_being_Ordinal_st_C_in_B_holds_
K_._C_=_F3((K_|_C))_)_)
take K = L | B; ::_thesis: ( F3((L | B)) = F3(K) & dom K = B & ( for C being Ordinal st C in B holds
K . C = F3((K | C)) ) )
thus F3((L | B)) = F3(K) ; ::_thesis: ( dom K = B & ( for C being Ordinal st C in B holds
K . C = F3((K | C)) ) )
A6: B c= dom L by A5, Def2;
hence dom K = B by RELAT_1:62; ::_thesis: for C being Ordinal st C in B holds
K . C = F3((K | C))
let C be Ordinal; ::_thesis: ( C in B implies K . C = F3((K | C)) )
assume A7: C in B ; ::_thesis: K . C = F3((K | C))
then C c= B by Def2;
then A8: L | C = K | C by FUNCT_1:51;
K . C = L . C by A7, FUNCT_1:49;
hence K . C = F3((K | C)) by A3, A4, A6, A7, A8; ::_thesis: verum
end;
then F2(B) = F3((L | B)) by A1
.= L . B by A3, A4, A5 ;
hence F1() . b = L . b by A2, A3, A5; ::_thesis: verum
end;
then F1() = L by A3, FUNCT_1:2;
hence for B being Ordinal st B in dom F1() holds
F1() . B = F3((F1() | B)) by A4; ::_thesis: verum
end;
theorem :: ORDINAL1:35
for A, B being Ordinal holds
( A c< B or A = B or B c< A )
proof
let A, B be Ordinal; ::_thesis: ( A c< B or A = B or B c< A )
assume that
A1: ( not A c< B & not A = B ) and
A2: not B c< A ; ::_thesis: contradiction
not A c= B by A1, XBOOLE_0:def_8;
hence contradiction by A2, XBOOLE_0:def_8; ::_thesis: verum
end;
begin
definition
let X be set ;
func On X -> set means :Def9: :: ORDINAL1:def 9
for x being set holds
( x in it iff ( x in X & x is Ordinal ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in X & x is Ordinal ) )
proof
defpred S1[ set ] means $1 is Ordinal;
thus ex Y being set st
for x being set holds
( x in Y iff ( x in X & S1[x] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in X & x is Ordinal ) ) ) & ( for x being set holds
( x in b2 iff ( x in X & x is Ordinal ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ( $1 in X & $1 is Ordinal );
let Y, Z be set ; ::_thesis: ( ( for x being set holds
( x in Y iff ( x in X & x is Ordinal ) ) ) & ( for x being set holds
( x in Z iff ( x in X & x is Ordinal ) ) ) implies Y = Z )
assume that
A1: for x being set holds
( x in Y iff S1[x] ) and
A2: for x being set holds
( x in Z iff S1[x] ) ; ::_thesis: Y = Z
thus Y = Z from XBOOLE_0:sch_2(A1, A2); ::_thesis: verum
end;
func Lim X -> set means :: ORDINAL1:def 10
for x being set holds
( x in it iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) )
proof
defpred S1[ set ] means ex A being Ordinal st
( $1 = A & A is limit_ordinal );
thus ex Y being set st
for x being set holds
( x in Y iff ( x in X & S1[x] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) ) ) & ( for x being set holds
( x in b2 iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ( $1 in X & ex A being Ordinal st
( $1 = A & A is limit_ordinal ) );
let Y, Z be set ; ::_thesis: ( ( for x being set holds
( x in Y iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) ) ) & ( for x being set holds
( x in Z iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) ) ) implies Y = Z )
assume that
A3: for x being set holds
( x in Y iff S1[x] ) and
A4: for x being set holds
( x in Z iff S1[x] ) ; ::_thesis: Y = Z
thus Y = Z from XBOOLE_0:sch_2(A3, A4); ::_thesis: verum
end;
end;
:: deftheorem Def9 defines On ORDINAL1:def_9_:_
for X, b2 being set holds
( b2 = On X iff for x being set holds
( x in b2 iff ( x in X & x is Ordinal ) ) );
:: deftheorem defines Lim ORDINAL1:def_10_:_
for X, b2 being set holds
( b2 = Lim X iff for x being set holds
( x in b2 iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) ) );
theorem Th36: :: ORDINAL1:36
for D being Ordinal ex A being Ordinal st
( D in A & A is limit_ordinal )
proof
let D be Ordinal; ::_thesis: ex A being Ordinal st
( D in A & A is limit_ordinal )
consider Field being set such that
A1: D in Field and
A2: for X, Y being set st X in Field & Y c= X holds
Y in Field and
A3: for X being set st X in Field holds
bool X in Field and
for X being set holds
( not X c= Field or X,Field are_equipotent or X in Field ) by ZFMISC_1:112;
for X being set st X in On Field holds
( X is Ordinal & X c= On Field )
proof
let X be set ; ::_thesis: ( X in On Field implies ( X is Ordinal & X c= On Field ) )
assume A4: X in On Field ; ::_thesis: ( X is Ordinal & X c= On Field )
then reconsider A = X as Ordinal by Def9;
A5: A in Field by A4, Def9;
thus X is Ordinal by A4, Def9; ::_thesis: X c= On Field
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X or y in On Field )
assume A6: y in X ; ::_thesis: y in On Field
then y in A ;
then reconsider B = y as Ordinal by Th13;
B c= A by A6, Def2;
then B in Field by A2, A5;
hence y in On Field by Def9; ::_thesis: verum
end;
then reconsider ON = On Field as Ordinal by Th19;
take ON ; ::_thesis: ( D in ON & ON is limit_ordinal )
thus D in ON by A1, Def9; ::_thesis: ON is limit_ordinal
for A being Ordinal st A in ON holds
succ A in ON
proof
let A be Ordinal; ::_thesis: ( A in ON implies succ A in ON )
A7: succ A c= bool A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in succ A or x in bool A )
assume x in succ A ; ::_thesis: x in bool A
then ( x in A or x = A ) by Th8;
then x c= A by Def2;
hence x in bool A ; ::_thesis: verum
end;
assume A in ON ; ::_thesis: succ A in ON
then A in Field by Def9;
then bool A in Field by A3;
then succ A in Field by A2, A7;
hence succ A in ON by Def9; ::_thesis: verum
end;
hence ON is limit_ordinal by Th28; ::_thesis: verum
end;
definition
func omega -> set means :Def11: :: ORDINAL1:def 11
( {} in it & it is limit_ordinal & it is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
it c= A ) );
existence
ex b1 being set st
( {} in b1 & b1 is limit_ordinal & b1 is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
b1 c= A ) )
proof
defpred S1[ Ordinal] means ( {} in $1 & $1 is limit_ordinal );
A1: ex A being Ordinal st S1[A] by Th36;
ex C being Ordinal st
( S1[C] & ( for A being Ordinal st S1[A] holds
C c= A ) ) from ORDINAL1:sch_1(A1);
hence ex b1 being set st
( {} in b1 & b1 is limit_ordinal & b1 is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
b1 c= A ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st {} in b1 & b1 is limit_ordinal & b1 is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
b1 c= A ) & {} in b2 & b2 is limit_ordinal & b2 is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
b2 c= A ) holds
b1 = b2
proof
let B, C be set ; ::_thesis: ( {} in B & B is limit_ordinal & B is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
B c= A ) & {} in C & C is limit_ordinal & C is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
C c= A ) implies B = C )
assume ( {} in B & B is limit_ordinal & B is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
B c= A ) & {} in C & C is limit_ordinal & C is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal 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 Def11 defines omega ORDINAL1:def_11_:_
for b1 being set holds
( b1 = omega iff ( {} in b1 & b1 is limit_ordinal & b1 is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
b1 c= A ) ) );
registration
cluster omega -> non empty ordinal ;
coherence
( not omega is empty & omega is ordinal ) by Def11;
end;
definition
let A be set ;
attrA is natural means :Def12: :: ORDINAL1:def 12
A in omega ;
end;
:: deftheorem Def12 defines natural ORDINAL1:def_12_:_
for A being set holds
( A is natural iff A in omega );
registration
cluster natural for number ;
existence
ex b1 being number st b1 is natural
proof
take n = the Element of omega ; ::_thesis: n is natural
thus n in omega ; :: according to ORDINAL1:def_12 ::_thesis: verum
end;
end;
definition
mode Nat is natural number ;
end;
registration
natural number ex b1 being number st
for b2 being natural number holds b2 in b1
proof
take omega ; ::_thesis: for b1 being natural number holds b1 in omega
let y be Nat; ::_thesis: y in omega
thus y in omega by Def12; ::_thesis: verum
end;
end;
registration
let A be Ordinal;
cluster -> ordinal for Element of A;
coherence
for b1 being Element of A holds b1 is ordinal
proof
let x be Element of A; ::_thesis: x is ordinal
( A is empty or not A is empty ) ;
hence x is ordinal by Th13, SUBSET_1:def_1; ::_thesis: verum
end;
end;
registration
cluster natural -> ordinal for number ;
coherence
for b1 being number st b1 is natural holds
b1 is ordinal
proof
let n be number ; ::_thesis: ( n is natural implies n is ordinal )
assume n is natural ; ::_thesis: n is ordinal
then reconsider n = n as Element of omega by Def12;
n is ordinal ;
hence n is ordinal ; ::_thesis: verum
end;
end;
scheme :: ORDINAL1:sch 6
ALFA{ F1() -> non empty set , P1[ set , set ] } :
ex F being Function st
( dom F = F1() & ( for d being Element of F1() ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) ) ) )
provided
A1: for d being Element of F1() ex A being Ordinal st P1[d,A]
proof
defpred S1[ set , set ] means ex A being Ordinal st
( A = $2 & P1[$1,A] & ( for B being Ordinal st P1[$1,B] holds
A c= B ) );
A2: for x being set st x in F1() holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in F1() implies ex y being set st S1[x,y] )
assume x in F1() ; ::_thesis: ex y being set st S1[x,y]
then reconsider d = x as Element of F1() ;
defpred S2[ Ordinal] means P1[d,$1];
A3: ex A being Ordinal st S2[A] by A1;
consider A being Ordinal such that
A4: ( S2[A] & ( for B being Ordinal st S2[B] holds
A c= B ) ) from ORDINAL1:sch_1(A3);
reconsider y = A as set ;
take y ; ::_thesis: S1[x,y]
take A ; ::_thesis: ( A = y & P1[x,A] & ( for B being Ordinal st P1[x,B] holds
A c= B ) )
thus ( A = y & P1[x,A] & ( for B being Ordinal st P1[x,B] holds
A c= B ) ) by A4; ::_thesis: verum
end;
A5: for x, y, z being set st x in F1() & S1[x,y] & S1[x,z] holds
y = z
proof
let x, y, z be set ; ::_thesis: ( x in F1() & S1[x,y] & S1[x,z] implies y = z )
assume x in F1() ; ::_thesis: ( not S1[x,y] or not S1[x,z] or y = z )
given A1 being Ordinal such that A6: A1 = y and
A7: ( P1[x,A1] & ( for B being Ordinal st P1[x,B] holds
A1 c= B ) ) ; ::_thesis: ( not S1[x,z] or y = z )
given A2 being Ordinal such that A8: A2 = z and
A9: ( P1[x,A2] & ( for B being Ordinal st P1[x,B] holds
A2 c= B ) ) ; ::_thesis: y = z
( A1 c= A2 & A2 c= A1 ) by A7, A9;
hence y = z by A6, A8, XBOOLE_0:def_10; ::_thesis: verum
end;
consider F being Function such that
A10: ( dom F = F1() & ( for x being set st x in F1() holds
S1[x,F . x] ) ) from FUNCT_1:sch_2(A5, A2);
take F ; ::_thesis: ( dom F = F1() & ( for d being Element of F1() ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) ) ) )
thus dom F = F1() by A10; ::_thesis: for d being Element of F1() ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) )
let d be Element of F1(); ::_thesis: ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) )
thus ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) ) by A10; ::_thesis: verum
end;
theorem :: ORDINAL1:37
for X being set holds (succ X) \ {X} = X
proof
let X be set ; ::_thesis: (succ X) \ {X} = X
thus (succ X) \ {X} c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= (succ X) \ {X}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (succ X) \ {X} or x in X )
assume A1: x in (succ X) \ {X} ; ::_thesis: x in X
then A2: not x in {X} by XBOOLE_0:def_5;
( x in X or x = X ) by A1, Th8;
hence x in X by A2, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in (succ X) \ {X} )
assume A3: x in X ; ::_thesis: x in (succ X) \ {X}
then x <> X ;
then A4: not x in {X} by TARSKI:def_1;
x in succ X by A3, Th8;
hence x in (succ X) \ {X} by A4, XBOOLE_0:def_5; ::_thesis: verum
end;
registration
cluster empty -> natural for number ;
coherence
for b1 being number st b1 is empty holds
b1 is natural
proof
{} in omega by Def11;
hence for b1 being number st b1 is empty holds
b1 is natural by Def12; ::_thesis: verum
end;
cluster -> natural for Element of omega ;
coherence
for b1 being Element of omega holds b1 is natural by Def12;
end;
registration
cluster non empty natural for number ;
existence
ex b1 being number st
( not b1 is empty & b1 is natural )
proof
take succ {} ; ::_thesis: ( not succ {} is empty & succ {} is natural )
thus not succ {} is empty ; ::_thesis: succ {} is natural
( omega is limit_ordinal & {} in omega ) by Def11;
hence succ {} in omega by Th28; :: according to ORDINAL1:def_12 ::_thesis: verum
end;
end;
registration
let a be natural Ordinal;
cluster succ a -> natural ;
coherence
succ a is natural
proof
( omega is limit_ordinal & a in omega ) by Def11, Def12;
hence succ a in omega by Th28; :: according to ORDINAL1:def_12 ::_thesis: verum
end;
end;
registration
cluster empty -> c=-linear for number ;
coherence
for b1 being set st b1 is empty holds
b1 is c=-linear
proof
let X be set ; ::_thesis: ( X is empty implies X is c=-linear )
assume A1: X is empty ; ::_thesis: X is c=-linear
let x be set ; :: according to ORDINAL1:def_8 ::_thesis: for y being set st x in X & y in X holds
x,y are_c=-comparable
thus for y being set st x in X & y in X holds
x,y are_c=-comparable by A1; ::_thesis: verum
end;
end;
registration
let X be c=-linear set ;
cluster -> c=-linear for Element of bool X;
coherence
for b1 being Subset of X holds b1 is c=-linear
proof
let Y be Subset of X; ::_thesis: Y is c=-linear
let x, y be set ; :: according to ORDINAL1:def_8 ::_thesis: ( x in Y & y in Y implies x,y are_c=-comparable )
assume ( x in Y & y in Y ) ; ::_thesis: x,y are_c=-comparable
hence x,y are_c=-comparable by Def8; ::_thesis: verum
end;
end;