defpred S1[ Ordinal, T-Sequence] means ( dom $2 = $1 & ( {} in $1 implies $2 . {} = F2() ) & ( for A being Ordinal st succ A in $1 holds
$2 . (succ A) = F3(A,($2 . A)) ) & ( for A being Ordinal st A in $1 & A <> {} & A is limit_ordinal holds
$2 . A = F4(A,($2 | A)) ) );
defpred S2[ Ordinal] means ex L being T-Sequence st S1[$1,L];
A1: for B being Ordinal st ( for C being Ordinal st C in B holds
S2[C] ) holds
S2[B]
proof
let B be Ordinal; :: thesis: ( ( for C being Ordinal st C in B holds
S2[C] ) implies S2[B] )
assume A2: for C being Ordinal st C in B holds
ex L being T-Sequence st S1[C,L] ; :: thesis: S2[B]
defpred S3[ set , set ] means ( $1 is Ordinal & $2 is T-Sequence & ( for A being Ordinal
for L being T-Sequence st A = $1 & L = $2 holds
S1[A,L] ) );
A3: for a, b, c being set st S3[a,b] & S3[a,c] holds
b = c
proof
let a, b, c be set ; :: thesis: ( S3[a,b] & S3[a,c] implies b = c )
assume A4: ( a is Ordinal & b is T-Sequence & ( for A being Ordinal
for L being T-Sequence st A = a & L = b holds
S1[A,L] ) & a is Ordinal & c is T-Sequence & ( for A being Ordinal
for L being T-Sequence st A = a & L = c holds
S1[A,L] ) ) ; :: thesis: b = c
then reconsider a = a as Ordinal ;
reconsider b = b as T-Sequence by A4;
reconsider c = c as T-Sequence by A4;
A5: dom b = a by A4;
A6: ( {} in a implies b . {} = F2() ) by A4;
A7: for A being Ordinal st succ A in a holds
b . (succ A) = F3(A,(b . A)) by A4;
A8: for A being Ordinal st A in a & A <> {} & A is limit_ordinal holds
b . A = F4(A,(b | A)) by A4;
A9: dom c = a by A4;
A10: ( {} in a implies c . {} = F2() ) by A4;
A11: for A being Ordinal st succ A in a holds
c . (succ A) = F3(A,(c . A)) by A4;
A12: for A being Ordinal st A in a & A <> {} & A is limit_ordinal holds
c . A = F4(A,(c | A)) by A4;
b = c from ORDINAL2:sch 4(A5, A6, A7, A8, A9, A10, A11, A12);
 hence b = c ; :: thesis: verum
end;
consider G being Function such that
A13: for a, b being set holds
( [a,b] in G iff ( a in B & S3[a,b] ) ) from FUNCT_1:sch 1(A3);
 A14: 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 RELAT_1:def 4;
hence a in B by A13; :: thesis: verum
end;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in B or a in dom G )
assume A15: a in B ; :: thesis: a in dom G
then reconsider a' = a as Ordinal ;
consider L being T-Sequence such that
A16: S1[a',L] by A2, A15;
for A being Ordinal
for K being T-Sequence st A = a' & K = L holds
S1[A,K] by A16;
then [a',L] in G by A13, A15;
hence a in dom G by RELAT_1:def 4; :: thesis: verum
end;
defpred S4[ set , set ] means ex A being Ordinal ex L being T-Sequence st
( A = $1 & L = G . $1 & ( ( A = {} & $2 = F2() ) or ex B being Ordinal st
( A = succ B & $2 = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & $2 = F4(A,L) ) ) );
A17: for a, b, c being set st a in B & S4[a,b] & S4[a,c] holds
b = c
proof
let a, b, c be set ; :: thesis: ( a in B & S4[a,b] & S4[a,c] implies b = c )
assume a in B ; :: thesis: ( not S4[a,b] or not S4[a,c] or b = c )
given Ab being Ordinal, Lb being T-Sequence such that A18: ( Ab = a & Lb = G . a ) and
A19: ( ( Ab = {} & b = F2() ) or ex B being Ordinal st
( Ab = succ B & b = F3(B,(Lb . B)) ) or ( Ab <> {} & Ab is limit_ordinal & b = F4(Ab,Lb) ) ) ; :: thesis: ( not S4[a,c] or b = c )
given Ac being Ordinal, Lc being T-Sequence such that A20: ( Ac = a & Lc = G . a ) and
A21: ( ( Ac = {} & c = F2() ) or ex B being Ordinal st
( Ac = succ B & c = F3(B,(Lc . B)) ) or ( Ac <> {} & Ac is limit_ordinal & c = F4(Ac,Lc) ) ) ; :: thesis: b = c
now
given C being Ordinal such that A22: Ab = succ C ; :: thesis: b = c
consider A being Ordinal such that
A23: ( Ab = succ A & b = F3(A,(Lb . A)) ) by A19, A22, ORDINAL1:42;
consider D being Ordinal such that
A24: ( Ac = succ D & c = F3(D,(Lc . D)) ) by A18, A20, A21, A22, ORDINAL1:42;
A = D by A18, A20, A23, A24, ORDINAL1:12;
hence b = c by A18, A20, A23, A24; :: thesis: verum
end;
hence b = c by A18, A19, A20, A21; :: thesis: verum
end;
A25: for a being set st a in B holds
ex b being set st S4[a,b]
proof
let a be set ; :: thesis: ( a in B implies ex b being set st S4[a,b] )
assume A26: a in B ; :: thesis: ex b being set st S4[a,b]
then consider c being set such that
A27: [a,c] in G by A14, RELAT_1:def 4;
reconsider L = c as T-Sequence by A13, A27;
reconsider A = a as Ordinal by A26;
A28: now
assume A29: A = {} ; :: thesis: S4[a,F2()]
thus S4[a,F2()] :: thesis: verum
proof
take A ; :: thesis: ex L being T-Sequence st
( A = a & L = G . a & ( ( A = {} & F2() = F2() ) or ex B being Ordinal st
( A = succ B & F2() = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F2() = F4(A,L) ) ) )
take L ; :: thesis: ( A = a & L = G . a & ( ( A = {} & F2() = F2() ) or ex B being Ordinal st
( A = succ B & F2() = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F2() = F4(A,L) ) ) )
thus ( A = a & L = G . a ) by A27, FUNCT_1:8; :: thesis: ( ( A = {} & F2() = F2() ) or ex B being Ordinal st
( A = succ B & F2() = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F2() = F4(A,L) ) )
thus ( ( A = {} & F2() = F2() ) or ex B being Ordinal st
( A = succ B & F2() = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F2() = F4(A,L) ) ) by A29; :: thesis: verum
end;
end;
A30: now
given C being Ordinal such that A31: A = succ C ; :: thesis: ex b being set st S4[a,b]
thus ex b being set st S4[a,b] :: thesis: verum
proof
take F3(C,(L . C)) ; :: thesis: S4[a,F3(C,(L . C))]
take A ; :: thesis: ex L being T-Sequence st
( A = a & L = G . a & ( ( A = {} & F3(C,(L . C)) = F2() ) or ex B being Ordinal st
( A = succ B & F3(C,(L . C)) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F3(C,(L . C)) = F4(A,L) ) ) )
take L ; :: thesis: ( A = a & L = G . a & ( ( A = {} & F3(C,(L . C)) = F2() ) or ex B being Ordinal st
( A = succ B & F3(C,(L . C)) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F3(C,(L . C)) = F4(A,L) ) ) )
thus ( A = a & L = G . a ) by A27, FUNCT_1:8; :: thesis: ( ( A = {} & F3(C,(L . C)) = F2() ) or ex B being Ordinal st
( A = succ B & F3(C,(L . C)) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F3(C,(L . C)) = F4(A,L) ) )
thus ( ( A = {} & F3(C,(L . C)) = F2() ) or ex B being Ordinal st
( A = succ B & F3(C,(L . C)) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F3(C,(L . C)) = F4(A,L) ) ) by A31; :: thesis: verum
end;
end;
now
assume A32: ( A <> {} & ( for C being Ordinal holds A <> succ C ) ) ; :: thesis: S4[a,F4(A,L)]
thus S4[a,F4(A,L)] :: thesis: verum
proof
take A ; :: thesis: ex L being T-Sequence st
( A = a & L = G . a & ( ( A = {} & F4(A,L) = F2() ) or ex B being Ordinal st
( A = succ B & F4(A,L) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F4(A,L) = F4(A,L) ) ) )
take L ; :: thesis: ( A = a & L = G . a & ( ( A = {} & F4(A,L) = F2() ) or ex B being Ordinal st
( A = succ B & F4(A,L) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F4(A,L) = F4(A,L) ) ) )
thus ( A = a & L = G . a ) by A27, FUNCT_1:8; :: thesis: ( ( A = {} & F4(A,L) = F2() ) or ex B being Ordinal st
( A = succ B & F4(A,L) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F4(A,L) = F4(A,L) ) )
thus ( ( A = {} & F4(A,L) = F2() ) or ex B being Ordinal st
( A = succ B & F4(A,L) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F4(A,L) = F4(A,L) ) ) by A32, ORDINAL1:42; :: thesis: verum
end;
end;
hence ex b being set st S4[a,b] by A28, A30; :: thesis: verum
end;
consider F being Function such that
A33: ( dom F = B & ( for a being set st a in B holds
S4[a,F . a] ) ) from FUNCT_1:sch 2(A17, A25);
 reconsider L = F as T-Sequence by A33, ORDINAL1:def 7;
take L ; :: thesis: S1[B,L]
thus dom L = B by A33; :: thesis: ( ( {} in B implies L . {} = F2() ) & ( for A being Ordinal st succ A in B holds
L . (succ A) = F3(A,(L . A)) ) & ( for A being Ordinal st A in B & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A)) ) )
thus ( {} in B implies L . {} = F2() ) :: thesis: ( ( for A being Ordinal st succ A in B holds
L . (succ A) = F3(A,(L . A)) ) & ( for A being Ordinal st A in B & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A)) ) )
proof
assume {} in B ; :: thesis: L . {} = F2()
then ex A being Ordinal ex K being T-Sequence st
( A = {} & K = G . {} & ( ( A = {} & F . {} = F2() ) or ex B being Ordinal st
( A = succ B & F . {} = F3(B,(K . B)) ) or ( A <> {} & A is limit_ordinal & F . {} = F4(A,K) ) ) ) by A33;
hence L . {} = F2() ; :: thesis: verum
end;
A34: for A being Ordinal
for L1 being T-Sequence st A in B & L1 = G . A holds
L | A = L1
proof
defpred S5[ Ordinal] means for L1 being T-Sequence st $1 in B & L1 = G . $1 holds
L | $1 = L1;
A35: for A being Ordinal st ( for C being Ordinal st C in A holds
S5[C] ) holds
S5[A]
proof
let A be Ordinal; :: thesis: ( ( for C being Ordinal st C in A holds
S5[C] ) implies S5[A] )
assume A36: for C being Ordinal st C in A holds
for L1 being T-Sequence st C in B & L1 = G . C holds
L | C = L1 ; :: thesis: S5[A]
let L1 be T-Sequence; :: thesis: ( A in B & L1 = G . A implies L | A = L1 )
assume A37: ( A in B & L1 = G . A ) ; :: thesis: L | A = L1
then A38: [A,L1] in G by A14, FUNCT_1:8;
then A39: ( S1[A,L1] & A c= dom L ) by A13, A33, A37, ORDINAL1:def 2;
then A40: ( dom L1 = A & dom (L | A) = A & ( {} in A implies L1 . {} = F2() ) & ( for B being Ordinal
for x being set st succ B in A & x = L1 . B holds
L1 . (succ B) = F3(B,x) ) & ( for B being Ordinal
for L2 being T-Sequence st B in A & B <> {} & B is limit_ordinal & L2 = L1 | B holds
L1 . B = F4(B,L2) ) ) by RELAT_1:91;
now
let x be set ; :: thesis: ( x in A implies L1 . x = (L | A) . x )
assume A41: x in A ; :: thesis: L1 . x = (L | A) . x
then reconsider x' = x as Ordinal ;
A42: x' in B by A37, A41, ORDINAL1:19;
then consider A1 being Ordinal, L2 being T-Sequence such that
A43: ( A1 = x' & L2 = G . x' ) and
A44: ( ( A1 = {} & L . x' = F2() ) or ex B being Ordinal st
( A1 = succ B & L . x' = F3(B,(L2 . B)) ) or ( A1 <> {} & A1 is limit_ordinal & L . x' = F4(A1,L2) ) ) by A33;
A45: ( L | x' = L2 & (L | A) . x = L . x ) by A36, A41, A42, A43, FUNCT_1:72;
for D being Ordinal
for L3 being T-Sequence st D = x' & L3 = L1 | x' holds
S1[D,L3]
proof
let D be Ordinal; :: thesis: for L3 being T-Sequence st D = x' & L3 = L1 | x' holds
S1[D,L3]
let L3 be T-Sequence; :: thesis: ( D = x' & L3 = L1 | x' implies S1[D,L3] )
assume A46: ( D = x' & L3 = L1 | x' ) ; :: thesis: S1[D,L3]
x' c= A by A41, ORDINAL1:def 2;
hence dom L3 = D by A39, A46, RELAT_1:91; :: thesis: ( ( {} in D implies L3 . {} = F2() ) & ( for A being Ordinal st succ A in D holds
L3 . (succ A) = F3(A,(L3 . A)) ) & ( for A being Ordinal st A in D & A <> {} & A is limit_ordinal holds
L3 . A = F4(A,(L3 | A)) ) )
thus ( {} in D implies L3 . {} = F2() ) by A39, A41, A46, FUNCT_1:72, ORDINAL1:19; :: thesis: ( ( for A being Ordinal st succ A in D holds
L3 . (succ A) = F3(A,(L3 . A)) ) & ( for A being Ordinal st A in D & A <> {} & A is limit_ordinal holds
L3 . A = F4(A,(L3 | A)) ) )
thus for C being Ordinal st succ C in D holds
L3 . (succ C) = F3(C,(L3 . C)) :: thesis: for A being Ordinal st A in D & A <> {} & A is limit_ordinal holds
L3 . A = F4(A,(L3 | A))
proof
let C be Ordinal; :: thesis: ( succ C in D implies L3 . (succ C) = F3(C,(L3 . C)) )
assume A47: succ C in D ; :: thesis: L3 . (succ C) = F3(C,(L3 . C))
A48: C in succ C by ORDINAL1:10;
then C in D by A47, ORDINAL1:19;
then A49: ( succ C in A & succ C in x' & C in A & C in x' ) by A41, A46, A47, ORDINAL1:19;
( (L1 | x') . (succ C) = L1 . (succ C) & (L1 | x') . C = L1 . C ) by A46, A47, A48, FUNCT_1:72, ORDINAL1:19;
hence L3 . (succ C) = F3(C,(L3 . C)) by A13, A38, A46, A49; :: thesis: verum
end;
let C be Ordinal; :: thesis: ( C in D & C <> {} & C is limit_ordinal implies L3 . C = F4(C,(L3 | C)) )
assume A50: ( C in D & C <> {} & C is limit_ordinal ) ; :: thesis: L3 . C = F4(C,(L3 | C))
then C c= x' by A46, ORDINAL1:def 2;
then ( L1 | C = L3 | C & C in A ) by A41, A46, A50, FUNCT_1:82, ORDINAL1:19;
then ( L1 . C = F4(C,(L3 | C)) & (L1 | x') . C = L1 . C ) by A13, A38, A46, A50, FUNCT_1:72;
hence L3 . C = F4(C,(L3 | C)) by A46; :: thesis: verum
end;
then [x',(L1 | x')] in G by A13, A42;
then A51: L1 | x' = L2 by A43, FUNCT_1:8;
now
given D being Ordinal such that A52: x' = succ D ; :: thesis: L1 . x = (L | A) . x
consider C being Ordinal such that
A53: ( A1 = succ C & L . x' = F3(C,(L2 . C)) ) by A43, A44, A52, ORDINAL1:42;
( C = D & L1 . x = F3(D,(L1 . D)) ) by A13, A38, A41, A43, A52, A53, ORDINAL1:12;
hence L1 . x = (L | A) . x by A45, A51, A52, A53, FUNCT_1:72, ORDINAL1:10; :: thesis: verum
end;
hence L1 . x = (L | A) . x by A13, A38, A41, A43, A44, A45, A51; :: thesis: verum
end;
hence L | A = L1 by A40, FUNCT_1:9; :: thesis: verum
end;
thus for A being Ordinal holds S5[A] from ORDINAL1:sch 2(A35); :: thesis: verum
end;
thus for A being Ordinal st succ A in B holds
L . (succ A) = F3(A,(L . A)) :: thesis: for A being Ordinal st A in B & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A))
proof
let A be Ordinal; :: thesis: ( succ A in B implies L . (succ A) = F3(A,(L . A)) )
assume A54: succ A in B ; :: thesis: L . (succ A) = F3(A,(L . A))
then consider C being Ordinal, K being T-Sequence such that
A55: ( C = succ A & K = G . (succ A) ) and
A56: ( ( C = {} & F . (succ A) = F2() ) or ex B being Ordinal st
( C = succ B & F . (succ A) = F3(B,(K . B)) ) or ( C <> {} & C is limit_ordinal & F . (succ A) = F4(C,K) ) ) by A33;
consider D being Ordinal such that
A57: ( C = succ D & F . (succ A) = F3(D,(K . D)) ) by A55, A56, ORDINAL1:42;
( A = D & K = L | (succ A) & A in succ A ) by A34, A54, A55, A57, ORDINAL1:10, ORDINAL1:12;
hence L . (succ A) = F3(A,(L . A)) by A57, FUNCT_1:72; :: thesis: verum
end;
let D be Ordinal; :: thesis: ( D in B & D <> {} & D is limit_ordinal implies L . D = F4(D,(L | D)) )
assume A58: ( D in B & D <> {} & D is limit_ordinal ) ; :: thesis: L . D = F4(D,(L | D))
then ex A being Ordinal ex K being T-Sequence st
( A = D & K = G . D & ( ( A = {} & F . D = F2() ) or ex B being Ordinal st
( A = succ B & F . D = F3(B,(K . B)) ) or ( A <> {} & A is limit_ordinal & F . D = F4(A,K) ) ) ) by A33;
hence L . D = F4(D,(L | D)) by A34, A58, ORDINAL1:42; :: thesis: verum
end;
for A being Ordinal holds S2[A] from ORDINAL1:sch 2(A1);
 hence ex L being T-Sequence st
( dom L = F1() & ( {} in F1() implies L . {} = F2() ) & ( for A being Ordinal st succ A in F1() holds
L . (succ A) = F3(A,(L . A)) ) & ( for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A)) ) ) ; :: thesis: verum