let E be non empty set ; :: thesis: ex f being Function st
( dom f = E & ( for d being Element of E holds f . d = f .: d ) )
defpred S₁[ Ordinal, Function, non empty set ] means ( dom $2 = Collapse ($3,$1) & ( for d being Element of E st d in Collapse ($3,$1) holds
$2 . d = $2 .: d ) );
defpred S₂[ Ordinal] means for f1, f2 being Function st S₁[$1,f1,E] & S₁[$1,f2,E] holds
f1 = f2;
defpred S₃[ Ordinal] means ex f being Function st S₁[$1,f,E];
A1: for A, B being Ordinal
for f being Function st A c= B & S₁[B,f,E] holds
S₁[A,f | (Collapse (E,A)),E]

proof

let A, B be Ordinal; :: thesis: for f being Function st A c= B & S₁[B,f,E] holds
S₁[A,f | (Collapse (E,A)),E]
let f be Function; :: thesis: ( A c= B & S₁[B,f,E] implies S₁[A,f | (Collapse (E,A)),E] )
assume that
A2: A c= B and
A3: dom f = Collapse (E,B) and
A4: for d being Element of E st d in Collapse (E,B) holds
f . d = f .: d ; :: thesis: S₁[A,f | (Collapse (E,A)),E]
A5: Collapse (E,A) c= Collapse (E,B) by A2, Th4;
thus dom (f | (Collapse (E,A))) = Collapse (E,A) by A2, A3, Th4, RELAT_1:62; :: thesis: for d being Element of E st d in Collapse (E,A) holds
(f | (Collapse (E,A))) . d = (f | (Collapse (E,A))) .: d
let d be Element of E; :: thesis: ( d in Collapse (E,A) implies (f | (Collapse (E,A))) . d = (f | (Collapse (E,A))) .: d )
assume A6: d in Collapse (E,A) ; :: thesis: (f | (Collapse (E,A))) . d = (f | (Collapse (E,A))) .: d
for x being object st x in f .: d holds
x in (f | (Collapse (E,A))) .: d

proof

let x be object ; :: thesis: ( x in f .: d implies x in (f | (Collapse (E,A))) .: d )
A7: dom (f | (Collapse (E,A))) = Collapse (E,A) by A2, A3, Th4, RELAT_1:62;
assume x in f .: d ; :: thesis: x in (f | (Collapse (E,A))) .: d
then consider z being object such that
A8: z in dom f and
A9: z in d and
A10: x = f . z by FUNCT_1:def 6;
dom f c= E by A3, Th7;
then reconsider d1 = z as Element of E by A8;
A11: d1 in Collapse (E,A) by A6, A9, Th6;
then (f | (Collapse (E,A))) . z = f . z by FUNCT_1:49;
hence x in (f | (Collapse (E,A))) .: d by A9, A10, A11, A7, FUNCT_1:def 6; :: thesis: verum

end;

then A12: f .: d c= (f | (Collapse (E,A))) .: d ;
(f | (Collapse (E,A))) .: d c= f .: d by RELAT_1:128;
then A13: f .: d = (f | (Collapse (E,A))) .: d by A12;
thus (f | (Collapse (E,A))) . d = f . d by A6, FUNCT_1:49
.= (f | (Collapse (E,A))) .: d by A4, A5, A6, A13 ; :: thesis: verum

end;

A14: now :: thesis: for A being Ordinal st ( for B being Ordinal st B in A holds
S₂[B] ) holds
S₂[A]

let A be Ordinal; :: thesis: ( ( for B being Ordinal st B in A holds
S₂[B] ) implies S₂[A] )
assume A15: for B being Ordinal st B in A holds
S₂[B] ; :: thesis: S₂[A]
thus S₂[A] :: thesis: verum

proof

let f1, f2 be Function; :: thesis: ( S₁[A,f1,E] & S₁[A,f2,E] implies f1 = f2 )
assume that
A16: S₁[A,f1,E] and
A17: S₁[A,f2,E] ; :: thesis: f1 = f2

now :: thesis: for x being object st x in Collapse (E,A) holds
f1 . x = f2 . x

let x be object ; :: thesis: ( x in Collapse (E,A) implies f1 . x = f2 . x )
assume A18: x in Collapse (E,A) ; :: thesis: f1 . x = f2 . x
Collapse (E,A) c= E by Th7;
then reconsider d = x as Element of E by A18;
A19: f1 .: d = f2 .: d

proof

thus for y being object st y in f1 .: d holds
y in f2 .: d :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: f2 .: d c= f1 .: d

proof

let y be object ; :: thesis: ( y in f1 .: d implies y in f2 .: d )
assume y in f1 .: d ; :: thesis: y in f2 .: d
then consider z being object such that
A20: z in dom f1 and
A21: z in d and
A22: y = f1 . z by FUNCT_1:def 6;
dom f1 c= E by A16, Th7;
then reconsider d1 = z as Element of E by A20;
consider B being Ordinal such that
A23: B in A and
A24: d1 in Collapse (E,B) by A18, A21, Th6;
B c= A by A23, ORDINAL1:def 2;
then ( S₁[B,f1 | (Collapse (E,B)),E] & S₁[B,f2 | (Collapse (E,B)),E] ) by A1, A16, A17;
then A25: f1 | (Collapse (E,B)) = f2 | (Collapse (E,B)) by A15, A23;
f1 . d1 = (f1 | (Collapse (E,B))) . d1 by A24, FUNCT_1:49
.= f2 . d1 by A24, A25, FUNCT_1:49 ;
hence y in f2 .: d by A16, A17, A20, A21, A22, FUNCT_1:def 6; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f2 .: d or y in f1 .: d )
assume y in f2 .: d ; :: thesis: y in f1 .: d
then consider z being object such that
A26: z in dom f2 and
A27: z in d and
A28: y = f2 . z by FUNCT_1:def 6;
dom f2 c= E by A17, Th7;
then reconsider d1 = z as Element of E by A26;
consider B being Ordinal such that
A29: B in A and
A30: d1 in Collapse (E,B) by A18, A27, Th6;
B c= A by A29, ORDINAL1:def 2;
then ( S₁[B,f1 | (Collapse (E,B)),E] & S₁[B,f2 | (Collapse (E,B)),E] ) by A1, A16, A17;
then A31: f1 | (Collapse (E,B)) = f2 | (Collapse (E,B)) by A15, A29;
f1 . d1 = (f1 | (Collapse (E,B))) . d1 by A30, FUNCT_1:49
.= f2 . d1 by A30, A31, FUNCT_1:49 ;
hence y in f1 .: d by A16, A17, A26, A27, A28, FUNCT_1:def 6; :: thesis: verum

end;

f1 . d = f1 .: d by A16, A18;
hence f1 . x = f2 . x by A17, A18, A19; :: thesis: verum

end;

hence f1 = f2 by A16, A17, FUNCT_1:2; :: thesis: verum

end;

end;

A32: for A being Ordinal holds S₂[A] from ORDINAL1:sch 2(A14);
A33: for A being Ordinal st ( for B being Ordinal st B in A holds
S₃[B] ) holds
S₃[A]

proof

let A be Ordinal; :: thesis: ( ( for B being Ordinal st B in A holds
S₃[B] ) implies S₃[A] )
assume for B being Ordinal st B in A holds
ex f being Function st S₁[B,f,E] ; :: thesis: S₃[A]
defpred S₄[ object , object ] means ex d, e being set st
( d = $1 & e = $2 & ( for x being object holds
( x in e iff ex d1 being Element of E ex B being Ordinal ex f being Function st
( d1 in d & B in A & d1 in Collapse (E,B) & S₁[B,f,E] & x = f . d1 ) ) ) );
A34: for x being object st x in Collapse (E,A) holds
ex y being object st S₄[x,y]

proof

A35: Collapse (E,A) c= E by Th7;
let x be object ; :: thesis: ( x in Collapse (E,A) implies ex y being object st S₄[x,y] )
assume x in Collapse (E,A) ; :: thesis: ex y being object st S₄[x,y]
then reconsider d = x as Element of E by A35;
defpred S₅[ object , object ] means ex B being Ordinal ex f being Function st
( B in A & $1 in Collapse (E,B) & S₁[B,f,E] & $2 = f . $1 );
A36: for x, y, z being object st S₅[x,y] & S₅[x,z] holds
y = z

proof

let x, y, z be object ; :: thesis: ( S₅[x,y] & S₅[x,z] implies y = z )
given B1 being Ordinal, f1 being Function such that B1 in A and
A37: x in Collapse (E,B1) and
A38: S₁[B1,f1,E] and
A39: y = f1 . x ; :: thesis: ( not S₅[x,z] or y = z )
given B2 being Ordinal, f2 being Function such that B2 in A and
A40: x in Collapse (E,B2) and
A41: S₁[B2,f2,E] and
A42: z = f2 . x ; :: thesis: y = z

A43: now :: thesis: ( B2 c= B1 implies y = z )

assume B2 c= B1 ; :: thesis: y = z
then S₁[B2,f1 | (Collapse (E,B2)),E] by A1, A38;
then f1 | (Collapse (E,B2)) = f2 by A32, A41;
hence y = z by A39, A40, A42, FUNCT_1:49; :: thesis: verum

end;

now :: thesis: ( B1 c= B2 implies y = z )

assume B1 c= B2 ; :: thesis: y = z
then S₁[B1,f2 | (Collapse (E,B1)),E] by A1, A41;
then f2 | (Collapse (E,B1)) = f1 by A32, A38;
hence y = z by A37, A39, A42, FUNCT_1:49; :: thesis: verum

end;

hence y = z by A43; :: thesis: verum

end;

consider X being set such that
A44: for y being object holds
( y in X iff ex x being object st
( x in d & S₅[x,y] ) ) from TARSKI:sch 1(A36);
take y = X; :: thesis: S₄[x,y]
take d ; :: thesis: ex e being set st
( d = x & e = y & ( for x being object holds
( x in e iff ex d1 being Element of E ex B being Ordinal ex f being Function st
( d1 in d & B in A & d1 in Collapse (E,B) & S₁[B,f,E] & x = f . d1 ) ) ) )
take X ; :: thesis: ( d = x & X = y & ( for x being object holds
( x in X iff ex d1 being Element of E ex B being Ordinal ex f being Function st
( d1 in d & B in A & d1 in Collapse (E,B) & S₁[B,f,E] & x = f . d1 ) ) ) )
thus d = x ; :: thesis: ( X = y & ( for x being object holds
( x in X iff ex d1 being Element of E ex B being Ordinal ex f being Function st
( d1 in d & B in A & d1 in Collapse (E,B) & S₁[B,f,E] & x = f . d1 ) ) ) )
thus y = X ; :: thesis: for x being object holds
( x in X iff ex d1 being Element of E ex B being Ordinal ex f being Function st
( d1 in d & B in A & d1 in Collapse (E,B) & S₁[B,f,E] & x = f . d1 ) )
let x be object ; :: thesis: ( x in X iff ex d1 being Element of E ex B being Ordinal ex f being Function st
( d1 in d & B in A & d1 in Collapse (E,B) & S₁[B,f,E] & x = f . d1 ) )
thus ( x in X implies ex d1 being Element of E ex B being Ordinal ex f being Function st
( d1 in d & B in A & d1 in Collapse (E,B) & S₁[B,f,E] & x = f . d1 ) ) :: thesis: ( ex d1 being Element of E ex B being Ordinal ex f being Function st
( d1 in d & B in A & d1 in Collapse (E,B) & S₁[B,f,E] & x = f . d1 ) implies x in X )

proof

assume x in X ; :: thesis: ex d1 being Element of E ex B being Ordinal ex f being Function st
( d1 in d & B in A & d1 in Collapse (E,B) & S₁[B,f,E] & x = f . d1 )
then consider y being object such that
A45: y in d and
A46: ex B being Ordinal ex f being Function st
( B in A & y in Collapse (E,B) & S₁[B,f,E] & x = f . y ) by A44;
consider B being Ordinal, f being Function such that
A47: B in A and
A48: y in Collapse (E,B) and
A49: ( S₁[B,f,E] & x = f . y ) by A46;
Collapse (E,B) c= E by Th7;
then reconsider d1 = y as Element of E by A48;
take d1 ; :: thesis: ex B being Ordinal ex f being Function st
( d1 in d & B in A & d1 in Collapse (E,B) & S₁[B,f,E] & x = f . d1 )
take B ; :: thesis: ex f being Function st
( d1 in d & B in A & d1 in Collapse (E,B) & S₁[B,f,E] & x = f . d1 )
take f ; :: thesis: ( d1 in d & B in A & d1 in Collapse (E,B) & S₁[B,f,E] & x = f . d1 )
thus ( d1 in d & B in A & d1 in Collapse (E,B) & S₁[B,f,E] & x = f . d1 ) by A45, A47, A48, A49; :: thesis: verum

end;

given d1 being Element of E, B being Ordinal, f being Function such that A50: ( d1 in d & B in A & d1 in Collapse (E,B) & S₁[B,f,E] & x = f . d1 ) ; :: thesis: x in X
thus x in X by A44, A50; :: thesis: verum

end;

consider f being Function such that
A51: ( dom f = Collapse (E,A) & ( for x being object st x in Collapse (E,A) holds
S₄[x,f . x] ) ) from CLASSES1:sch 1(A34);
defpred S₅[ Ordinal] means ( $1 c= A implies S₁[$1,f | (Collapse (E,$1)),E] );
A52: for B being Ordinal st ( for C being Ordinal st C in B holds
S₅[C] ) holds
S₅[B]

proof

let B be Ordinal; :: thesis: ( ( for C being Ordinal st C in B holds
S₅[C] ) implies S₅[B] )
assume A53: for C being Ordinal st C in B holds
S₅[C] ; :: thesis: S₅[B]
assume A54: B c= A ; :: thesis: S₁[B,f | (Collapse (E,B)),E]
then A55: Collapse (E,B) c= Collapse (E,A) by Th4;
thus A56: dom (f | (Collapse (E,B))) = Collapse (E,B) by A51, A54, Th4, RELAT_1:62; :: thesis: for d being Element of E st d in Collapse (E,B) holds
(f | (Collapse (E,B))) . d = (f | (Collapse (E,B))) .: d
let d be Element of E; :: thesis: ( d in Collapse (E,B) implies (f | (Collapse (E,B))) . d = (f | (Collapse (E,B))) .: d )
assume A57: d in Collapse (E,B) ; :: thesis: (f | (Collapse (E,B))) . d = (f | (Collapse (E,B))) .: d
then (f | (Collapse (E,B))) . d = f . d by FUNCT_1:49;
then consider d9, e being set such that
A58: d9 = d and
A59: e = (f | (Collapse (E,B))) . d and
A60: for x being object holds
( x in e iff ex d1 being Element of E ex B being Ordinal ex f being Function st
( d1 in d9 & B in A & d1 in Collapse (E,B) & S₁[B,f,E] & x = f . d1 ) ) by A51, A55, A57;
set X = (f | (Collapse (E,B))) . d;
A61: (f | (Collapse (E,B))) . d c= (f | (Collapse (E,B))) .: d

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (f | (Collapse (E,B))) . d or x in (f | (Collapse (E,B))) .: d )
assume x in (f | (Collapse (E,B))) . d ; :: thesis: x in (f | (Collapse (E,B))) .: d
then consider d1 being Element of E, C being Ordinal, h being Function such that
A62: d1 in d9 and
C in A and
A63: d1 in Collapse (E,C) and
A64: S₁[C,h,E] and
A65: x = h . d1 by A60, A59;
consider C9 being Ordinal such that
A66: C9 in B and
A67: d1 in Collapse (E,C9) by A57, A58, A62, Th6;
A68: for C being Ordinal
for h being Function st C c= C9 & S₁[C,h,E] & d1 in Collapse (E,C) & x = h . d1 holds
x in (f | (Collapse (E,B))) .: d

proof

let C be Ordinal; :: thesis: for h being Function st C c= C9 & S₁[C,h,E] & d1 in Collapse (E,C) & x = h . d1 holds
x in (f | (Collapse (E,B))) .: d
let h be Function; :: thesis: ( C c= C9 & S₁[C,h,E] & d1 in Collapse (E,C) & x = h . d1 implies x in (f | (Collapse (E,B))) .: d )
assume that
A69: C c= C9 and
A70: S₁[C,h,E] and
A71: d1 in Collapse (E,C) and
A72: x = h . d1 ; :: thesis: x in (f | (Collapse (E,B))) .: d
A73: C in B by A66, A69, ORDINAL1:12;
then C c= A by A54, ORDINAL1:def 2;
then S₁[C,f | (Collapse (E,C)),E] by A53, A73;
then A74: f | (Collapse (E,C)) = h by A32, A70;
A75: Collapse (E,C) c= Collapse (E,B) by Th4, A73, ORDINAL1:def 2;
then f | (Collapse (E,C)) = (f | (Collapse (E,B))) | (Collapse (E,C)) by FUNCT_1:51;
then h . d1 = (f | (Collapse (E,B))) . d1 by A71, A74, FUNCT_1:49;
hence x in (f | (Collapse (E,B))) .: d by A56, A58, A62, A71, A72, A75, FUNCT_1:def 6; :: thesis: verum

end;

( C9 c= C implies x in (f | (Collapse (E,B))) .: d )

proof

assume C9 c= C ; :: thesis: x in (f | (Collapse (E,B))) .: d
then A76: S₁[C9,h | (Collapse (E,C9)),E] by A1, A64;
h . d1 = (h | (Collapse (E,C9))) . d1 by A67, FUNCT_1:49;
hence x in (f | (Collapse (E,B))) .: d by A65, A67, A68, A76; :: thesis: verum

end;

hence x in (f | (Collapse (E,B))) .: d by A63, A64, A65, A68; :: thesis: verum

end;

(f | (Collapse (E,B))) .: d c= (f | (Collapse (E,B))) . d

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (f | (Collapse (E,B))) .: d or x in (f | (Collapse (E,B))) . d )
assume x in (f | (Collapse (E,B))) .: d ; :: thesis: x in (f | (Collapse (E,B))) . d
then consider y being object such that
A77: y in dom (f | (Collapse (E,B))) and
A78: y in d and
A79: x = (f | (Collapse (E,B))) . y by FUNCT_1:def 6;
Collapse (E,B) c= E by Th7;
then reconsider d1 = y as Element of E by A56, A77;
consider C being Ordinal such that
A80: C in B and
A81: d1 in Collapse (E,C) by A57, A78, Th6;
Collapse (E,C) c= Collapse (E,B) by Th4, A80, ORDINAL1:def 2;
then (f | (Collapse (E,B))) | (Collapse (E,C)) = f | (Collapse (E,C)) by FUNCT_1:51;
then A82: (f | (Collapse (E,C))) . y = (f | (Collapse (E,B))) . y by A81, FUNCT_1:49;
C c= A by A54, A80, ORDINAL1:def 2;
then S₁[C,f | (Collapse (E,C)),E] by A53, A80;
hence x in (f | (Collapse (E,B))) . d by A54, A58, A60, A78, A79, A80, A81, A82, A59; :: thesis: verum

end;

hence (f | (Collapse (E,B))) . d = (f | (Collapse (E,B))) .: d by A61; :: thesis: verum

end;

A83: for B being Ordinal holds S₅[B] from ORDINAL1:sch 2(A52);
take f ; :: thesis: S₁[A,f,E]
f | (dom f) = f by RELAT_1:68;
hence S₁[A,f,E] by A51, A83; :: thesis: verum

end;

A84: for A being Ordinal holds S₃[A] from ORDINAL1:sch 2(A33);
consider A being Ordinal such that
A85: E = Collapse (E,A) by Th8;
consider f being Function such that
A86: S₁[A,f,E] by A84;
take f ; :: thesis: ( dom f = E & ( for d being Element of E holds f . d = f .: d ) )
thus dom f = E by A85, A86; :: thesis: for d being Element of E holds f . d = f .: d
let d be Element of E; :: thesis: f . d = f .: d
thus f . d = f .: d by A85, A86; :: thesis: verum