let E be non empty set ; :: thesis:
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]

let A, B be Ordinal; :: thesis:
let f be Function; :: thesis:
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:
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:
let d be Element of E; :: thesis:
assume A6: d in Collapse (E,A) ; :: thesis:
for x being set st x in f .: d holds
x in (f | (Collapse (E,A))) .: d

let x be set ; :: thesis:
A7: dom (f | (Collapse (E,A))) = Collapse (E,A) by A2, A3, Th4, RELAT_1:62;
assume x in f .: d ; :: thesis:
then consider z being set 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:

end;

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

end;

A14: now

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

proof

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

now

let x be set ; :: thesis:
assume A18: x in Collapse (E,A) ; :: thesis:
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 set st y in f1 .: d holds
y in f2 .: d :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

proof

let y be set ; :: thesis:
assume y in f1 .: d ; :: thesis:
then consider z being set 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:

end;

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in f2 .: d ; :: thesis:
then consider z being set 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:

end;

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

end;

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

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:
assume for B being Ordinal st B in A holds
ex f being Function st S₁[B,f,E] ; :: thesis:
defpred S₄[ set , set ] means ex d being Element of E st
( d = $1 & ( for x being set holds
( x in $2 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 set st x in Collapse (E,A) holds
ex y being set st S₄[x,y]

proof

A35: Collapse (E,A) c= E by Th7;
let x be set ; :: thesis:
assume x in Collapse (E,A) ; :: thesis:
then reconsider d = x as Element of E by A35;
defpred S₅[ set , set ] 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 set st S₅[x,y] & S₅[x,z] holds
y = z

proof

let x, y, z be set ; :: thesis:
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:
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:

A43: now

assume B2 c= B1 ; :: thesis:
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:

end;

now

assume B1 c= B2 ; :: thesis:
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:

end;

hence y = z by A43; :: thesis:

end;

consider X being set such that
A44: for y being set holds
( y in X iff ex x being set st
( x in d & S₅[x,y] ) ) from TARSKI:sch 1(A36);
take y = X; :: thesis:
take d ; :: thesis:
thus d = x ; :: thesis:
let x be set ; :: thesis:
thus ( x in y 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:

proof

assume x in y ; :: thesis:
then consider y being set 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:
take B ; :: thesis:
take f ; :: thesis:
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:

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:
thus x in y by A44, A50; :: thesis:

end;

consider f being Function such that
A51: ( dom f = Collapse (E,A) & ( for x being set 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:
assume A53: for C being Ordinal st C in B holds
S₅[C] ; :: thesis:
assume A54: B c= A ; :: thesis:
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:
let d be Element of E; :: thesis:
assume A57: d in Collapse (E,B) ; :: thesis:
then (f | (Collapse (E,B))) . d = f . d by FUNCT_1:49;
then consider d9 being Element of E such that
A58: d9 = d and
A59: for x being set holds
( x in (f | (Collapse (E,B))) . d 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;
A60: (f | (Collapse (E,B))) . d c= (f | (Collapse (E,B))) .: d

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in (f | (Collapse (E,B))) . d ; :: thesis:
then consider d1 being Element of E, C being Ordinal, h being Function such that
A61: d1 in d9 and
C in A and
A62: d1 in Collapse (E,C) and
A63: S₁[C,h,E] and
A64: x = h . d1 by A59;
consider C9 being Ordinal such that
A65: C9 in B and
A66: d1 in Collapse (E,C9) by A57, A58, A61, Th6;
A67: 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:
let h be Function; :: thesis:
assume that
A68: C c= C9 and
A69: S₁[C,h,E] and
A70: d1 in Collapse (E,C) and
A71: x = h . d1 ; :: thesis:
A72: C in B by A65, A68, ORDINAL1:12;
then C c= A by A54, ORDINAL1:def 2;
then S₁[C,f | (Collapse (E,C)),E] by A53, A72;
then A73: f | (Collapse (E,C)) = h by A32, A69;
C c= B by A72, ORDINAL1:def 2;
then A74: Collapse (E,C) c= Collapse (E,B) by Th4;
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 A70, A73, FUNCT_1:49;
hence x in (f | (Collapse (E,B))) .: d by A56, A58, A61, A70, A71, A74, FUNCT_1:def 6; :: thesis:

end;

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

proof

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

end;

hence x in (f | (Collapse (E,B))) .: d by A62, A63, A64, A67; :: thesis:

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in (f | (Collapse (E,B))) .: d ; :: thesis:
then consider y being set such that
A76: y in dom (f | (Collapse (E,B))) and
A77: y in d and
A78: 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, A76;
consider C being Ordinal such that
A79: C in B and
A80: d1 in Collapse (E,C) by A57, A77, Th6;
C c= B by A79, ORDINAL1:def 2;
then Collapse (E,C) c= Collapse (E,B) by Th4;
then (f | (Collapse (E,B))) | (Collapse (E,C)) = f | (Collapse (E,C)) by FUNCT_1:51;
then A81: (f | (Collapse (E,C))) . y = (f | (Collapse (E,B))) . y by A80, FUNCT_1:49;
C c= A by A54, A79, ORDINAL1:def 2;
then S₁[C,f | (Collapse (E,C)),E] by A53, A79;
hence x in (f | (Collapse (E,B))) . d by A54, A58, A59, A77, A78, A79, A80, A81; :: thesis:

end;

hence (f | (Collapse (E,B))) . d = (f | (Collapse (E,B))) .: d by A60, XBOOLE_0:def 10; :: thesis:

end;

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

end;

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