let M be non empty set ; :: thesis:
let i be Element of NAT ; :: thesis:
let H1 be ZF-formula; :: thesis:
let v1 be Function of VAR ,M; :: thesis:
defpred S₁[ ZF-formula, Element of NAT ] means for v1 being Function of VAR ,M st not x. 0 in Free $1 & M,v1 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),($1 <=> ((x. 4) '=' (x. 0 ))))) holds
ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j < $2 & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0 ))))) & def_func' $1,v1 = def_func' H2,v2 );
defpred S₂[ Element of NAT ] means for H being ZF-formula holds S₁[H,$1];
A1: for i being Element of NAT st S₂[i] holds
S₂[i + 1]

let i be Element of NAT ; :: thesis:
assume A2: for H being ZF-formula holds S₁[H,i] ; :: thesis:
let H be ZF-formula; :: thesis:
let v1 be Function of VAR ,M; :: thesis:
assume that
A3: not x. 0 in Free H and
A4: M,v1 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) ; :: thesis:
A5: ( i = 0 implies ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j ((x. 4) '=' (x. 0 ))))) & def_func' H,v1 = def_func' H2,v2 ) )

assume A6: i = 0 ; :: thesis:
consider k being Element of NAT such that
A7: for j being Element of NAT st x. j in variables_in H holds
j < k by Th4;
( k > 4 or not k > 4 ) ;
then consider k1 being Element of NAT such that
A8: ( ( k > 4 & k1 = k ) or ( not k > 4 & k1 = 5 ) ) ;
take F = H / (x. 0 ),(x. k1); :: thesis:
take v1 / (x. k1),(v1 . (x. 0 )) ; :: thesis:
thus for j being Element of NAT st j < i + 1 & x. j in variables_in F & not j = 3 holds
j = 4 :: thesis:

proof

let j be Element of NAT ; :: thesis:
assume j < i + 1 ; :: thesis:
then j <= 0 by A6, NAT_1:13;
then j = 0 by NAT_1:2;
hence ( not x. j in variables_in F or j = 3 or j = 4 ) by A8, ZF_LANG1:86, ZF_LANG1:198; :: thesis:

end;

A9: x. k1 <> x. 0 by A8, ZF_LANG1:86;
k1 <> 3 by A8;
then A10: x. k1 <> x. 3 by ZF_LANG1:86;
A11: x. k1 <> x. 4 by A8, ZF_LANG1:86;
not x. k1 in variables_in H by A7, A8, XXREAL_0:2;
hence ( not x. 0 in Free F & M,v1 / (x. k1),(v1 . (x. 0 )) |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(F <=> ((x. 4) '=' (x. 0 ))))) & def_func' H,v1 = def_func' F,(v1 / (x. k1),(v1 . (x. 0 ))) ) by A3, A4, A9, A10, A11, Th15; :: thesis:

end;

A12: ( i <> 0 & i <> 3 & i <> 4 implies ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j ((x. 4) '=' (x. 0 ))))) & def_func' H,v1 = def_func' H2,v2 ) )

proof

A13: x. 3 <> x. 4 by ZF_LANG1:86;
assume that
A14: i <> 0 and
A15: i <> 3 and
A16: i <> 4 ; :: thesis:
A17: x. 0 <> x. i by A14, ZF_LANG1:86;
consider H1 being ZF-formula, v9 being Function of VAR ,M such that
A18: for j being Element of NAT st j ((x. 4) '=' (x. 0 ))))) and
A21: def_func' H,v1 = def_func' H1,v9 by A2, A3, A4;
consider k being Element of NAT such that
A22: for j being Element of NAT st x. j in variables_in (All (x. 4),(x. i),H1) holds
j < k by Th4;
take H2 = H1 / (x. i),(x. k); :: thesis:
take v2 = v9 / (x. k),(v9 . (x. i)); :: thesis:
A23: variables_in (All (x. 4),(x. i),H1) = (variables_in H1) \/ {(x. 4),(x. i)} by ZF_LANG1:160;
x. i in {(x. 4),(x. i)} by TARSKI:def 2;
then A24: x. i in variables_in (All (x. 4),(x. i),H1) by A23, XBOOLE_0:def 3;
then A25: x. i <> x. k by A22;
then A26: v2 / (x. i),(v2 . (x. k)) = (v9 / (x. i),(v2 . (x. k))) / (x. k),(v9 . (x. i)) by FUNCT_7:35;
thus for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 :: thesis:

proof

x. i in {(x. i)} by TARSKI:def 1;
then A27: not x. i in (variables_in H1) \ {(x. i)} by XBOOLE_0:def 5;
A28: not x. i in {(x. k)} by A25, TARSKI:def 1;
let j be Element of NAT ; :: thesis:
A29: variables_in H2 c= ((variables_in H1) \ {(x. i)}) \/ {(x. k)} by ZF_LANG1:201;
assume j x. k by ZF_LANG1:86;
assume A32: x. j in variables_in H2 ; :: thesis:
then ( x. j in (variables_in H1) \ {(x. i)} or x. j in {(x. k)} ) by A29, XBOOLE_0:def 3;
then A33: x. j in variables_in H1 by A31, TARSKI:def 1, XBOOLE_0:def 5;
( j = i or j < i ) by A30, XXREAL_0:1;
hence ( j = 3 or j = 4 ) by A18, A27, A28, A29, A32, A33, XBOOLE_0:def 3; :: thesis:

end;

now

let e be Element of M; :: thesis:
A58: v2 . (x. k) = v9 . (x. i) by FUNCT_7:130;
A59: (v2 / (x. 3),e) . (x. k) = v2 . (x. k) by A54, FUNCT_7:34, ZF_LANG1:86;
M,v9 / (x. 3),e |= Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 )))) by A20, ZF_LANG1:80;
then consider e9 being Element of M such that
A60: M,(v9 / (x. 3),e) / (x. 0 ),e9 |= All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 ))) by ZF_LANG1:82;
A61: (((v9 / (x. 3),e) / (x. 0 ),e9) / (x. 4),e9) . (x. 0 ) = ((v9 / (x. 3),e) / (x. 0 ),e9) . (x. 0 ) by FUNCT_7:34, ZF_LANG1:86;
A62: ((v9 / (x. 3),e) / (x. 0 ),e9) . (x. 0 ) = e9 by FUNCT_7:130;
(((v9 / (x. 3),e) / (x. 0 ),e9) / (x. 4),e9) . (x. 4) = e9 by FUNCT_7:130;
then A63: M,((v9 / (x. 3),e) / (x. 0 ),e9) / (x. 4),e9 |= (x. 4) '=' (x. 0 ) by A61, A62, ZF_MODEL:12;
A64: M,((v9 / (x. 3),e) / (x. 0 ),e9) / (x. 4),e9 |= H1 <=> ((x. 4) '=' (x. 0 )) by A60, ZF_LANG1:80;
then A65: M,((v9 / (x. 3),e) / (x. 0 ),e9) / (x. 4),e9 |= H1 by A63, ZF_MODEL:19;
A66: (v2 / (x. 3),e) . (x. k) = ((v2 / (x. 3),e) / (x. 4),e9) . (x. k) by A43, FUNCT_7:34;
A67: (((v2 / (x. 3),e) / (x. 4),e9) / (x. 0 ),e9) . (x. k) = ((v2 / (x. 3),e) / (x. 4),e9) . (x. k) by A45, FUNCT_7:34, ZF_LANG1:86;
A68: ((v9 / (x. 3),e) / (x. 0 ),e9) / (x. 4),e9 = ((v9 / (x. 3),e) / (x. 4),e9) / (x. 0 ),e9 by FUNCT_7:35, ZF_LANG1:86;
A69: v2 / (x. i),(v2 . (x. k)) = (v9 / (x. i),(v2 . (x. k))) / (x. k),(v9 . (x. i)) by A25, FUNCT_7:35;
A70: v9 / (x. i),(v9 . (x. i)) = v9 by FUNCT_7:37;
((v2 / (x. 3),e) / (x. 4),e9) / (x. 0 ),e9 = (((v9 / (x. 3),e) / (x. 4),e9) / (x. 0 ),e9) / (x. k),(v9 . (x. i)) by A46, A55, A43, A49, A53, A13, Th8;
then A71: M,((v2 / (x. 3),e) / (x. 4),e9) / (x. 0 ),e9 |= H1 by A41, A65, A68, Th6;
(((v2 / (x. 3),e) / (x. 4),e9) / (x. 0 ),e9) / (x. i),(v2 . (x. k)) = (((v2 / (x. i),(v2 . (x. k))) / (x. 3),e) / (x. 4),e9) / (x. 0 ),e9 by A17, A37, A36, A49, A53, A13, Th8;
then M,((v2 / (x. 3),e) / (x. 4),e9) / (x. 0 ),e9 |= H2 by A41, A71, A67, A66, A59, A69, A58, A70, Th13;
then M,(v2 / (x. 3),e) / (x. 4),e9 |= H2 by A51, Th10;
then A72: (def_func' H2,v2) . e = e9 by A51, A57, Th11;
M,((v9 / (x. 3),e) / (x. 4),e9) / (x. 0 ),e9 |= H1 by A64, A63, A68, ZF_MODEL:19;
then M,(v9 / (x. 3),e) / (x. 4),e9 |= H1 by A19, Th10;
hence (def_func' H2,v2) . e = (def_func' H1,v9) . e by A19, A20, A72, Th11; :: thesis:

end;

hence def_func' H2,v2 = def_func' H,v1 by A21, FUNCT_2:113; :: thesis:

end;

now

assume A73: ( i = 3 or i = 4 ) ; :: thesis:
thus ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j ((x. 4) '=' (x. 0 ))))) & def_func' H,v1 = def_func' H2,v2 ) :: thesis:

proof

consider H2 being ZF-formula, v2 being Function of VAR ,M such that
A74: for j being Element of NAT st j ((x. 4) '=' (x. 0 ))))) and
A77: def_func' H,v1 = def_func' H2,v2 by A2, A3, A4;
take H2 ; :: thesis:
take v2 ; :: thesis:
thus for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 :: thesis:

proof

let j be Element of NAT ; :: thesis:
assume that
A78: j < i + 1 and
A79: x. j in variables_in H2 ; :: thesis:
j <= i by A78, NAT_1:13;
then ( j < i or j = i ) by XXREAL_0:1;
hence ( j = 3 or j = 4 ) by A73, A74, A79; :: thesis:

end;

thus ( not x. 0 in Free H2 & M,v2 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0 ))))) & def_func' H,v1 = def_func' H2,v2 ) by A75, A76, A77; :: thesis:

end;

hence ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j ((x. 4) '=' (x. 0 ))))) & def_func' H,v1 = def_func' H2,v2 ) by A12, A5; :: thesis:

end;

A80: S₂[ 0 ]

proof

let H be ZF-formula; :: thesis:
let v1 be Function of VAR ,M; :: thesis:
assume that
A81: not x. 0 in Free H and
A82: M,v1 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) ; :: thesis:
take H ; :: thesis:
take v1 ; :: thesis:
thus ( ( for j being Element of NAT st j < 0 & x. j in variables_in H & not j = 3 holds
j = 4 ) & not x. 0 in Free H & M,v1 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) & def_func' H,v1 = def_func' H,v1 ) by A81, A82, NAT_1:2; :: thesis:

end;

for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A80, A1);
hence ( not x. 0 in Free H1 & M,v1 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 ))))) implies ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j ((x. 4) '=' (x. 0 ))))) & def_func' H1,v1 = def_func' H2,v2 ) ) ; :: thesis: