defpred S1[ set , set , set ] means ex O2 being Ordinal st
( O2 = $3 & ( for X being set
for n being Nat st X c= Rank (the_rank_of $2) holds
ex Y being set st
( Y c= Rank O2 & P1[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set
for n being Nat st X c= Rank (the_rank_of $2) holds
ex Y being set st
( Y c= Rank O & P1[n,X,Y] ) ) holds
O2 c= O ) );
A2: for n being Nat
for x being set ex y being set st S1[n,x,y]
proof
defpred S2[ object , object ] means for m being Nat ex y being set st
( $2 is Ordinal & y c= Rank (the_rank_of $2) & P1[m,$1,y] );
let n be Nat; :: thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; :: thesis: ex y being set st S1[n,x,y]
defpred S3[ Ordinal] means for X being set
for n being Nat st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank $1 & P1[n,X,Y] );
A3: for x9 being object st x9 in bool (Rank (the_rank_of x)) holds
ex o being object st S2[x9,o]
proof
let x9 be object ; :: thesis: ( x9 in bool (Rank (the_rank_of x)) implies ex o being object st S2[x9,o] )
assume x9 in bool (Rank (the_rank_of x)) ; :: thesis: ex o being object st S2[x9,o]
defpred S4[ object , object ] means ex y being set st
( $2 is Ordinal & y c= Rank (the_rank_of $2) & P1[$1,x9,y] );
A4: for e being object st e in NAT holds
ex u being object st S4[e,u]
proof
let i be object ; :: thesis: ( i in NAT implies ex u being object st S4[i,u] )
assume i in NAT ; :: thesis: ex u being object st S4[i,u]
then reconsider i9 = i as Nat ;
thus ex o being object ex y being set st
( o is Ordinal & y c= Rank (the_rank_of o) & P1[i,x9,y] ) :: thesis: verum
proof
x9 is set by TARSKI:1;
then consider y being set such that
A5: P1[i9,x9,y] by A1;
take o = the_rank_of y; :: thesis: ex y being set st
( o is Ordinal & y c= Rank (the_rank_of o) & P1[i,x9,y] )
take y ; :: thesis: ( o is Ordinal & y c= Rank (the_rank_of o) & P1[i,x9,y] )
thus o is Ordinal ; :: thesis: ( y c= Rank (the_rank_of o) & P1[i,x9,y] )
the_rank_of (the_rank_of y) = the_rank_of y by CLASSES1:73;
hence y c= Rank (the_rank_of o) by CLASSES1:65; :: thesis: P1[i,x9,y]
thus P1[i,x9,y] by A5; :: thesis: verum
end;
end;
consider h being Function such that
A6: dom h = NAT and
A7: for i being object st i in NAT holds
S4[i,h . i] from CLASSES1:sch 1(A4);
 take o = sup (rng h); :: thesis: S2[x9,o]
thus for m being Nat ex y being set st
( o is Ordinal & y c= Rank (the_rank_of o) & P1[m,x9,y] ) :: thesis: verum
proof
let m be Nat; :: thesis: ex y being set st
( o is Ordinal & y c= Rank (the_rank_of o) & P1[m,x9,y] )
A8: m in NAT by ORDINAL1:def 12;
then consider y being set such that
A9: h . m is Ordinal and
A10: y c= Rank (the_rank_of (h . m)) and
A11: P1[m,x9,y] by A7;
reconsider O = h . m as Ordinal by A9;
h . m in rng h by A6, A8, FUNCT_1:def 3;
then h . m in sup (rng h) by A9, ORDINAL2:19;
then h . m c= o by ORDINAL1:def 2;
then A12: Rank O c= Rank o by CLASSES1:37;
take y ; :: thesis: ( o is Ordinal & y c= Rank (the_rank_of o) & P1[m,x9,y] )
thus o is Ordinal ; :: thesis: ( y c= Rank (the_rank_of o) & P1[m,x9,y] )
y c= Rank O by A10, CLASSES1:73;
then y c= Rank o by A12;
hence y c= Rank (the_rank_of o) by CLASSES1:73; :: thesis: P1[m,x9,y]
thus P1[m,x9,y] by A11; :: thesis: verum
end;
end;
consider f being Function such that
A13: dom f = bool (Rank (the_rank_of x)) and
A14: for x9 being object st x9 in bool (Rank (the_rank_of x)) holds
S2[x9,f . x9] from CLASSES1:sch 1(A3);
 A15: ex O being Ordinal st S3[O]
proof
take O2 = sup (rng f); :: thesis: S3[O2]
thus for X being set
for m being Nat st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O2 & P1[m,X,Y] ) :: thesis: verum
proof
let X be set ; :: thesis: for m being Nat st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O2 & P1[m,X,Y] )
let m be Nat; :: thesis: ( X c= Rank (the_rank_of x) implies ex Y being set st
( Y c= Rank O2 & P1[m,X,Y] ) )
assume A16: X c= Rank (the_rank_of x) ; :: thesis: ex Y being set st
( Y c= Rank O2 & P1[m,X,Y] )
then consider Y being set such that
A17: f . X is Ordinal and
A18: Y c= Rank (the_rank_of (f . X)) and
A19: P1[m,X,Y] by A14;
reconsider O = f . X as Ordinal by A17;
f . X in rng f by A13, A16, FUNCT_1:def 3;
then f . X in sup (rng f) by A17, ORDINAL2:19;
then f . X c= O2 by ORDINAL1:def 2;
then A20: Rank O c= Rank O2 by CLASSES1:37;
take Y ; :: thesis: ( Y c= Rank O2 & P1[m,X,Y] )
the_rank_of O = O by CLASSES1:73;
hence Y c= Rank O2 by A18, A20; :: thesis: P1[m,X,Y]
thus P1[m,X,Y] by A19; :: thesis: verum
end;
end;
consider O2 being Ordinal such that
A21: ( S3[O2] & ( for O being Ordinal st S3[O] holds
O2 c= O ) ) from ORDINAL1:sch 1(A15);
 take O2 ; :: thesis: S1[n,x,O2]
thus S1[n,x,O2] by A21; :: thesis: verum
end;
A22: for n being Nat
for x, y1, y2 being set st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2
proof
let n be Nat; :: thesis: for x, y1, y2 being set st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2
let x, y1, y2 be set ; :: thesis: ( S1[n,x,y1] & S1[n,x,y2] implies y1 = y2 )
assume that
A23: S1[n,x,y1] and
A24: S1[n,x,y2] ; :: thesis: y1 = y2
consider O2 being Ordinal such that
A25: O2 = y2 and
A26: ( ( for X being set
for n being Nat st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O2 & P1[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set
for n being Nat st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O & P1[n,X,Y] ) ) holds
O2 c= O ) ) by A24;
consider O1 being Ordinal such that
A27: O1 = y1 and
A28: ( ( for X being set
for n being Nat st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O1 & P1[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set
for n being Nat st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O & P1[n,X,Y] ) ) holds
O1 c= O ) ) by A23;
( O1 c= O2 & O2 c= O1 ) by A28, A26;
hence y1 = y2 by A27, A25, XBOOLE_0:def 10; :: thesis: verum
end;
ex f being Function st
( dom f = NAT & f . 0 = the_rank_of F1() & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) )
proof
deffunc H1( Nat) -> set = { k where k is Nat : k <= $1 } ;
A29: for p, q being Function
for k being Nat st dom p = H1(k) & dom q = H1(k + 1) & p . 0 = q . 0 & ( for n being Nat st n < k holds
( S1[n,p . n,p . (n + 1)] & S1[n,q . n,q . (n + 1)] ) ) holds
p . k = q . k
proof
let p, q be Function; :: thesis: for k being Nat st dom p = H1(k) & dom q = H1(k + 1) & p . 0 = q . 0 & ( for n being Nat st n < k holds
( S1[n,p . n,p . (n + 1)] & S1[n,q . n,q . (n + 1)] ) ) holds
p . k = q . k
let k be Nat; :: thesis: ( dom p = H1(k) & dom q = H1(k + 1) & p . 0 = q . 0 & ( for n being Nat st n < k holds
( S1[n,p . n,p . (n + 1)] & S1[n,q . n,q . (n + 1)] ) ) implies p . k = q . k )
defpred S2[ Nat] means ( $1 <= k implies p . $1 = q . $1 );
assume that
dom p = H1(k) and
dom q = H1(k + 1) and
A30: p . 0 = q . 0 and
A31: for n being Nat st n < k holds
( S1[n,p . n,p . (n + 1)] & S1[n,q . n,q . (n + 1)] ) ; :: thesis: p . k = q . k
A32: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A33: ( n <= k implies p . n = q . n ) ; :: thesis: S2[n + 1]
assume n + 1 <= k ; :: thesis: p . (n + 1) = q . (n + 1)
then A34: n < k by NAT_1:13;
then A35: S1[n,p . n,p . (n + 1)] by A31;
S1[n,p . n,q . (n + 1)] by A31, A33, A34;
hence p . (n + 1) = q . (n + 1) by A22, A35; :: thesis: verum
end;
A36: S2[ 0 ] by A30;
for n being Nat holds S2[n] from NAT_1:sch 2(A36, A32);
 hence p . k = q . k ; :: thesis: verum
end;
A37: for n being Nat ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) )
proof
defpred S2[ Nat] means ex p being Function st
( dom p = H1($1) & p . 0 = the_rank_of F1() & ( for k being Nat st k < $1 holds
S1[k,p . k,p . (k + 1)] ) );
A38: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
given p being Function such that dom p = H1(n) and
A39: p . 0 = the_rank_of F1() and
A40: for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ; :: thesis: S2[n + 1]
consider z being set such that
A41: S1[n,p . n,z] by A2;
defpred S3[ object , object ] means for k being Nat st k = $1 holds
( ( k <= n implies $2 = p . k ) & ( k = n + 1 implies $2 = z ) );
A42: for x being object st x in H1(n + 1) holds
ex y being object st S3[x,y]
proof
let x be object ; :: thesis: ( x in H1(n + 1) implies ex y being object st S3[x,y] )
assume x in H1(n + 1) ; :: thesis: ex y being object st S3[x,y]
then A43: ex m being Nat st
( m = x & m <= n + 1 ) ;
then reconsider t = x as Nat ;
A44: ( t <= n implies ex y being object st S3[x,y] )
proof
assume A45: t <= n ; :: thesis: ex y being object st S3[x,y]
take p . x ; :: thesis: S3[x,p . x]
let k be Nat; :: thesis: ( k = x implies ( ( k <= n implies p . x = p . k ) & ( k = n + 1 implies p . x = z ) ) )
assume A46: k = x ; :: thesis: ( ( k <= n implies p . x = p . k ) & ( k = n + 1 implies p . x = z ) )
hence ( k <= n implies p . x = p . k ) ; :: thesis: ( k = n + 1 implies p . x = z )
assume k = n + 1 ; :: thesis: p . x = z
then n + 1 <= n + 0 by A45, A46;
hence p . x = z by XREAL_1:6; :: thesis: verum
end;
( t = n + 1 implies ex y being object st S3[x,y] )
proof
assume A47: t = n + 1 ; :: thesis: ex y being object st S3[x,y]
take z ; :: thesis: S3[x,z]
let k be Nat; :: thesis: ( k = x implies ( ( k <= n implies z = p . k ) & ( k = n + 1 implies z = z ) ) )
assume A48: k = x ; :: thesis: ( ( k <= n implies z = p . k ) & ( k = n + 1 implies z = z ) )
thus ( k <= n implies z = p . k ) :: thesis: ( k = n + 1 implies z = z )
proof
assume k <= n ; :: thesis: z = p . k
then n + 1 <= n + 0 by A47, A48;
hence z = p . k by XREAL_1:6; :: thesis: verum
end;
thus ( k = n + 1 implies z = z ) ; :: thesis: verum
end;
hence ex y being object st S3[x,y] by A43, A44, NAT_1:8; :: thesis: verum
end;
consider q being Function such that
A49: ( dom q = H1(n + 1) & ( for x being object st x in H1(n + 1) holds
S3[x,q . x] ) ) from CLASSES1:sch 1(A42);
 take q ; :: thesis: ( dom q = H1(n + 1) & q . 0 = the_rank_of F1() & ( for k being Nat st k < n + 1 holds
S1[k,q . k,q . (k + 1)] ) )
thus dom q = H1(n + 1) by A49; :: thesis: ( q . 0 = the_rank_of F1() & ( for k being Nat st k < n + 1 holds
S1[k,q . k,q . (k + 1)] ) )
0 in H1(n + 1) ;
hence q . 0 = the_rank_of F1() by A39, A49; :: thesis: for k being Nat st k < n + 1 holds
S1[k,q . k,q . (k + 1)]
let k be Nat; :: thesis: ( k < n + 1 implies S1[k,q . k,q . (k + 1)] )
assume A50: k < n + 1 ; :: thesis: S1[k,q . k,q . (k + 1)]
A51: now :: thesis: ( k <> n implies S1[k,q . k,q . (k + 1)] )
A52: k + 1 <= n + 1 by A50, NAT_1:13;
assume k <> n ; :: thesis: S1[k,q . k,q . (k + 1)]
then k + 1 <> n + 1 ;
then A53: k + 1 <= n by A52, NAT_1:8;
then A54: k < n by NAT_1:13;
k + 1 in H1(n + 1) by A52;
then A55: q . (k + 1) = p . (k + 1) by A49, A53;
k in H1(n + 1) by A50;
then p . k = q . k by A49, A54;
hence S1[k,q . k,q . (k + 1)] by A40, A55, A54; :: thesis: verum
end;
now :: thesis: ( k = n implies S1[k,q . k,q . (k + 1)] )
assume A56: k = n ; :: thesis: S1[k,q . k,q . (k + 1)]
then k <= n + 1 by NAT_1:11;
then k in H1(n + 1) ;
then A57: q . k = p . k by A49, A56;
k + 1 in H1(n + 1) by A56;
then q . (k + 1) = z by A49, A56;
hence S1[k,q . k,q . (k + 1)] by A41, A56, A57; :: thesis: verum
end;
hence S1[k,q . k,q . (k + 1)] by A51; :: thesis: verum
end;
A58: S2[ 0 ]
proof
set s = H1( 0 ) --> (the_rank_of F1());
take H1( 0 ) --> (the_rank_of F1()) ; :: thesis: ( dom (H1( 0 ) --> (the_rank_of F1())) = H1( 0 ) & (H1( 0 ) --> (the_rank_of F1())) . 0 = the_rank_of F1() & ( for k being Nat st k < 0 holds
S1[k,(H1( 0 ) --> (the_rank_of F1())) . k,(H1( 0 ) --> (the_rank_of F1())) . (k + 1)] ) )
thus dom (H1( 0 ) --> (the_rank_of F1())) = H1( 0 ) by FUNCOP_1:13; :: thesis: ( (H1( 0 ) --> (the_rank_of F1())) . 0 = the_rank_of F1() & ( for k being Nat st k < 0 holds
S1[k,(H1( 0 ) --> (the_rank_of F1())) . k,(H1( 0 ) --> (the_rank_of F1())) . (k + 1)] ) )
0 in H1( 0 ) ;
hence (H1( 0 ) --> (the_rank_of F1())) . 0 = the_rank_of F1() by FUNCOP_1:7; :: thesis: for k being Nat st k < 0 holds
S1[k,(H1( 0 ) --> (the_rank_of F1())) . k,(H1( 0 ) --> (the_rank_of F1())) . (k + 1)]
thus for k being Nat st k < 0 holds
S1[k,(H1( 0 ) --> (the_rank_of F1())) . k,(H1( 0 ) --> (the_rank_of F1())) . (k + 1)] ; :: thesis: verum
end;
thus for n being Nat holds S2[n] from NAT_1:sch 2(A58, A38); :: thesis: verum
end;
ex f being Function st
( dom f = NAT & ( for n being Nat ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n ) ) )
proof
defpred S2[ object , object ] means for n being Nat st n = $1 holds
ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) & $2 = p . n );
A59: for x being object st x in NAT holds
ex y being object st S2[x,y]
proof
let x be object ; :: thesis: ( x in NAT implies ex y being object st S2[x,y] )
assume x in NAT ; :: thesis: ex y being object st S2[x,y]
then reconsider n = x as Nat ;
consider p being Function such that
A60: ( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) ) by A37;
take p . n ; :: thesis: S2[x,p . n]
let k be Nat; :: thesis: ( k = x implies ex p being Function st
( dom p = H1(k) & p . 0 = the_rank_of F1() & ( for k being Nat st k < k holds
S1[k,p . k,p . (k + 1)] ) & p . n = p . k ) )
assume A61: k = x ; :: thesis: ex p being Function st
( dom p = H1(k) & p . 0 = the_rank_of F1() & ( for k being Nat st k < k holds
S1[k,p . k,p . (k + 1)] ) & p . n = p . k )
take p ; :: thesis: ( dom p = H1(k) & p . 0 = the_rank_of F1() & ( for k being Nat st k < k holds
S1[k,p . k,p . (k + 1)] ) & p . n = p . k )
thus ( dom p = H1(k) & p . 0 = the_rank_of F1() & ( for k being Nat st k < k holds
S1[k,p . k,p . (k + 1)] ) & p . n = p . k ) by A60, A61; :: thesis: verum
end;
consider f being Function such that
A62: ( dom f = NAT & ( for x being object st x in NAT holds
S2[x,f . x] ) ) from CLASSES1:sch 1(A59);
 take f ; :: thesis: ( dom f = NAT & ( for n being Nat ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n ) ) )
thus dom f = NAT by A62; :: thesis: for n being Nat ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n )
let n be Nat; :: thesis: ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n )
n in NAT by ORDINAL1:def 12;
then consider p being Function such that
A63: ( dom p = H1(n) & p . 0 = the_rank_of F1() ) and
A64: for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] and
A65: f . n = p . n by A62;
take p ; :: thesis: ( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n )
thus ( dom p = H1(n) & p . 0 = the_rank_of F1() ) by A63; :: thesis: ( ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n )
thus for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] by A64; :: thesis: f . n = p . n
thus f . n = p . n by A65; :: thesis: verum
end;
then consider f being Function such that
A66: dom f = NAT and
A67: for n being Nat ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n ) ;
take f ; :: thesis: ( dom f = NAT & f . 0 = the_rank_of F1() & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) )
thus dom f = NAT by A66; :: thesis: ( f . 0 = the_rank_of F1() & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) )
ex p being Function st
( dom p = H1( 0 ) & p . 0 = the_rank_of F1() & ( for k being Nat st k < 0 holds
S1[k,p . k,p . (k + 1)] ) & f . 0 = p . 0 ) by A67;
hence f . 0 = the_rank_of F1() ; :: thesis: for n being Nat holds S1[n,f . n,f . (n + 1)]
let d be Nat; :: thesis: S1[d,f . d,f . (d + 1)]
consider p being Function such that
A68: dom p = H1(d + 1) and
A69: p . 0 = the_rank_of F1() and
A70: for k being Nat st k < d + 1 holds
S1[k,p . k,p . (k + 1)] and
A71: f . (d + 1) = p . (d + 1) by A67;
consider q being Function such that
A72: dom q = H1(d) and
A73: q . 0 = the_rank_of F1() and
A74: for k being Nat st k < d holds
S1[k,q . k,q . (k + 1)] and
A75: f . d = q . d by A67;
( dom p = H1(d + 1) & dom q = H1(d) & p . 0 = q . 0 & ( for k being Nat st k < d holds
( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) ) )
proof
thus dom p = H1(d + 1) by A68; :: thesis: ( dom q = H1(d) & p . 0 = q . 0 & ( for k being Nat st k < d holds
( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) ) )
thus dom q = H1(d) by A72; :: thesis: ( p . 0 = q . 0 & ( for k being Nat st k < d holds
( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) ) )
thus p . 0 = q . 0 by A69, A73; :: thesis: for k being Nat st k < d holds
( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] )
let k be Nat; :: thesis: ( k < d implies ( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) )
assume A76: k < d ; :: thesis: ( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] )
hence S1[k,q . k,q . (k + 1)] by A74; :: thesis: S1[k,p . k,p . (k + 1)]
d <= d + 1 by NAT_1:11;
then k < d + 1 by A76, XXREAL_0:2;
hence S1[k,p . k,p . (k + 1)] by A70; :: thesis: verum
end;
then p . d = q . d by A29;
hence S1[d,f . d,f . (d + 1)] by A70, A71, A75, XREAL_1:29; :: thesis: verum
end;
then consider g being Function such that
A77: dom g = NAT and
A78: g . 0 = the_rank_of F1() and
A79: for n being Nat holds S1[n,g . n,g . (n + 1)] ;
defpred S2[ object , object ] means ex i being Nat st
( i = $1 `2 & P1[$1 `2 ,$1 `1 ,$2 `1 ] & $2 `2 = i + 1 & ( for y being set holds
( not P1[$1 `2 ,$1 `1 ,y] or not the_rank_of y in the_rank_of ($2 `1) ) ) );
A80: ( [F1(),0] `1 = F1() & [F1(),0] `2 = 0 ) ;
set beta = sup (rng g);
A81: for x being object st x in [:(Rank (sup (rng g))),NAT:] holds
ex u being object st S2[x,u]
proof
let x be object ; :: thesis: ( x in [:(Rank (sup (rng g))),NAT:] implies ex u being object st S2[x,u] )
defpred S3[ Ordinal] means ex y being set st
( y c= Rank $1 & P1[x `2 ,x `1 ,y] );
assume x in [:(Rank (sup (rng g))),NAT:] ; :: thesis: ex u being object st S2[x,u]
then consider a, b being object such that
A82: a in Rank (sup (rng g)) and
A83: b in NAT and
A84: x = [a,b] by ZFMISC_1:def 2;
reconsider b = b as Nat by A83;
A85: ( x `2 = b & x `1 = a ) by A84;
the_rank_of a in sup (rng g) by A82, CLASSES1:66;
then consider alfa being Ordinal such that
A86: alfa in rng g and
A87: the_rank_of a c= alfa by ORDINAL2:21;
consider k being object such that
A88: k in dom g and
A89: alfa = g . k by A86, FUNCT_1:def 3;
reconsider k = k as Nat by A77, A88;
A90: S1[k,alfa,g . (k + 1)] by A79, A89;
then reconsider O2 = g . (k + 1) as Ordinal ;
reconsider a = a as set by TARSKI:1;
a c= Rank alfa by A87, CLASSES1:65;
then a c= Rank (the_rank_of alfa) by CLASSES1:73;
then ex y being set st
( y c= Rank O2 & P1[x `2 ,x `1 ,y] ) by A90, A85;
then A91: ex O being Ordinal st S3[O] ;
consider O being Ordinal such that
A92: S3[O] and
A93: for O9 being Ordinal st S3[O9] holds
O c= O9 from ORDINAL1:sch 1(A91);
 consider Y being set such that
A94: Y c= Rank O and
A95: P1[b,a,Y] by A85, A92;
A96: the_rank_of Y c= O by A94, CLASSES1:65;
take u = [Y,(b + 1)]; :: thesis: S2[x,u]
take i = b; :: thesis: ( i = x `2 & P1[x `2 ,x `1 ,u `1 ] & u `2 = i + 1 & ( for y being set holds
( not P1[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) ) ) )
thus i = x `2 by A84; :: thesis: ( P1[x `2 ,x `1 ,u `1 ] & u `2 = i + 1 & ( for y being set holds
( not P1[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) ) ) )
thus P1[x `2 ,x `1 ,u `1 ] by A85, A95; :: thesis: ( u `2 = i + 1 & ( for y being set holds
( not P1[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) ) ) )
thus u `2 = i + 1 ; :: thesis: for y being set holds
( not P1[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) )
given y being set such that A97: P1[x `2 ,x `1 ,y] and
A98: the_rank_of y in the_rank_of (u `1) ; :: thesis: contradiction
A99: y c= Rank (the_rank_of y) by CLASSES1:def 9;
the_rank_of y in the_rank_of Y by A98;
hence contradiction by A93, A97, A96, A99, ORDINAL1:5; :: thesis: verum
end;
consider F being Function such that
dom F = [:(Rank (sup (rng g))),NAT:] and
A100: for x being object st x in [:(Rank (sup (rng g))),NAT:] holds
S2[x,F . x] from CLASSES1:sch 1(A81);
 deffunc H1( Nat, set ) -> object = (F . [$2,$1]) `1 ;
consider f being Function such that
A101: dom f = NAT and
A102: f . 0 = F1() and
A103: for n being Nat holds f . (n + 1) = H1(n,f . n) from NAT_1:sch 11();
 defpred S3[ Nat] means the_rank_of (f . $1) in sup (rng g);
g . 0 in rng g by A77, FUNCT_1:def 3;
then A104: S3[ 0 ] by A78, A102, ORDINAL2:19;
A105: for n being Nat st S3[n] holds
S3[n + 1]
proof
let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
assume A106: the_rank_of (f . n) in sup (rng g) ; :: thesis: S3[n + 1]
then consider o1 being Ordinal such that
A107: o1 in rng g and
A108: the_rank_of (f . n) c= o1 by ORDINAL2:21;
A109: n in NAT by ORDINAL1:def 12;
f . n in Rank (sup (rng g)) by A106, CLASSES1:66;
then A110: [(f . n),n] in [:(Rank (sup (rng g))),NAT:] by A109, ZFMISC_1:87;
consider m being object such that
A111: m in dom g and
A112: g . m = o1 by A107, FUNCT_1:def 3;
reconsider m = m as Nat by A77, A111;
consider o2 being Ordinal such that
A113: o2 = g . (m + 1) and
A114: for X being set
for n being Nat st X c= Rank (the_rank_of (g . m)) holds
ex Y being set st
( Y c= Rank o2 & P1[n,X,Y] ) and
for o being Ordinal st ( for X being set
for n being Nat st X c= Rank (the_rank_of (g . m)) holds
ex Y being set st
( Y c= Rank o & P1[n,X,Y] ) ) holds
o2 c= o by A79;
the_rank_of (f . n) c= the_rank_of (g . m) by A108, A112, CLASSES1:73;
then f . n c= Rank (the_rank_of (g . m)) by CLASSES1:65;
then consider YY being set such that
A115: YY c= Rank o2 and
A116: P1[n,f . n,YY] by A114;
A117: the_rank_of YY c= o2 by A115, CLASSES1:65;
( [(f . n),n] `1 = f . n & [(f . n),n] `2 = n ) ;
then ex i being Nat st
( i = n & P1[n,f . n,(F . [(f . n),n]) `1 ] & (F . [(f . n),n]) `2 = i + 1 & ( for y being set holds
( not P1[n,f . n,y] or not the_rank_of y in the_rank_of ((F . [(f . n),n]) `1) ) ) ) by A100, A110;
then A118: the_rank_of ((F . [(f . n),n]) `1) c= the_rank_of YY by A116, ORDINAL1:16;
g . (m + 1) in rng g by A77, FUNCT_1:def 3;
then A119: o2 in sup (rng g) by A113, ORDINAL2:19;
f . (n + 1) = (F . [(f . n),n]) `1 by A103;
hence S3[n + 1] by A118, A117, A119, ORDINAL1:12, XBOOLE_1:1; :: thesis: verum
end;
A120: for n being Nat holds S3[n] from NAT_1:sch 2(A104, A105);
 defpred S4[ Nat] means P1[$1,f . $1,f . ($1 + 1)];
A121: for n being Nat st S4[n] holds
S4[n + 1]
proof
let n be Nat; :: thesis: ( S4[n] implies S4[n + 1] )
assume P1[n,f . n,f . (n + 1)] ; :: thesis: S4[n + 1]
the_rank_of (f . (n + 1)) in sup (rng g) by A120;
then f . (n + 1) in Rank (sup (rng g)) by CLASSES1:66;
then A122: [(f . (n + 1)),(n + 1)] in [:(Rank (sup (rng g))),NAT:] by ZFMISC_1:87;
( [(f . (n + 1)),(n + 1)] `1 = f . (n + 1) & [(f . (n + 1)),(n + 1)] `2 = n + 1 ) ;
then ex i being Nat st
( i = n + 1 & P1[n + 1,f . (n + 1),(F . [(f . (n + 1)),(n + 1)]) `1 ] & (F . [(f . (n + 1)),(n + 1)]) `2 = i + 1 & ( for y being set holds
( not P1[n + 1,f . (n + 1),y] or not the_rank_of y in the_rank_of ((F . [(f . (n + 1)),(n + 1)]) `1) ) ) ) by A100, A122;
hence S4[n + 1] by A103; :: thesis: verum
end;
take f ; :: thesis: ( dom f = NAT & f . 0 = F1() & ( for n being Nat holds P1[n,f . n,f . (n + 1)] ) )
thus dom f = NAT by A101; :: thesis: ( f . 0 = F1() & ( for n being Nat holds P1[n,f . n,f . (n + 1)] ) )
thus f . 0 = F1() by A102; :: thesis: for n being Nat holds P1[n,f . n,f . (n + 1)]
F1() in Rank (sup (rng g)) by A102, A104, CLASSES1:66;
then [F1(),0] in [:(Rank (sup (rng g))),NAT:] by ZFMISC_1:87;
then ex i being Nat st
( i = [F1(),0] `2 & P1[ 0 ,F1(),(F . [F1(),0]) `1 ] & (F . [F1(),0]) `2 = i + 1 & ( for y being set holds
( not P1[ 0 ,F1(),y] or not the_rank_of y in the_rank_of ((F . [F1(),0]) `1) ) ) ) by A100, A80;
then A123: S4[ 0 ] by A102, A103;
thus for n being Nat holds S4[n] from NAT_1:sch 2(A123, A121); :: thesis: verum