Copyright (c) 1989 Association of Mizar Users
environ
vocabulary BOOLE, ZFMISC_1, TARSKI, FUNCT_1, RELAT_1, ORDINAL1, HAHNBAN,
ARYTM;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1;
constructors TARSKI, ENUMSET1, FUNCT_1, SUBSET_1, XBOOLE_0;
clusters FUNCT_1, RELAT_1, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1;
theorems TARSKI, XBOOLE_0, FUNCT_1, ZFMISC_1, ENUMSET1, RELAT_1, XBOOLE_1;
schemes XBOOLE_0, FUNCT_1;
begin
::
:: 1. Some consequences of regularity axiom (TARSKI:7)
::
reserve X,Y,Z,X1,X2,X3,X4,X5,X6,x,y for set;
canceled 2;
theorem
Th3: not ( X in Y & Y in Z & Z in X)
proof
A1: X in { X,Y,Z } & Y in { X,Y,Z } & Z in { X,Y,Z } by ENUMSET1:14;
then consider T being set such that
A2: T in { X,Y,Z } and
A3: not ex x st x in { X,Y,Z } & x in T by TARSKI:7;
T = X or T = Y or T = Z by A2,ENUMSET1:13;
hence thesis by A1,A3;
end;
theorem
not ( X1 in X2 & X2 in X3 & X3 in X4 & X4 in X1)
proof
A1: X1 in { X1,X2,X3,X4 } & X2 in { X1,X2,X3,X4 } &
X3 in { X1,X2,X3,X4 } & X4 in { X1,X2,X3,X4 } by ENUMSET1:19;
then consider T being set such that
A2: T in { X1,X2,X3,X4 } and
A3: not ex x st x in { X1,X2,X3,X4 } & x in T by TARSKI:7;
T = X1 or T = X2 or T = X3 or T = X4 by A2,ENUMSET1:18;
hence thesis by A1,A3;
end;
theorem
not ( X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X1)
proof assume
A1: X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X1;
set Z = { X1,X2,X3,X4,X5 };
A2: X1 in { X1,X2,X3,X4,X5 } by ENUMSET1:24;
for Y st Y in Z ex y st y in Z & y in Y
proof let Y such that
A3: Y in Z;
A4: Y in { X1,X2,X3,X4,X5 }
implies Y = X1 or Y = X2 or Y = X3 or Y = X4 or Y = X5
by ENUMSET1:23;
now per cases by A3,A4;
suppose
A5: Y = X1;
take y = X5;
thus y in Z & y in Y by A1,A5,ENUMSET1:24;
suppose
A6: Y = X2;
take y = X1;
thus y in Z & y in Y by A1,A6,ENUMSET1:24;
suppose
A7: Y = X3;
take y = X2;
thus y in Z & y in Y by A1,A7,ENUMSET1:24;
suppose
A8: Y = X4;
take y = X3;
thus y in Z & y in Y by A1,A8,ENUMSET1:24;
suppose
A9: Y = X5;
take y = X4;
thus y in Z & y in Y by A1,A9,ENUMSET1:24;
end;
hence thesis;
end;
hence contradiction by A2,TARSKI:7;
end;
theorem
not ( X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X6 & X6 in X1)
proof assume
A1: X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X6 & X6 in X1;
set Z = { X1,X2,X3,X4,X5,X6 };
A2: X1 in { X1,X2,X3,X4,X5,X6 } by ENUMSET1:29;
for Y st Y in Z ex y st y in Z & y in Y
proof let Y such that
A3: Y in Z;
A4: Y in { X1,X2,X3,X4,X5,X6 }
implies Y = X1 or Y = X2 or Y = X3 or Y = X4 or Y = X5 or Y = X6
by ENUMSET1:28;
now per cases by A3,A4;
suppose
A5: Y = X1;
take y = X6;
thus y in Z & y in Y by A1,A5,ENUMSET1:29;
suppose
A6: Y = X2;
take y = X1;
thus y in Z & y in Y by A1,A6,ENUMSET1:29;
suppose
A7: Y = X3;
take y = X2;
thus y in Z & y in Y by A1,A7,ENUMSET1:29;
suppose
A8: Y = X4;
take y = X3;
thus y in Z & y in Y by A1,A8,ENUMSET1:29;
suppose
A9: Y = X5;
take y = X4;
thus y in Z & y in Y by A1,A9,ENUMSET1:29;
suppose
A10: Y = X6;
take y = X5;
thus y in Z & y in Y by A1,A10,ENUMSET1:29;
end;
hence thesis;
end;
hence contradiction by A2,TARSKI:7;
end;
theorem
Th7: Y in X implies not X c= Y
proof assume
A1: Y in X;
assume X c= Y;
then Y in Y by A1;
hence contradiction;
end;
definition let X;
func succ X -> set equals
:Def1: X \/ { X };
coherence;
end;
definition let X;
cluster succ X -> non empty;
coherence
proof
succ X = X \/ { X } & X in { X } by Def1,TARSKI:def 1;
hence thesis by XBOOLE_0:def 2;
end;
end;
canceled 2;
theorem
Th10: X in succ X
proof
X in { X } by TARSKI:def 1;
then X in X \/ { X } by XBOOLE_0:def 2;
hence X in succ X by Def1;
end;
canceled;
theorem
succ X = succ Y implies X = Y
proof
assume that
A1: succ X = succ Y and
A2: X <> Y;
X in succ X by Th10;
then X in Y \/ { Y } by A1,Def1;
then A3: X in Y or X in { Y } by XBOOLE_0:def 2;
Y in succ Y by Th10;
then Y in X \/ { X } by A1,Def1;
then Y in X or Y in { X } by XBOOLE_0:def 2;
hence contradiction by A2,A3,TARSKI:def 1;
end;
theorem
x in succ X iff x in X or x = X
proof
thus x in succ X implies x in X or x = X
proof assume x in succ X;
then x in X \/ { X } by Def1;
then x in X or x in { X } by XBOOLE_0:def 2;
hence thesis by TARSKI:def 1;
end;
assume x in X or x = X;
then x in X or x in { X } by TARSKI:def 1;
then x in X \/ { X } by XBOOLE_0:def 2;
hence thesis by Def1;
end;
theorem
Th14: X <> succ X
proof assume
A1: X = succ X;
X in succ X by Th10;
hence contradiction by A1;
end;
::
:: 3. epsilon-transitivity & epsilon-connectedness
::
reserve a,b,c,X,Y,Z,x,y,z for set;
definition let X;
attr X is epsilon-transitive means
:Def2: for x st x in X holds x c= X;
attr X is epsilon-connected means
:Def3: for x,y st x in X & y in X holds x in y or x = y or y in x;
end;
Lm1: {} is epsilon-transitive & {} is epsilon-connected
proof
thus x in {} implies x c= {};
thus x in {} & y in {} implies x in y or x = y or y in x;
end;
::
:: 4. Definition of ordinal numbers - Ordinal
::
definition let IT be set;
attr IT is ordinal means
:Def4: IT is epsilon-transitive epsilon-connected;
end;
definition
cluster ordinal -> epsilon-transitive epsilon-connected set;
coherence by Def4;
cluster epsilon-transitive epsilon-connected -> ordinal set;
coherence by Def4;
end;
definition
redefine mode set;
synonym number;
end;
definition
cluster ordinal number;
existence proof take {}; thus thesis by Def4,Lm1; end;
end;
definition
mode Ordinal is ordinal number;
end;
reserve A,B,C,D for Ordinal;
canceled 4;
theorem Th19:
for A being epsilon-transitive set st
A in B & B in C holds A in C
proof
let A be epsilon-transitive set;
assume
A1: A in B & B in C;
then B c= C by Def2;
hence A in C by A1;
end;
canceled;
theorem Th21:
for x being epsilon-transitive set, A being Ordinal
st x c< A holds x in A
proof let x be epsilon-transitive set, A be Ordinal;
assume
A1: x c< A;
then A2: x c= A by XBOOLE_0:def 8;
consider a being Element of A \ x;
A \ x <> {}
proof
assume A \ x = {};
then A c= x by XBOOLE_1:37;
hence contradiction by A1,XBOOLE_1:60;
end;
then a in A \ x;
then consider y such that
A3: y in A \ x and
A4: not ex a st a in A \ x & a in y by TARSKI:7;
A5: y in A & not y in x by A3,XBOOLE_0:def 4;
then A6: y c= A by Def2;
now let a;
assume
A7: a in y;
then not a in A \ x by A4; hence a in x by A6,A7,XBOOLE_0:def 4;
end;
then A8: y c= x by TARSKI:def 3;
now let a;
assume a in x;
then consider z such that
A9: z = a & z in x;
z c= x by A9,Def2;
then not y in z by A3,XBOOLE_0:def 4;
hence a in y by A2,A5,A9,Def3;
end;
then x c= y by TARSKI:def 3;
hence thesis by A5,A8,XBOOLE_0:def 10;
end;
theorem
for A being epsilon-transitive set,
B, C being Ordinal st
A c= B & B in C holds A in C
proof
let A be epsilon-transitive set,
B, C be Ordinal;
assume
A1: A c= B & B in C;
then B c= C by Def2;
then A c= C & A <> C by A1,Th7,XBOOLE_1:1;
then A c< C by XBOOLE_0:def 8;
hence thesis by Th21;
end;
theorem
Th23: a in A implies a is Ordinal
proof assume
A1: a in A;
then A2: a c= A by Def2;
then for y,z st y in a & z in a holds y in z or y = z or z in
y by Def3;
then A3: a is epsilon-connected by Def3;
now let y; assume
A4: y in a;
assume not y c= a;
then consider b such that
A5: b in y & not b in a by TARSKI:def 3;
b in y \ a by A5,XBOOLE_0:def 4;
then consider z such that
A6: z in y \ a & not ex c st c in y \ a & c in z by TARSKI:7;
A7: z in y & not z in a by A6,XBOOLE_0:def 4;
y c= A by A2,A4,Def2;
then z in a or z = a or a in z by A1,A7,Def3;
hence contradiction by A4,A7,Th3;
end;
then a is epsilon-transitive by Def2;
hence thesis by A3,Def4;
end;
theorem
Th24: A in B or A = B or B in A
proof assume
A1: not A in B & A <> B;
then not A c< B by Th21;
then not A c= B by A1,XBOOLE_0:def 8;
then consider a such that
A2: a in A & not a in B by TARSKI:def 3;
a in A \ B by A2,XBOOLE_0:def 4;
then consider X such that
A3: X in A \ B & not ex a st a in A \ B & a in X by TARSKI:7;
A4: X in A & not X in B by A3,XBOOLE_0:def 4;
then A5: X c= A by Def2;
A6: X is Ordinal by A4,Th23;
now let b;
assume
A7: b in X;
then not b in A \ B by A3;
hence b in B by A5,A7,XBOOLE_0:def 4;
end;
then X c= B by TARSKI:def 3;
then X c< B or X = B by XBOOLE_0:def 8;
hence thesis by A4,A6,Th21;
end;
definition let A,B;
redefine pred A c= B;
connectedness
proof let A,B;
A in B or A = B or B in A by Th24;
hence thesis by Def2;
end;
end;
theorem
A,B are_c=-comparable
proof
A c= B or B c= A;
hence thesis by XBOOLE_0:def 9;
end;
theorem
Th26: A c= B or B in A
proof
A in B or A = B or B in A by Th24;
hence thesis by Def2;
end;
theorem
Th27: {} is Ordinal by Def4,Lm1;
definition
cluster empty Ordinal;
existence by Th27;
end;
definition
cluster empty -> ordinal number;
coherence by Def4,Lm1;
end;
definition
cluster {} -> ordinal;
coherence;
end;
canceled;
theorem
Th29: x is Ordinal implies succ x is Ordinal
proof
assume
A1: x is Ordinal;
A2: succ x = x \/ { x } by Def1;
A3: now let y;
assume
A4: y in succ x;
y in { x } implies y = x by TARSKI:def 1;
hence y in x or y = x by A2,A4,XBOOLE_0:def 2;
end;
now let y;
assume A5: y in succ x;
A6: now assume y in x;
then A7: y c= x by A1,Def2;
x c= x \/ { x } by XBOOLE_1:7;
hence y c= succ x by A2,A7,XBOOLE_1:1;
end;
y = x implies y c= succ x by A2,XBOOLE_1:7;
hence y c= succ x by A3,A5,A6;
end;
then A8: succ x is epsilon-transitive by Def2;
now let y,z;
assume
A9: y in succ x & z in succ x;
then A10: y in x or y = x by A3;
z in x or z = x by A3,A9;
hence y in z or y = z or z in y by A1,A10,Def3;
end;
then succ x is epsilon-connected by Def3;
hence thesis by A8,Def4;
end;
theorem
Th30: x is ordinal implies union x is ordinal
proof assume
x is epsilon-transitive & x is epsilon-connected;
then reconsider A = x as Ordinal by Def4;
thus y in union x implies y c= union x
proof assume y in union x;
then consider z such that
A1: y in z & z in x by TARSKI:def 4;
z in A by A1;
then reconsider z as Ordinal by Th23;
z c= A by A1,Def2; hence thesis by A1,ZFMISC_1:92;
end;
let y,z; assume
A2: y in union x & z in union x;
then consider X such that
A3: y in X & X in x by TARSKI:def 4;
consider Y such that
A4: z in Y & Y in x by A2,TARSKI:def 4;
X in A & Y in A by A3,A4;
then reconsider X,Y as Ordinal by Th23;
y in X & z in Y by A3,A4;
then y is Ordinal & z is Ordinal by Th23;
hence thesis by Th24;
end;
definition
cluster non empty Ordinal;
existence
proof
reconsider A = succ {} as Ordinal by Th29;
take A; thus thesis;
end;
end;
definition let A;
cluster succ A -> non empty ordinal;
coherence by Th29;
cluster union A -> ordinal;
coherence by Th30;
end;
theorem
(for x st x in X holds x is Ordinal & x c= X) implies X is ordinal
proof assume
A1: for x st x in X holds x is Ordinal & x c= X;
thus X is epsilon-transitive
proof let x; assume x in X; hence x c= X by A1;
end;
let x,y; assume
x in X & y in X;
then x is Ordinal & y is Ordinal by A1;
hence x in y or x = y or y in x by Th24;
end;
theorem
Th32: X c= A & X <> {} implies ex C st C in X & for B st B in X holds C c= B
proof
consider a being Element of X;
assume
A1: X c= A & X <> {};
then a in X;
then consider Y such that
A2: Y in X & not ex a st a in X & a in Y by TARSKI:7;
Y is Ordinal by A1,A2,Th23;
then consider C such that
A3: C = Y;
take C;
thus C in X by A2,A3;
let B;
assume
B in X;
then not B in C by A2,A3;
then B = C or C in B by Th24;
hence C c= B by Def2;
end;
theorem
Th33: A in B iff succ A c= B
proof
thus A in B implies succ A c= B
proof assume
A1: A in B;
then A2: A c= B by Def2;
a in { A } implies a in B by A1,TARSKI:def 1;
then { A } c= B by TARSKI:def 3;
then A \/ { A } c= B by A2,XBOOLE_1:8;
hence thesis by Def1;
end;
assume
A3: succ A c= B;
A in succ A by Th10;
hence thesis by A3;
end;
theorem
Th34: A in succ C iff A c= C
proof
thus A in succ C implies A c= C
proof assume
A in succ C;
then A in C \/ { C } by Def1;
then A in C or A in { C } by XBOOLE_0:def 2;
hence thesis by Def2,TARSKI:def 1;
end;
assume
A1: A c= C;
assume not A in succ C;
then A2: A = succ C or succ C in A by Th24;
C in succ C by Th10;
then A3: C c= succ C by Def2;
succ C c= C by A1,A2,Def2;
then succ C = C by A3,XBOOLE_0:def 10;
hence contradiction by Th14;
end;
::
:: 6. Transfinite induction and principle of minimum of ordinals
::
scheme Ordinal_Min { P[Ordinal] } :
ex A st P[A] & for B st P[B] holds A c= B provided
A1: ex A st P[A]
proof
consider A such that
A2: P[A] by A1;
defpred R[set] means ex B st $1 = B & P[B];
consider X such that
A3: x in X iff x in succ A & R[x] from Separation;
A in succ A by Th10;
then A4: X <> {} by A2,A3;
for a holds
a in X implies a in succ A by A3;
then X c= succ A by TARSKI:def 3;
then consider C such that
A5: C in X & for B st B in X holds C c= B by A4,Th32;
take C;
ex B st C = B & P[B] by A3,A5;
hence P[C];
let B; assume
A6: P[B];
assume
A7: not C c= B;
then B c= C & B <> C;
then B c< C by XBOOLE_0:def 8;
then A8: B in C by Th21;
C in succ A by A3,A5;
then C c= succ A by Def2;
then B in X by A3,A6,A8;
hence contradiction by A5,A7;
end;
scheme Transfinite_Ind { P[Ordinal] } :
for A holds P[A] provided
A1: for A st for C st C in A holds P[C] holds P[A]
proof let A;
set Y = succ A;
defpred R[set] means ex B st $1 = B & P[B];
consider Z such that
A2: x in Z iff x in Y & R[x] from Separation;
A3: Y \ Z c= Y by XBOOLE_1:36;
now assume Y \ Z <> {};
then consider C such that
A4: C in Y \ Z & for B st B in Y \ Z holds C c= B by A3,Th32;
A5: C in Y & not C in Z by A4,XBOOLE_0:def 4;
now let B such that
A6: B in C;
A7: C c= Y by A5,Def2;
now assume not B in Z;
then B in Y \ Z by A6,A7,XBOOLE_0:def 4;
then A8: C c= B by A4;
C <> B by A6;
then C c< B by A8,XBOOLE_0:def 8;
hence contradiction by A6,Th21;
end;
then ex B' being Ordinal st B = B' & P[B'] by A2;
hence P[B];
end;
then P[C] by A1;
hence contradiction by A2,A5;
end;
then not A in Y or A in Z by XBOOLE_0:def 4;
then ex B st A = B & P[B] by A2,Th10;
hence thesis;
end;
::
:: 7. Properties of sets of ordinals
::
theorem
Th35: for X st for a st a in X holds a is Ordinal holds union X is ordinal
proof let X such that
A1: for a st a in X holds a is Ordinal;
thus union X is epsilon-transitive
proof let x; assume
x in union X;
then consider Y such that
A2: x in Y & Y in X by TARSKI:def 4;
Y is Ordinal by A1,A2;
then A3: x c= Y by A2,Def2;
let a; assume a in x; hence a in union X by A2,A3,TARSKI:def 4;
end;
let x,y; assume
A4: x in union X & y in union X;
then consider Y such that
A5: x in Y & Y in X by TARSKI:def 4;
consider Z such that
A6: y in Z & Z in X by A4,TARSKI:def 4;
Y is Ordinal & Z is Ordinal by A1,A5,A6;
then x is Ordinal & y is Ordinal by A5,A6,Th23;
hence thesis by Th24;
end;
theorem
Th36: for X st for a st a in X holds a is Ordinal ex A st X c= A
proof let X; assume
A1: for a st a in X holds a is Ordinal;
then A2: union X is Ordinal by Th35;
then reconsider A = succ(union X) as Ordinal by Th29;
take A;
let a; assume
A3: a in X;
then reconsider B = a as Ordinal by A1;
b in B implies b in union X by A3,TARSKI:def 4;
then B c= union X by TARSKI:def 3;
hence thesis by A2,Th34;
end;
theorem
Th37: not ex X st for x holds x in X iff x is Ordinal
proof given X such that
A1: for x holds x in X iff x is Ordinal;
A2: X is epsilon-transitive
proof let x; assume
x in X;
then A3: x is Ordinal by A1;
thus thesis
proof let a;
assume a in x;
then a is Ordinal by A3,Th23;
hence thesis by A1;
end;
end;
X is epsilon-connected
proof let x,y; assume
x in X & y in X;
then x is Ordinal & y is Ordinal by A1;
hence thesis by Th24;
end;
then X is Ordinal by A2,Def4;
then X in X by A1;
hence contradiction;
end;
theorem
Th38: not ex X st for A holds A in X
proof given X such that
A1: A in X;
defpred P[set] means $1 is Ordinal;
consider Y such that
A2: a in Y iff a in X & P[a] from Separation;
now let x; assume
A3: x is Ordinal;
then x in X by A1;
hence x in Y by A2,A3;
end;
then x in Y iff x is Ordinal by A2;
hence contradiction by Th37;
end;
theorem
for X ex A st not A in X & for B st not B in X holds A c= B
proof let X;
consider B such that
A1: not B in X by Th38;
defpred P[set] means not $1 in X;
consider Y such that
A2: a in Y iff a in succ B & P[a] from Separation;
for a holds
a in Y implies a in succ B by A2;
then A3: Y c= succ B by TARSKI:def 3;
B in succ B by Th10;
then Y <> {} by A1,A2;
then consider A such that
A4: A in Y & for B st B in Y holds A c= B by A3,Th32;
take A;
thus not A in X by A2,A4;
let C; assume
A5: not C in X;
assume
A6: not A c= C;
then not A in C by Def2;
then A7: C in A by A6,Th24;
A in succ B by A2,A4;
then A c= succ B by Def2;
then C in Y by A2,A5,A7;
hence contradiction by A4,A6;
end;
::
:: 8. Limit ordinals
::
definition let A be set;
canceled;
attr A is being_limit_ordinal means
:Def6: A = union A;
synonym A is_limit_ordinal;
end;
canceled;
theorem
Th41: for A holds A is_limit_ordinal iff for C st C in A holds succ C in A
proof let A;
thus A is_limit_ordinal implies for C st C in A holds succ C in A
proof assume
A is_limit_ordinal;
then A1: A = union A by Def6;
let C; assume
C in A;
then consider z such that
A2: C in z & z in A by A1,TARSKI:def 4;
for b holds b in { C } implies b in z by A2,TARSKI:def 1;
then A3: { C } c= z by TARSKI:def 3;
A4: z is Ordinal by A2,Th23;
then C c= z by A2,Def2;
then C \/ { C } c= z by A3,XBOOLE_1:8;
then succ C c= z by Def1;
then succ C = z or succ C c< z by XBOOLE_0:def 8;
then A5: succ C = z or succ C in z by A4,Th21;
z c= A by A2,Def2;
hence thesis by A2,A5;
end;
assume
A6: for C st C in A holds succ C in A;
now let a;
assume
A7: a in A;
then a is Ordinal by Th23;
then A8: succ a in A by A6,A7;
a in succ a by Th10;
hence a in union A by A8,TARSKI:def 4;
end;
then A9: A c= union A by TARSKI:def 3;
now let a;
assume a in union A;
then consider z such that
A10: a in z & z in A by TARSKI:def 4;
z c= A by A10,Def2;
hence a in A by A10;
end;
then union A c= A by TARSKI:def 3;
then A = union A by A9,XBOOLE_0:def 10;
hence thesis by Def6;
end;
theorem
not A is_limit_ordinal iff ex B st A = succ B
proof
thus not A is_limit_ordinal implies ex B st A = succ B
proof assume
not A is_limit_ordinal;
then consider B such that
A1: B in A & not succ B in A by Th41;
take B;
assume
A2: A <> succ B;
succ B c= A by A1,Th33;
then succ B c< A by A2,XBOOLE_0:def 8;
hence contradiction by A1,Th21;
end;
given B such that
A3: A = succ B;
A4: B in A by A3,Th10;
not succ B in A by A3;
hence not A is_limit_ordinal by A4,Th41;
end;
reserve F,G for Function;
::
:: 9. Transfinite sequences
::
definition let IT be Function;
attr IT is T-Sequence-like means
:Def7: dom IT is ordinal;
end;
definition
cluster T-Sequence-like Function;
existence
proof
reconsider E = {} as empty Function;
take E;
dom E = E;
hence thesis by Def7;
end;
end;
definition
mode T-Sequence is T-Sequence-like Function;
end;
definition let Z;
mode T-Sequence of Z -> T-Sequence means
:Def8: rng it c= Z;
existence
proof
dom {} = {};
then reconsider L = {} as T-Sequence by Def7;
take L;
rng {} = {};
hence rng L c= Z by XBOOLE_1:2;
end;
end;
canceled 2;
theorem
{} is T-Sequence of Z
proof
reconsider F = {} as Function;
A1: now consider a being Element of dom F;
assume dom F <> {};
then ex b st [a,b] in F by RELAT_1:def 4;
hence contradiction;
end;
then reconsider L = F as T-Sequence by Def7;
rng L = {} by A1,RELAT_1:65;
then rng L c= Z by XBOOLE_1:2;
hence {} is T-Sequence of Z by Def8;
end;
reserve L,L1 for T-Sequence;
theorem
dom F is Ordinal implies F is T-Sequence of rng F
proof assume
dom F is Ordinal;
then F is T-Sequence by Def7;
hence thesis by Def8;
end;
definition let L;
cluster dom L -> ordinal;
coherence by Def7;
end;
theorem
Th47: X c= Y implies for L being T-Sequence of X holds L is T-Sequence of Y
proof assume
A1: X c= Y;
let L be T-Sequence of X;
rng L c= X by Def8;
hence rng L c= Y by A1,XBOOLE_1:1;
end;
definition let L,A;
redefine func L|A -> T-Sequence of rng L;
coherence
proof
A1: A c= dom L implies dom(L|A) = A by RELAT_1:91;
dom L c= A implies dom(L|A) = dom L by RELAT_1:97;
then L|A is T-Sequence & rng(L|A) c= rng L by A1,Def7,FUNCT_1:76;
hence thesis by Def8;
end;
end;
theorem
for L being T-Sequence of X for A holds L|A is T-Sequence of X
proof let L be T-Sequence of X; let A;
rng L c= X by Def8;
hence L|A is T-Sequence of X by Th47;
end;
definition let IT be set;
attr IT is c=-linear means
:Def9: for x,y being set st x in IT & y in IT holds x,y are_c=-comparable;
end;
theorem
(for a st a in X holds a is T-Sequence) & X is c=-linear
implies union X is T-Sequence
proof assume that
A1: for a st a in X holds a is T-Sequence and
A2: X is c=-linear;
union X is Relation-like Function-like
proof
thus a in union X implies ex b,c st [b,c] = a
proof assume a in union X;
then consider x such that
A3: a in x & x in X by TARSKI:def 4;
reconsider x as T-Sequence by A1,A3;
x = x & for a st a in x holds ex b,c st [b,c] = a
by RELAT_1:def 1;
hence ex b,c st [b,c] = a by A3;
end;
let a,b,c; assume
A4: [a,b] in union X & [a,c] in union X;
then consider x such that
A5: [a,b] in x & x in X by TARSKI:def 4;
consider y such that
A6: [a,c] in y & y in X by A4,TARSKI:def 4;
reconsider x as T-Sequence by A1,A5;
reconsider y as T-Sequence by A1,A6;
x,y are_c=-comparable by A2,A5,A6,Def9;
then x c= y or y c= x by XBOOLE_0:def 9;
hence b = c by A5,A6,FUNCT_1:def 1;
end;
then reconsider F = union X as Function;
defpred P[set,set] means
$1 in X & for L st L = $1 holds dom L = $2;
A7: for a,b,c st P[a,b] & P[a,c] holds b = c
proof let a,b,c; assume
A8: ( a in X & for L st L = a holds dom L = b ) &
a in X & for L st L = a holds dom L = c;
then reconsider a as T-Sequence by A1;
dom a = b & dom a = c by A8;
hence b = c;
end;
consider G such that
A9: [a,b] in G iff a in X & P[a,b] from GraphFunc(A7);
A10: [a,b] in G implies b is Ordinal
proof assume
A11: [a,b] in G;
then a in X & for L st L = a holds dom L = b by A9;
then reconsider a as T-Sequence by A1;
dom a = b by A9,A11;
hence b is Ordinal;
end;
a in rng G implies a is Ordinal
proof assume
a in rng G;
then consider b such that
A12: b in dom G & a = G.b by FUNCT_1:def 5;
[b,a] in G by A12,FUNCT_1:8;
hence thesis by A10;
end;
then consider A such that
A13: rng G c= A by Th36;
defpred P[Ordinal] means for B st B in rng G holds B c= $1;
for B st B in rng G holds B c= A by A13,Def2;
then A14: ex A st P[A];
consider A such that
A15: P[A] & for C st P[C] holds A c= C from Ordinal_Min(A14);
F is T-Sequence-like
proof
dom F = A
proof
thus a in dom F implies a in A
proof assume a in dom F;
then consider b such that
A16: [a,b] in F by RELAT_1:def 4;
consider x such that
A17: [a,b] in x & x in X by A16,TARSKI:def 4;
reconsider x as T-Sequence by A1,A17;
A18: a in dom x by A17,RELAT_1:def 4;
for L st L = x holds dom L = dom x;
then [x,dom x] in G by A9,A17;
then x in dom G & dom x = G.x by FUNCT_1:8;
then dom x in rng G by FUNCT_1:def 5;
then dom x c= A by A15;
hence a in A by A18;
end;
let a; assume
A19: a in A;
then reconsider a' = a as Ordinal by Th23;
now assume
A20: for L st L in X holds not a' in dom L;
A21: now let L; assume L in X;
then not a' in dom L by A20;
hence dom L c= a' by Th26;
end;
now let B; assume B in rng G;
then consider c such that
A22: c in dom G & B = G.c by FUNCT_1:def 5;
A23: [c,B] in G by A22,FUNCT_1:8;
then c in X by A9;
then reconsider c as T-Sequence by A1;
c in X & dom c = B by A9,A23;
hence B c= a' by A21;
end;
then A24: A c= a' by A15;
a' c= A by A19,Def2;
then A = a by A24,XBOOLE_0:def 10;
hence contradiction by A19;
end;
then consider L such that
A25: L in X & a in dom L;
A26: L c= F by A25,ZFMISC_1:92;
consider b such that
A27: [a,b] in L by A25,RELAT_1:def 4;
thus a in dom F by A26,A27,RELAT_1:def 4;
end;
hence dom F is ordinal;
end;
hence thesis;
end;
::
:: 10. Schemes of definability by transfinite induction
::
scheme TS_Uniq { A()->Ordinal, H(T-Sequence)->set,
L1, L2() -> T-Sequence } :
L1() = L2() provided
A1: dom L1() = A() & for B,L st B in A() & L = L1()|B holds L1().B = H(L) and
A2: dom L2() = A() & for B,L st B in A() & L = L2()|B holds L2().B = H(L)
proof
assume
L1() <> L2();
then consider a such that
A3: a in A() & L1().a <> L2().a by A1,A2,FUNCT_1:9;
defpred P[set] means L1().$1 <> L2().$1;
consider X such that
A4: x in X iff x in A() & P[x] from Separation;
A5: X <> {} by A3,A4;
for b holds
b in X implies b in A() by A4;
then X c= A() by TARSKI:def 3;
then consider B such that
A6: B in X & for C st C in X holds B c= C by A5,Th32;
A7: B in A() & L1().B <> L2().B by A4,A6;
then A8: B c= A() by Def2;
A9: now let C; assume
A10: C in B;
then not B c= C by Th7;
then not C in X by A6;
hence L1().C = L2().C by A4,A8,A10;
end;
A11: dom(L1()|B) = B & dom(L2()|B) = B by A1,A2,A8,RELAT_1:91;
now let a; assume
A12: a in B;
then reconsider a' = a as Ordinal by Th23;
A13: L1().a' = L2().a' by A9,A12;
L1()|B.a = L1().a & L2()|B.a = L2().a by A11,A12,FUNCT_1:70;
hence L1()|B.a = L2()|B.a by A13;
end;
then A14: L1()|B = L2()|B by A11,FUNCT_1:9;
L1().B = H(L1()|B) & L2().B = H(L2()|B) by A1,A2,A7;
hence contradiction by A4,A6,A14;
end;
scheme TS_Exist { A()->Ordinal,H(T-Sequence)->set } :
ex L st dom L = A() & for B,L1 st B in A() & L1 = L|B holds L.B = H(L1)
proof
defpred S[Ordinal] means
ex L st dom L = $1 & for B st B in $1 holds L.B = H(L|B);
A1: for B st for C st C in B holds S[C] holds S[B]
proof let B such that
A2: for C st C in B
ex L st dom L = C & for D st D in C holds L.D = H(L|D);
defpred P[set,set] means
$1 is Ordinal & $2 is T-Sequence &
for A,L st A = $1 & L = $2 holds dom L = A &
for B st B in A holds L.B = H(L|B);
A3: for a,b,c st P[a,b] & P[a,c] holds b = c
proof let a,b,c; assume
A4: ( a is Ordinal & b is T-Sequence & for A,L st A = a & L = b holds
dom L = A & for B st B in A holds L.B = H(L|B) ) &
( a is Ordinal & c is T-Sequence & for A,L st A = a & L = c holds
dom L = A & for B st B in A holds L.B = H(L|B) );
then reconsider a as Ordinal;
reconsider b as T-Sequence by A4;
reconsider c as T-Sequence by A4;
deffunc HH(Ordinal) = H($1);
A5: dom b = a & for B,L st B in a & L=b|B holds b.B = HH(L) by A4;
A6: dom c = a & for B,L st B in a & L=c|B holds c.B = HH(L) by A4;
b = c from TS_Uniq(A5,A6);
hence thesis;
end;
consider G such that
A7: [a,b] in G iff a in B & P[a,b] from GraphFunc(A3);
A8: dom G = B
proof
thus a in dom G implies a in B
proof assume a in dom G;
then ex b st [a,b] in G by RELAT_1:def 4;
hence a in B by A7;
end;
let a; assume
A9: a in B;
then reconsider a' = a as Ordinal by Th23;
consider L such that
A10: dom L = a' & for D st D in a' holds L.D = H(L|D) by A2,A9;
for A holds for K be T-Sequence holds A = a' & K = L
implies dom K = A & for B holds B in A implies K.B = H(K|B) by A10;
then [a',L] in G by A7,A9;
hence a in dom G by RELAT_1:def 4;
end;
defpred R[Ordinal,Ordinal] means
ex L st L = G.$1 & $2 = H(L);
A11: for a,b,c st a in B & R[a,b] & R[a,c] holds b = c;
A12: for a st a in B ex b st R[a,b]
proof let a; assume a in B;
then consider c such that
A13: [a,c] in G by A8,RELAT_1:def 4;
reconsider L = c as T-Sequence by A7,A13;
take b = H(L), L;
thus L = G.a by A13,FUNCT_1:8;
thus b = H(L);
end;
consider F such that
A14: dom F = B & for a st a in B holds R[a,F.a]
from FuncEx(A11,A12);
reconsider L = F as T-Sequence by A14,Def7;
take L;
thus dom L = B by A14;
let D; assume
A15: D in B;
then consider K being T-Sequence such that
A16: K = G.D & F.D = H(K) by A14;
D c= dom L by A14,A15,Def2;
then A17: dom(L|D) = D by RELAT_1:91;
A18: [D,K] in G by A8,A15,A16,FUNCT_1:8;
then A19: dom K = D & for B st B in D holds K.B = H(K|B) by A7;
A20: now let C; assume
A21: C in D;
then A22: C in B by A15,Th19;
now let A,L such that
A23: A = C & L = K|C;
A24: C c= D by A21,Def2;
hence
A25: dom L = A by A19,A23,RELAT_1:91;
let B; assume
A26: B in A;
then B in D & B c= A by A23,A24,Def2;
then K.B = H(K|B) & K|B = L|B by A7,A18,A23,FUNCT_1:82;
hence L.B = H(L|B) by A23,A25,A26,FUNCT_1:70;
end;
then [C,K|C] in G by A7,A22;
hence G.C = K|C by FUNCT_1:8;
end;
now let a; assume
A27: a in D;
then reconsider A = a as Ordinal by Th23;
A28: G.A = K|A by A20,A27;
A29: A in B by A15,A27,Th19;
A30: L|D.A = L.A by A27,FUNCT_1:72;
ex J being T-Sequence st J = G.A & F.A = H(J) by A14,A29;
hence L|D.a = K.a by A7,A18,A27,A28,A30;
end;
hence L.D = H(L|D) by A16,A17,A19,FUNCT_1:9;
end;
for A holds S[A] from Transfinite_Ind(A1);
then consider L such that
A31: dom L = A() & for B st B in A() holds L.B = H(L|B);
take L;
thus dom L = A() by A31;
let B,L1; assume
B in A() & L1 = L|B;
hence thesis by A31;
end;
scheme Func_TS { L() -> T-Sequence, F(Ordinal)->set, H(T-Sequence)->set } :
for B st B in dom L() holds L().B = H(L()|B)
provided
A1: for A,a holds a = F(A) iff
ex L st a = H(L) & dom L = A & for B st B in A holds L.B = H(L|B) and
A2: for A st A in dom L() holds L().A = F(A)
proof
consider L such that
F(dom L()) = H(L) and
A3: dom L = dom L() and
A4: for B st B in dom L() holds L.B = H(L|B) by A1;
now let b; assume
A5: b in dom L;
then reconsider B = b as Ordinal by Th23;
now take K = L|B;
thus H(L|B) = H(K);
A6: B c= dom L by A5,Def2;
hence
dom K = B by RELAT_1:91;
let C; assume
A7: C in B;
then C in dom L() & C c= B by A3,A6,Def2;
then K.C = L.C & L|C = K|C by A7,FUNCT_1:72,82;
hence K.C = H(K|C) by A3,A4,A6,A7;
end;
then F(B) = H(L|B) by A1 .= L.B by A3,A4,A5;
hence L().b = L.b by A2,A3,A5;
end;
then L() = L by A3,FUNCT_1:9;
hence thesis by A4;
end;
theorem
A c< B or A = B or B c< A
proof assume not(A c< B or A = B or B c< A);
then not(A c= B or B c= A) by XBOOLE_0:def 8;
hence contradiction;
end;