let M be non empty set ; :: thesis: for i being Element of NAT
for H1 being ZF-formula
for v1 being Function of VAR ,M st not x. 0 in Free H1 & M,v1 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H1 <=> ((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 < i & 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' H1,v1 = def_func' H2,v2 )
let i be Element of NAT ; :: thesis: for H1 being ZF-formula
for v1 being Function of VAR ,M st not x. 0 in Free H1 & M,v1 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H1 <=> ((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 < i & 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' H1,v1 = def_func' H2,v2 )
let H1 be ZF-formula; :: thesis: for v1 being Function of VAR ,M st not x. 0 in Free H1 & M,v1 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H1 <=> ((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 < i & 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' H1,v1 = def_func' H2,v2 )
let v1 be Function of VAR ,M; :: thesis: ( 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 < i & 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' H1,v1 = def_func' H2,v2 ) )
defpred S1[ 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 S2[ Element of NAT ] means for H being ZF-formula holds S1[H,$1];
A1: S2[ 0 ]
proof
let H be ZF-formula; :: thesis: S1[H, 0 ]
let v1 be Function of VAR ,M; :: thesis: ( not x. 0 in Free H & M,v1 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((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 < 0 & 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' H,v1 = def_func' H2,v2 ) )
assume A2: ( not x. 0 in Free H & M,v1 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) ) ; :: thesis: ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j < 0 & 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' H,v1 = def_func' H2,v2 )
take H ; :: thesis: ex v2 being Function of VAR ,M st
( ( 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,v2 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) & def_func' H,v1 = def_func' H,v2 )
take v1 ; :: thesis: ( ( 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 )
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 A2, NAT_1:2; :: thesis: verum
end;
A3: for i being Element of NAT st S2[i] holds
S2[i + 1]
proof
let i be Element of NAT ; :: thesis: ( S2[i] implies S2[i + 1] )
assume A4: for H being ZF-formula holds S1[H,i] ; :: thesis: S2[i + 1]
let H be ZF-formula; :: thesis: S1[H,i + 1]
let v1 be Function of VAR ,M; :: thesis: ( not x. 0 in Free H & M,v1 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((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 < i + 1 & 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' H,v1 = def_func' H2,v2 ) )
assume A5: ( not x. 0 in Free H & M,v1 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) ) ; :: thesis: ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j < i + 1 & 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' H,v1 = def_func' H2,v2 )
A6: ( 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 < i + 1 & 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' H,v1 = def_func' H2,v2 ) )
proof
assume A7: ( i <> 0 & i <> 3 & i <> 4 ) ; :: thesis: ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j < i + 1 & 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' H,v1 = def_func' H2,v2 )
consider H1 being ZF-formula, v' being Function of VAR ,M such that
A8: for j being Element of NAT st j < i & x. j in variables_in H1 & not j = 3 holds
j = 4 and
A9: ( not x. 0 in Free H1 & M,v' |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 ))))) ) and
A10: def_func' H,v1 = def_func' H1,v' by A4, A5;
consider k being Element of NAT such that
A11: for j being Element of NAT st x. j in variables_in (All (x. 4),(x. i),H1) holds
j < k by Th4;
( not x. k in variables_in (All (x. 4),(x. i),H1) & x. i in {(x. 4),(x. i)} & x. 4 in {(x. 4),(x. i)} & variables_in (All (x. 4),(x. i),H1) = (variables_in H1) \/ {(x. 4),(x. i)} ) by A11, TARSKI:def 2, ZF_LANG1:160;
then A12: ( not x. k in variables_in H1 & x. i in variables_in (All (x. 4),(x. i),H1) & x. 4 in variables_in (All (x. 4),(x. i),H1) ) by XBOOLE_0:def 3;
take H2 = H1 / (x. i),(x. k); :: thesis: ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j < i + 1 & 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' H,v1 = def_func' H2,v2 )
take v2 = v' / (x. k),(v' . (x. i)); :: thesis: ( ( for j being Element of NAT st j < i + 1 & 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' H,v1 = def_func' H2,v2 )
( 0 <> k & 3 <> k & 4 <> k & 0 <> i & 3 <> i & 4 <> i & i <> k ) by A7, A11, A12;
then A13: ( x. 0 <> x. k & x. 3 <> x. k & x. 4 <> x. k & x. i <> x. k & x. 0 <> x. i & x. 3 <> x. i & x. 4 <> x. i ) by ZF_LANG1:86;
A14: ( x. 0 <> x. 3 & x. 0 <> x. 4 & x. 3 <> x. 4 ) by ZF_LANG1:86;
( not x. 0 in (Free H1) \ {(x. i)} & not x. 0 in {(x. k)} ) by A9, A13, TARSKI:def 1, XBOOLE_0:def 5;
then A15: ( not x. 0 in ((Free H1) \ {(x. i)}) \/ {(x. k)} & Free H2 c= ((Free H1) \ {(x. i)}) \/ {(x. k)} ) by Th1, XBOOLE_0:def 3;
then A16: not x. 0 in Free H2 ;
thus for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 :: thesis: ( 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 )
proof
let j be Element of NAT ; :: thesis: ( j < i + 1 & x. j in variables_in H2 & not j = 3 implies j = 4 )
assume j < i + 1 ; :: thesis: ( not x. j in variables_in H2 or j = 3 or j = 4 )
then A17: j <= i by NAT_1:13;
then A18: ( j = i or j < i ) by XXREAL_0:1;
x. i in {(x. i)} by TARSKI:def 1;
then ( not x. i in (variables_in H1) \ {(x. i)} & not x. i in {(x. k)} ) by A13, TARSKI:def 1, XBOOLE_0:def 5;
then A19: ( not x. i in ((variables_in H1) \ {(x. i)}) \/ {(x. k)} & variables_in H2 c= ((variables_in H1) \ {(x. i)}) \/ {(x. k)} ) by XBOOLE_0:def 3, ZF_LANG1:201;
assume A20: x. j in variables_in H2 ; :: thesis: ( j = 3 or j = 4 )
then ( x. j in ((variables_in H1) \ {(x. i)}) \/ {(x. k)} & x. j <> x. i & j < k ) by A11, A12, A17, A19, XXREAL_0:2;
then ( not x. j in {(x. i)} & ( x. j in (variables_in H1) \ {(x. i)} or x. j in {(x. k)} ) & x. j <> x. k ) by TARSKI:def 1, XBOOLE_0:def 3, ZF_LANG1:86;
then x. j in variables_in H1 by TARSKI:def 1, XBOOLE_0:def 5;
hence ( j = 3 or j = 4 ) by A8, A18, A19, A20; :: thesis: verum
end;
thus not x. 0 in Free H2 by A15; :: thesis: ( M,v2 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0 ))))) & def_func' H,v1 = def_func' H2,v2 )
A21: (All (x. 3),(Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 )))))) / (x. i),(x. k) = All (x. 3),((Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 ))))) / (x. i),(x. k)) by A13, ZF_LANG1:173
.= All (x. 3),(Ex (x. 0 ),((All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 )))) / (x. i),(x. k))) by A13, ZF_LANG1:178
.= All (x. 3),(Ex (x. 0 ),(All (x. 4),((H1 <=> ((x. 4) '=' (x. 0 ))) / (x. i),(x. k)))) by A13, ZF_LANG1:173
.= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H2 <=> (((x. 4) '=' (x. 0 )) / (x. i),(x. k))))) by ZF_LANG1:177
.= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0 ))))) by A13, ZF_LANG1:166 ;
A22: variables_in (All (x. 3),(Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 )))))) = (variables_in (Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 )))))) \/ {(x. 3)} by ZF_LANG1:155
.= ((variables_in (All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 ))))) \/ {(x. 0 )}) \/ {(x. 3)} by ZF_LANG1:159
.= (((variables_in (H1 <=> ((x. 4) '=' (x. 0 )))) \/ {(x. 4)}) \/ {(x. 0 )}) \/ {(x. 3)} by ZF_LANG1:155
.= ((((variables_in H1) \/ (variables_in ((x. 4) '=' (x. 0 )))) \/ {(x. 4)}) \/ {(x. 0 )}) \/ {(x. 3)} by ZF_LANG1:158
.= ((((variables_in H1) \/ {(x. 4),(x. 0 )}) \/ {(x. 4)}) \/ {(x. 0 )}) \/ {(x. 3)} by ZF_LANG1:151 ;
not x. k in {(x. 4),(x. 0 )} by A13, TARSKI:def 2;
then ( not x. k in (variables_in H1) \/ {(x. 4),(x. 0 )} & not x. k in {(x. 4)} ) by A12, A13, TARSKI:def 1, XBOOLE_0:def 3;
then ( not x. k in ((variables_in H1) \/ {(x. 4),(x. 0 )}) \/ {(x. 4)} & not x. k in {(x. 0 )} ) by A13, TARSKI:def 1, XBOOLE_0:def 3;
then ( not x. k in (((variables_in H1) \/ {(x. 4),(x. 0 )}) \/ {(x. 4)}) \/ {(x. 0 )} & not x. k in {(x. 3)} ) by A13, TARSKI:def 1, XBOOLE_0:def 3;
then A23: ( not x. k in variables_in (All (x. 3),(Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 )))))) & not x. i in variables_in (All (x. 3),(Ex (x. 0 ),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0 )))))) ) by A13, A21, A22, XBOOLE_0:def 3, ZF_LANG1:198;
then ( M,v2 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 ))))) & v2 . (x. k) = v' . (x. i) & v' / (x. i),(v' . (x. i)) = v' & v2 / (x. i),(v2 . (x. k)) = (v' / (x. i),(v2 . (x. k))) / (x. k),(v' . (x. i)) ) by A9, A13, Th6, FUNCT_7:37, FUNCT_7:35, FUNCT_7:130;
hence A24: M,v2 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0 ))))) by A21, A23, Th13; :: thesis: def_func' H,v1 = def_func' H2,v2
now
let e be Element of M; :: thesis: (def_func' H2,v2) . e = (def_func' H1,v') . e
M,v' / (x. 3),e |= Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 )))) by A9, ZF_LANG1:80;
then consider e' being Element of M such that
A25: M,(v' / (x. 3),e) / (x. 0 ),e' |= All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 ))) by ZF_LANG1:82;
( (((v' / (x. 3),e) / (x. 0 ),e') / (x. 4),e') . (x. 4) = e' & (((v' / (x. 3),e) / (x. 0 ),e') / (x. 4),e') . (x. 0 ) = ((v' / (x. 3),e) / (x. 0 ),e') . (x. 0 ) & ((v' / (x. 3),e) / (x. 0 ),e') . (x. 0 ) = e' ) by A14, FUNCT_7:34, FUNCT_7:130;
then A26: ( M,((v' / (x. 3),e) / (x. 0 ),e') / (x. 4),e' |= H1 <=> ((x. 4) '=' (x. 0 )) & M,((v' / (x. 3),e) / (x. 0 ),e') / (x. 4),e' |= (x. 4) '=' (x. 0 ) ) by A25, ZF_LANG1:80, ZF_MODEL:12;
then A27: M,((v' / (x. 3),e) / (x. 0 ),e') / (x. 4),e' |= H1 by ZF_MODEL:19;
A28: ( ((v' / (x. 3),e) / (x. 0 ),e') / (x. 4),e' = ((v' / (x. 3),e) / (x. 4),e') / (x. 0 ),e' & ((v2 / (x. 3),e) / (x. 0 ),e') / (x. 4),e' = ((v2 / (x. 3),e) / (x. 4),e') / (x. 0 ),e' & ((v2 / (x. 3),e) / (x. 4),e') / (x. 0 ),e' = (((v' / (x. 3),e) / (x. 4),e') / (x. 0 ),e') / (x. k),(v' . (x. i)) ) by A13, A14, Th8, FUNCT_7:35;
then A29: M,((v2 / (x. 3),e) / (x. 4),e') / (x. 0 ),e' |= H1 by A12, A27, Th6;
( (((v2 / (x. 3),e) / (x. 4),e') / (x. 0 ),e') . (x. k) = ((v2 / (x. 3),e) / (x. 4),e') . (x. k) & (v2 / (x. 3),e) . (x. k) = ((v2 / (x. 3),e) / (x. 4),e') . (x. k) & (v2 / (x. 3),e) . (x. k) = v2 . (x. k) & (((v2 / (x. 3),e) / (x. 4),e') / (x. 0 ),e') / (x. i),(v2 . (x. k)) = (((v2 / (x. i),(v2 . (x. k))) / (x. 3),e) / (x. 4),e') / (x. 0 ),e' & v2 / (x. i),(v2 . (x. k)) = (v' / (x. i),(v2 . (x. k))) / (x. k),(v' . (x. i)) & v2 . (x. k) = v' . (x. i) & v' / (x. i),(v' . (x. i)) = v' ) by A13, A14, Th8, FUNCT_7:37, FUNCT_7:35, FUNCT_7:34, FUNCT_7:130;
then ( M,((v' / (x. 3),e) / (x. 4),e') / (x. 0 ),e' |= H1 & M,((v2 / (x. 3),e) / (x. 4),e') / (x. 0 ),e' |= H2 ) by A12, A26, A28, A29, Th13, ZF_MODEL:19;
then ( M,(v' / (x. 3),e) / (x. 4),e' |= H1 & M,(v2 / (x. 3),e) / (x. 4),e' |= H2 ) by A9, A16, Th10;
then ( (def_func' H2,v2) . e = e' & (def_func' H1,v') . e = e' ) by A9, A16, A24, Th11;
hence (def_func' H2,v2) . e = (def_func' H1,v') . e ; :: thesis: verum
end;
hence def_func' H2,v2 = def_func' H,v1 by A10, FUNCT_2:113; :: thesis: verum
end;
A30: now
assume A31: ( i = 3 or i = 4 ) ; :: thesis: ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j < i + 1 & 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' H,v1 = def_func' H2,v2 )
thus ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j < i + 1 & 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' H,v1 = def_func' H2,v2 ) :: thesis: verum
proof
consider H2 being ZF-formula, v2 being Function of VAR ,M such that
A32: for j being Element of NAT st j < i & x. j in variables_in H2 & not j = 3 holds
j = 4 and
A33: ( not x. 0 in Free H2 & M,v2 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0 ))))) ) and
A34: def_func' H,v1 = def_func' H2,v2 by A4, A5;
take H2 ; :: thesis: ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j < i + 1 & 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' H,v1 = def_func' H2,v2 )
take v2 ; :: thesis: ( ( for j being Element of NAT st j < i + 1 & 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' H,v1 = def_func' H2,v2 )
thus for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 :: thesis: ( 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 )
proof
let j be Element of NAT ; :: thesis: ( j < i + 1 & x. j in variables_in H2 & not j = 3 implies j = 4 )
assume A35: ( j < i + 1 & x. j in variables_in H2 ) ; :: thesis: ( j = 3 or j = 4 )
then j <= i by NAT_1:13;
then ( j < i or j = i ) by XXREAL_0:1;
hence ( j = 3 or j = 4 ) by A31, A32, A35; :: thesis: verum
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 A33, A34; :: thesis: verum
end;
end;
( i = 0 implies ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j < i + 1 & 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' H,v1 = def_func' H2,v2 ) )
proof
assume A36: i = 0 ; :: thesis: ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j < i + 1 & 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' H,v1 = def_func' H2,v2 )
consider k being Element of NAT such that
A37: 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
A38: ( ( k > 4 & k1 = k ) or ( not k > 4 & k1 = 5 ) ) ;
take F = H / (x. 0 ),(x. k1); :: thesis: ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j < i + 1 & x. j in variables_in F & not j = 3 holds
j = 4 ) & not x. 0 in Free F & M,v2 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(F <=> ((x. 4) '=' (x. 0 ))))) & def_func' H,v1 = def_func' F,v2 )
take v1 / (x. k1),(v1 . (x. 0 )) ; :: thesis: ( ( for j being Element of NAT st j < i + 1 & x. j in variables_in F & not j = 3 holds
j = 4 ) & 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 ))) )
( k1 <> 0 & k1 <> 3 & k1 <> 4 ) by A38;
then A39: ( x. k1 <> x. 0 & x. k1 <> x. 3 & x. k1 <> x. 4 ) by ZF_LANG1:86;
A40: not x. k1 in variables_in H by A37, A38, XXREAL_0:2;
thus for j being Element of NAT st j < i + 1 & x. j in variables_in F & not j = 3 holds
j = 4 :: thesis: ( 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 ))) )
proof
let j be Element of NAT ; :: thesis: ( j < i + 1 & x. j in variables_in F & not j = 3 implies j = 4 )
assume j < i + 1 ; :: thesis: ( not x. j in variables_in F or j = 3 or j = 4 )
then ( j <= 0 & j >= 0 ) by A36, NAT_1:2, NAT_1:13;
then j = 0 ;
hence ( not x. j in variables_in F or j = 3 or j = 4 ) by A38, ZF_LANG1:86, ZF_LANG1:198; :: thesis: verum
end;
( x. 0 <> x. 3 & x. 0 <> x. 4 ) by ZF_LANG1:86;
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 A5, A39, A40, Th15; :: thesis: verum
end;
hence ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j < i + 1 & 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' H,v1 = def_func' H2,v2 ) by A6, A30; :: thesis: verum
end;
for i being Element of NAT holds S2[i] from NAT_1:sch 1(A1, A3);
 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 < i & 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' H1,v1 = def_func' H2,v2 ) ) ; :: thesis: verum