defpred S2[ Function of VAR ,E] means for y being Variable holds
( not $1 . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y );
defpred S3[ set ] means for g being Function of VAR ,E st S2[g] & g . (x. 3) = $1 `1 & g . (x. 4) = $1 `2 holds
E,g |= H;
consider X being set such that
A3: for a being set holds
( a in X iff ( a in [:E,E:] & S3[a] ) ) from XBOOLE_0:sch 1();
 ( X is Relation-like & X is Function-like )
proof
thus for a being set st a in X holds
ex b, c being set st [b,c] = a :: according to RELAT_1:def 1 :: thesis: X is Function-like
proof
let a be set ; :: thesis: ( a in X implies ex b, c being set st [b,c] = a )
assume a in X ; :: thesis: ex b, c being set st [b,c] = a
then a in [:E,E:] by A3;
hence ex b, c being set st [b,c] = a by RELAT_1:def 1; :: thesis: verum
end;
let a be set ; :: according to FUNCT_1:def 1 :: thesis: for b1, b2 being set holds
( not [a,b1] in X or not [a,b2] in X or b1 = b2 )
let b, c be set ; :: thesis: ( not [a,b] in X or not [a,c] in X or b = c )
assume that
A4: [a,b] in X and
A5: [a,c] in X ; :: thesis: b = c
( [a,b] in [:E,E:] & [a,c] in [:E,E:] ) by A3, A4, A5;
then reconsider a9 = a, b9 = b, c9 = c as Element of E by ZFMISC_1:106;
set f = val +* (x. 3),a9;
for x being Variable st (val +* (x. 3),a9) . x <> val . x holds
x = x. 3 by FUNCT_7:34;
then E,val +* (x. 3),a9 |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))) by A2, ZF_MODEL:16;
then consider g being Function of VAR ,E such that
A6: for x being Variable st g . x <> (val +* (x. 3),a9) . x holds
x. 0 = x and
A7: E,g |= All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))) by ZF_MODEL:20;
A8: ( (val +* (x. 3),a9) . (x. 3) = a9 & g . (x. 3) = (val +* (x. 3),a9) . (x. 3) ) by A6, FUNCT_7:130;
set g1 = g +* (x. 4),b9;
A9: (g +* (x. 4),b9) . (x. 4) = b9 by FUNCT_7:130;
A10: S2[g +* (x. 4),b9]
proof
let y be Variable; :: thesis: ( not (g +* (x. 4),b9) . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y )
assume A11: (g +* (x. 4),b9) . y <> val . y ; :: thesis: ( x. 0 = y or x. 3 = y or x. 4 = y )
assume that
A12: x. 0 <> y and
A13: ( x. 3 <> y & x. 4 <> y ) ; :: thesis: contradiction
( (val +* (x. 3),a9) . y = val . y & (g +* (x. 4),b9) . y = g . y ) by A13, FUNCT_7:34;
hence contradiction by A6, A11, A12; :: thesis: verum
end;
for x being Variable st (g +* (x. 4),b9) . x <> g . x holds
x. 4 = x by FUNCT_7:34;
then A14: E,g +* (x. 4),b9 |= H <=> ((x. 4) '=' (x. 0 )) by A7, ZF_MODEL:16;
A15: (g +* (x. 4),b9) . (x. 3) = g . (x. 3) by FUNCT_7:34;
( [a,b] `1 = a9 & [a,b] `2 = b9 ) by MCART_1:7;
then E,g +* (x. 4),b9 |= H by A3, A4, A9, A15, A8, A10;
then E,g +* (x. 4),b9 |= (x. 4) '=' (x. 0 ) by A14, ZF_MODEL:19;
then A16: (g +* (x. 4),b9) . (x. 4) = (g +* (x. 4),b9) . (x. 0 ) by ZF_MODEL:12;
set g2 = g +* (x. 4),c9;
A17: (g +* (x. 4),c9) . (x. 4) = c9 by FUNCT_7:130;
A18: S2[g +* (x. 4),c9]
proof
let y be Variable; :: thesis: ( not (g +* (x. 4),c9) . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y )
assume A19: (g +* (x. 4),c9) . y <> val . y ; :: thesis: ( x. 0 = y or x. 3 = y or x. 4 = y )
assume that
A20: x. 0 <> y and
A21: ( x. 3 <> y & x. 4 <> y ) ; :: thesis: contradiction
( (val +* (x. 3),a9) . y = val . y & (g +* (x. 4),c9) . y = g . y ) by A21, FUNCT_7:34;
hence contradiction by A6, A19, A20; :: thesis: verum
end;
for x being Variable st (g +* (x. 4),c9) . x <> g . x holds
x. 4 = x by FUNCT_7:34;
then A22: E,g +* (x. 4),c9 |= H <=> ((x. 4) '=' (x. 0 )) by A7, ZF_MODEL:16;
A23: (g +* (x. 4),c9) . (x. 3) = g . (x. 3) by FUNCT_7:34;
( [a,c] `1 = a9 & [a,c] `2 = c9 ) by MCART_1:7;
then E,g +* (x. 4),c9 |= H by A3, A5, A17, A23, A8, A18;
then A24: E,g +* (x. 4),c9 |= (x. 4) '=' (x. 0 ) by A22, ZF_MODEL:19;
( (g +* (x. 4),b9) . (x. 0 ) = g . (x. 0 ) & (g +* (x. 4),c9) . (x. 0 ) = g . (x. 0 ) ) by FUNCT_7:34;
hence b = c by A9, A17, A24, A16, ZF_MODEL:12; :: thesis: verum
end;
then reconsider F = X as Function ;
A25: rng F c= E
proof
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in rng F or b in E )
assume b in rng F ; :: thesis: b in E
then consider a being set such that
A26: ( a in dom F & b = F . a ) by FUNCT_1:def 5;
[a,b] in F by A26, FUNCT_1:8;
then [a,b] in [:E,E:] by A3;
hence b in E by ZFMISC_1:106; :: thesis: verum
end;
A27: E c= dom F
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in E or a in dom F )
assume a in E ; :: thesis: a in dom F
then reconsider a9 = a as Element of E ;
set g = val +* (x. 3),a9;
for x being Variable st (val +* (x. 3),a9) . x <> val . x holds
x = x. 3 by FUNCT_7:34;
then E,val +* (x. 3),a9 |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))) by A2, ZF_MODEL:16;
then consider h being Function of VAR ,E such that
A28: for x being Variable st h . x <> (val +* (x. 3),a9) . x holds
x = x. 0 and
A29: E,h |= All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))) by ZF_MODEL:20;
set u = h . (x. 0 );
A30: (val +* (x. 3),a9) . (x. 3) = a9 by FUNCT_7:130;
A31: now
set m = h +* (x. 4),(h . (x. 0 ));
let f be Function of VAR ,E; :: thesis: ( S2[f] & f . (x. 3) = [a9,(h . (x. 0 ))] `1 & f . (x. 4) = [a9,(h . (x. 0 ))] `2 implies E,f |= H )
assume that
A32: S2[f] and
A33: f . (x. 3) = [a9,(h . (x. 0 ))] `1 and
A34: f . (x. 4) = [a9,(h . (x. 0 ))] `2 ; :: thesis: E,f |= H
A35: (h +* (x. 4),(h . (x. 0 ))) . (x. 4) = h . (x. 0 ) by FUNCT_7:130;
A36: now
let x be Variable; :: thesis: ( f . x <> (h +* (x. 4),(h . (x. 0 ))) . x implies not x. 0 <> x )
assume A37: f . x <> (h +* (x. 4),(h . (x. 0 ))) . x ; :: thesis: not x. 0 <> x
A38: x <> x. 4 by A34, A35, A37, MCART_1:7;
then A39: (h +* (x. 4),(h . (x. 0 ))) . x = h . x by FUNCT_7:34;
( (val +* (x. 3),a9) . (x. 3) = h . (x. 3) & h . (x. 3) = (h +* (x. 4),(h . (x. 0 ))) . (x. 3) ) by A28, FUNCT_7:34;
then A40: x <> x. 3 by A30, A33, A37, MCART_1:7;
then A41: (val +* (x. 3),a9) . x = val . x by FUNCT_7:34;
assume A42: x. 0 <> x ; :: thesis: contradiction
then f . x = val . x by A32, A38, A40;
hence contradiction by A28, A37, A42, A41, A39; :: thesis: verum
end;
for x being Variable st (h +* (x. 4),(h . (x. 0 ))) . x <> h . x holds
x. 4 = x by FUNCT_7:34;
then A43: E,h +* (x. 4),(h . (x. 0 )) |= H <=> ((x. 4) '=' (x. 0 )) by A29, ZF_MODEL:16;
(h +* (x. 4),(h . (x. 0 ))) . (x. 0 ) = h . (x. 0 ) by FUNCT_7:34;
then E,h +* (x. 4),(h . (x. 0 )) |= (x. 4) '=' (x. 0 ) by A35, ZF_MODEL:12;
then E,h +* (x. 4),(h . (x. 0 )) |= H by A43, ZF_MODEL:19;
then E,h +* (x. 4),(h . (x. 0 )) |= All (x. 0 ),H by A1, Th10;
hence E,f |= H by A36, ZF_MODEL:16; :: thesis: verum
end;
[a9,(h . (x. 0 ))] in [:E,E:] by ZFMISC_1:106;
then [a9,(h . (x. 0 ))] in X by A3, A31;
hence a in dom F by FUNCT_1:8; :: thesis: verum
end;
dom F c= E
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in dom F or a in E )
assume a in dom F ; :: thesis: a in E
then consider b being set such that
A44: [a,b] in F by RELAT_1:def 4;
[a,b] in [:E,E:] by A3, A44;
hence a in E by ZFMISC_1:106; :: thesis: verum
end;
then E = dom F by A27, XBOOLE_0:def 10;
then reconsider F = F as Function of E,E by A25, FUNCT_2:def 1, RELSET_1:11;
take F ; :: thesis: for g being Function of VAR ,E st ( for y being Variable holds
( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds
( E,g |= H iff F . (g . (x. 3)) = g . (x. 4) )
let f be Function of VAR ,E; :: thesis: ( ( for y being Variable holds
( not f . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) implies ( E,f |= H iff F . (f . (x. 3)) = f . (x. 4) ) )
assume A45: for y being Variable holds
( not f . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ; :: thesis: ( E,f |= H iff F . (f . (x. 3)) = f . (x. 4) )
thus ( E,f |= H implies F . (f . (x. 3)) = f . (x. 4) ) :: thesis: ( F . (f . (x. 3)) = f . (x. 4) implies E,f |= H )
proof
assume E,f |= H ; :: thesis: F . (f . (x. 3)) = f . (x. 4)
then A46: E,f |= All (x. 0 ),H by A1, Th10;
A47: now
let g be Function of VAR ,E; :: thesis: ( S2[g] & g . (x. 3) = [(f . (x. 3)),(f . (x. 4))] `1 & g . (x. 4) = [(f . (x. 3)),(f . (x. 4))] `2 implies E,g |= H )
assume that
A48: S2[g] and
A49: ( g . (x. 3) = [(f . (x. 3)),(f . (x. 4))] `1 & g . (x. 4) = [(f . (x. 3)),(f . (x. 4))] `2 ) ; :: thesis: E,g |= H
now
let x be Variable; :: thesis: ( g . x <> f . x implies not x. 0 <> x )
assume that
A50: g . x <> f . x and
A51: x. 0 <> x ; :: thesis: contradiction
A52: ( x <> x. 3 & x <> x. 4 ) by A49, A50, MCART_1:7;
then f . x = val . x by A45, A51;
hence contradiction by A48, A50, A51, A52; :: thesis: verum
end;
hence E,g |= H by A46, ZF_MODEL:16; :: thesis: verum
end;
[(f . (x. 3)),(f . (x. 4))] in [:E,E:] by ZFMISC_1:106;
then [(f . (x. 3)),(f . (x. 4))] in X by A3, A47;
hence F . (f . (x. 3)) = f . (x. 4) by FUNCT_1:8; :: thesis: verum
end;
A53: ( [(f . (x. 3)),(f . (x. 4))] `1 = f . (x. 3) & [(f . (x. 3)),(f . (x. 4))] `2 = f . (x. 4) ) by MCART_1:7;
A54: dom F = E by FUNCT_2:def 1;
assume F . (f . (x. 3)) = f . (x. 4) ; :: thesis: E,f |= H
then [(f . (x. 3)),(f . (x. 4))] in F by A54, FUNCT_1:8;
hence E,f |= H by A3, A45, A53; :: thesis: verum