:: ZFMODEL1 semantic presentation

begin

                   set x0 = x. 0;

set x1 = x. 1;

set x2 = x. 2;

set x3 = x. 3;

set x4 = x. 4;

theorem :: ZFMODEL1:1
for E being non empty set st E is epsilon-transitive holds
E |= the_axiom_of_extensionality
proof
let E be non empty set ; ::_thesis: ( E is epsilon-transitive implies E |= the_axiom_of_extensionality )
assume A1: for X being set st X in E holds
X c= E ; :: according to ORDINAL1:def_2 ::_thesis: E |= the_axiom_of_extensionality
 E |= (All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1))
proof
let f be Function of VAR,E; :: according to ZF_MODEL:def_5 ::_thesis: E,f |= (All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1))
now__::_thesis:_(_E,f_|=_All_((x._2),(((x._2)_'in'_(x._0))_<=>_((x._2)_'in'_(x._1))))_implies_E,f_|=_(x._0)_'='_(x._1)_)
assume A2: E,f |= All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) ; ::_thesis: E,f |= (x. 0) '=' (x. 1)
 f . (x. 0) = f . (x. 1)
proof
thus  for a being set st a in f . (x. 0) holds
a in f . (x. 1) :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: f . (x. 1) c= f . (x. 0)
proof
let a be set ; ::_thesis: ( a in f . (x. 0) implies a in f . (x. 1) )
assume A3: a in f . (x. 0) ; ::_thesis: a in f . (x. 1)
 f . (x. 0) c= E by A1;
then reconsider a9 = a as Element of E by A3;
set g = f +* ((x. 2),a9);
A4: (f +* ((x. 2),a9)) . (x. 1) = f . (x. 1) by FUNCT_7:32;
 for x being Variable st (f +* ((x. 2),a9)) . x <> f . x holds
x. 2 = x by FUNCT_7:32;
then  E,f +* ((x. 2),a9) |= ((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)) by A2, ZF_MODEL:16;
then A5: ( E,f +* ((x. 2),a9) |= (x. 2) 'in' (x. 0) iff E,f +* ((x. 2),a9) |= (x. 2) 'in' (x. 1) ) by ZF_MODEL:19;
 ( (f +* ((x. 2),a9)) . (x. 2) = a9 & (f +* ((x. 2),a9)) . (x. 0) = f . (x. 0) ) by FUNCT_7:32, FUNCT_7:128;
hence  a in f . (x. 1) by A3, A5, A4, ZF_MODEL:13; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f . (x. 1) or a in f . (x. 0) )
assume A6: a in f . (x. 1) ; ::_thesis: a in f . (x. 0)
 f . (x. 1) c= E by A1;
then reconsider a9 = a as Element of E by A6;
set g = f +* ((x. 2),a9);
A7: (f +* ((x. 2),a9)) . (x. 1) = f . (x. 1) by FUNCT_7:32;
 for x being Variable st (f +* ((x. 2),a9)) . x <> f . x holds
x. 2 = x by FUNCT_7:32;
then  E,f +* ((x. 2),a9) |= ((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)) by A2, ZF_MODEL:16;
then A8: ( E,f +* ((x. 2),a9) |= (x. 2) 'in' (x. 0) iff E,f +* ((x. 2),a9) |= (x. 2) 'in' (x. 1) ) by ZF_MODEL:19;
 ( (f +* ((x. 2),a9)) . (x. 2) = a9 & (f +* ((x. 2),a9)) . (x. 0) = f . (x. 0) ) by FUNCT_7:32, FUNCT_7:128;
hence  a in f . (x. 0) by A6, A8, A7, ZF_MODEL:13; ::_thesis: verum
end;
hence  E,f |= (x. 0) '=' (x. 1) by ZF_MODEL:12; ::_thesis: verum
end;
hence  E,f |= (All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)) by ZF_MODEL:18; ::_thesis: verum
end;
then  E |= All ((x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))) by ZF_MODEL:23;
hence  E |= the_axiom_of_extensionality by ZF_MODEL:23; ::_thesis: verum
end;

theorem Th2: :: ZFMODEL1:2
for E being non empty set st E is epsilon-transitive holds
( E |= the_axiom_of_pairs iff for u, v being Element of E holds {u,v} in E )
proof
let E be non empty set ; ::_thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_pairs iff for u, v being Element of E holds {u,v} in E ) )
assume A1: for X being set st X in E holds
X c= E ; :: according to ORDINAL1:def_2 ::_thesis: ( E |= the_axiom_of_pairs iff for u, v being Element of E holds {u,v} in E )
A2: for a being set
for u being Element of E st a in u holds
a is Element of E
proof
let a be set ; ::_thesis: for u being Element of E st a in u holds
a is Element of E
let u be Element of E; ::_thesis: ( a in u implies a is Element of E )
assume A3: a in u ; ::_thesis: a is Element of E
 u c= E by A1;
hence  a is Element of E by A3; ::_thesis: verum
end;
A4: ( E |= All ((x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))) iff E |= Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))) ) by ZF_MODEL:23;
thus  ( E |= the_axiom_of_pairs implies for u, v being Element of E holds {u,v} in E ) ::_thesis: ( ( for u, v being Element of E holds {u,v} in E ) implies E |= the_axiom_of_pairs )
proof
set fv = the Function of VAR,E;
assume A5: E |= the_axiom_of_pairs ; ::_thesis: for u, v being Element of E holds {u,v} in E
let u, v be Element of E; ::_thesis: {u,v} in E
set g = the Function of VAR,E +* ((x. 0),u);
set f = ( the Function of VAR,E +* ((x. 0),u)) +* ((x. 1),v);
 E,( the Function of VAR,E +* ((x. 0),u)) +* ((x. 1),v) |= Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))) by A4, A5, ZF_MODEL:23, ZF_MODEL:def_5;
then consider h being Function of VAR,E such that
A6: for x being Variable st h . x <> (( the Function of VAR,E +* ((x. 0),u)) +* ((x. 1),v)) . x holds
x. 2 = x and
A7: E,h |= All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) by ZF_MODEL:20;
A8: (( the Function of VAR,E +* ((x. 0),u)) +* ((x. 1),v)) . (x. 1) = v by FUNCT_7:128;
A9: ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) = u by FUNCT_7:128;
then A10: (( the Function of VAR,E +* ((x. 0),u)) +* ((x. 1),v)) . (x. 0) = u by FUNCT_7:32;
 for a being set holds
( a in h . (x. 2) iff ( a = u or a = v ) )
proof
let a be set ; ::_thesis: ( a in h . (x. 2) iff ( a = u or a = v ) )
thus  ( not a in h . (x. 2) or a = u or a = v ) ::_thesis: ( ( a = u or a = v ) implies a in h . (x. 2) )
proof
assume A11: a in h . (x. 2) ; ::_thesis: ( a = u or a = v )
then reconsider a9 = a as Element of E by A2;
set f3 = h +* ((x. 3),a9);
A12: (h +* ((x. 3),a9)) . (x. 3) = a9 by FUNCT_7:128;
 for x being Variable st (h +* ((x. 3),a9)) . x <> h . x holds
x. 3 = x by FUNCT_7:32;
then  E,h +* ((x. 3),a9) |= ((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) by A7, ZF_MODEL:16;
then A13: ( E,h +* ((x. 3),a9) |= (x. 3) 'in' (x. 2) iff E,h +* ((x. 3),a9) |= ((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)) ) by ZF_MODEL:19;
 (h +* ((x. 3),a9)) . (x. 2) = h . (x. 2) by FUNCT_7:32;
then  ( E,h +* ((x. 3),a9) |= (x. 3) '=' (x. 0) or E,h +* ((x. 3),a9) |= (x. 3) '=' (x. 1) ) by A11, A12, A13, ZF_MODEL:13, ZF_MODEL:17;
then A14: ( (h +* ((x. 3),a9)) . (x. 3) = (h +* ((x. 3),a9)) . (x. 0) or (h +* ((x. 3),a9)) . (x. 3) = (h +* ((x. 3),a9)) . (x. 1) ) by ZF_MODEL:12;
A15: (h +* ((x. 3),a9)) . (x. 1) = h . (x. 1) by FUNCT_7:32;
 ( (h +* ((x. 3),a9)) . (x. 0) = h . (x. 0) & h . (x. 0) = (( the Function of VAR,E +* ((x. 0),u)) +* ((x. 1),v)) . (x. 0) ) by A6, FUNCT_7:32;
hence  ( a = u or a = v ) by A9, A8, A6, A12, A14, A15, FUNCT_7:32; ::_thesis: verum
end;
assume A16: ( a = u or a = v ) ; ::_thesis: a in h . (x. 2)
then reconsider a9 = a as Element of E ;
set f3 = h +* ((x. 3),a9);
A17: (h +* ((x. 3),a9)) . (x. 3) = a9 by FUNCT_7:128;
 for x being Variable st (h +* ((x. 3),a9)) . x <> h . x holds
x. 3 = x by FUNCT_7:32;
then  E,h +* ((x. 3),a9) |= ((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) by A7, ZF_MODEL:16;
then A18: ( E,h +* ((x. 3),a9) |= (x. 3) 'in' (x. 2) iff E,h +* ((x. 3),a9) |= ((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)) ) by ZF_MODEL:19;
A19: ( (h +* ((x. 3),a9)) . (x. 1) = h . (x. 1) & h . (x. 1) = (( the Function of VAR,E +* ((x. 0),u)) +* ((x. 1),v)) . (x. 1) ) by A6, FUNCT_7:32;
 ( (h +* ((x. 3),a9)) . (x. 0) = h . (x. 0) & h . (x. 0) = (( the Function of VAR,E +* ((x. 0),u)) +* ((x. 1),v)) . (x. 0) ) by A6, FUNCT_7:32;
then  ( E,h +* ((x. 3),a9) |= (x. 3) '=' (x. 0) or E,h +* ((x. 3),a9) |= (x. 3) '=' (x. 1) ) by A8, A10, A16, A17, A19, ZF_MODEL:12;
then  (h +* ((x. 3),a9)) . (x. 3) in (h +* ((x. 3),a9)) . (x. 2) by A18, ZF_MODEL:13, ZF_MODEL:17;
hence  a in h . (x. 2) by A17, FUNCT_7:32; ::_thesis: verum
end;
then  h . (x. 2) = {u,v} by TARSKI:def_2;
hence  {u,v} in E ; ::_thesis: verum
end;
assume A20: for u, v being Element of E holds {u,v} in E ; ::_thesis: E |= the_axiom_of_pairs
let f be Function of VAR,E; :: according to ZF_MODEL:def_5 ::_thesis: E,f |= the_axiom_of_pairs
now__::_thesis:_for_g_being_Function_of_VAR,E_st_(_for_x_being_Variable_holds_
(_not_g_._x_<>_f_._x_or_x._0_=_x_or_x._1_=_x_)_)_holds_
E,g_|=_Ex_((x._2),(All_((x._3),(((x._3)_'in'_(x._2))_<=>_(((x._3)_'='_(x._0))_'or'_((x._3)_'='_(x._1)))))))
let g be Function of VAR,E; ::_thesis: ( ( for x being Variable holds
( not g . x <> f . x or x. 0 = x or x. 1 = x ) ) implies E,g |= Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))) )
assume  for x being Variable holds
( not g . x <> f . x or x. 0 = x or x. 1 = x ) ; ::_thesis: E,g |= Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))))
reconsider w = {(g . (x. 0)),(g . (x. 1))} as Element of E by A20;
set h = g +* ((x. 2),w);
A21: (g +* ((x. 2),w)) . (x. 2) = w by FUNCT_7:128;
now__::_thesis:_for_m_being_Function_of_VAR,E_st_(_for_x_being_Variable_st_m_._x_<>_(g_+*_((x._2),w))_._x_holds_
x._3_=_x_)_holds_
E,m_|=_((x._3)_'in'_(x._2))_<=>_(((x._3)_'='_(x._0))_'or'_((x._3)_'='_(x._1)))
let m be Function of VAR,E; ::_thesis: ( ( for x being Variable st m . x <> (g +* ((x. 2),w)) . x holds
x. 3 = x ) implies E,m |= ((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) )
A22: ( (g +* ((x. 2),w)) . (x. 0) = g . (x. 0) & (g +* ((x. 2),w)) . (x. 1) = g . (x. 1) ) by FUNCT_7:32;
A23: ( E,m |= (x. 3) 'in' (x. 2) iff m . (x. 3) in m . (x. 2) ) by ZF_MODEL:13;
A24: ( E,m |= ((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)) iff ( E,m |= (x. 3) '=' (x. 0) or E,m |= (x. 3) '=' (x. 1) ) ) by ZF_MODEL:17;
A25: ( E,m |= (x. 3) '=' (x. 1) iff m . (x. 3) = m . (x. 1) ) by ZF_MODEL:12;
A26: ( E,m |= (x. 3) '=' (x. 0) iff m . (x. 3) = m . (x. 0) ) by ZF_MODEL:12;
assume A27: for x being Variable st m . x <> (g +* ((x. 2),w)) . x holds
x. 3 = x ; ::_thesis: E,m |= ((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))
then A28: m . (x. 2) = (g +* ((x. 2),w)) . (x. 2) ;
 ( m . (x. 0) = (g +* ((x. 2),w)) . (x. 0) & m . (x. 1) = (g +* ((x. 2),w)) . (x. 1) ) by A27;
hence  E,m |= ((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) by A21, A22, A28, A23, A26, A25, A24, TARSKI:def_2, ZF_MODEL:19; ::_thesis: verum
end;
then A29: E,g +* ((x. 2),w) |= All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) by ZF_MODEL:16;
 for x being Variable st (g +* ((x. 2),w)) . x <> g . x holds
x. 2 = x by FUNCT_7:32;
hence  E,g |= Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))) by A29, ZF_MODEL:20; ::_thesis: verum
end;
hence  E,f |= the_axiom_of_pairs by ZF_MODEL:21; ::_thesis: verum
end;

theorem :: ZFMODEL1:3
for E being non empty set st E is epsilon-transitive holds
( E |= the_axiom_of_pairs iff for X, Y being set st X in E & Y in E holds
{X,Y} in E )
proof
let E be non empty set ; ::_thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_pairs iff for X, Y being set st X in E & Y in E holds
{X,Y} in E ) )
assume A1: E is epsilon-transitive ; ::_thesis: ( E |= the_axiom_of_pairs iff for X, Y being set st X in E & Y in E holds
{X,Y} in E )
hence  ( E |= the_axiom_of_pairs implies for X, Y being set st X in E & Y in E holds
{X,Y} in E ) by Th2; ::_thesis: ( ( for X, Y being set st X in E & Y in E holds
{X,Y} in E ) implies E |= the_axiom_of_pairs )
assume  for X, Y being set st X in E & Y in E holds
{X,Y} in E ; ::_thesis: E |= the_axiom_of_pairs
then  for u, v being Element of E holds {u,v} in E ;
hence  E |= the_axiom_of_pairs by A1, Th2; ::_thesis: verum
end;

theorem Th4: :: ZFMODEL1:4
for E being non empty set st E is epsilon-transitive holds
( E |= the_axiom_of_unions iff for u being Element of E holds union u in E )
proof
let E be non empty set ; ::_thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_unions iff for u being Element of E holds union u in E ) )
assume A1: for X being set st X in E holds
X c= E ; :: according to ORDINAL1:def_2 ::_thesis: ( E |= the_axiom_of_unions iff for u being Element of E holds union u in E )
thus  ( E |= the_axiom_of_unions implies for u being Element of E holds union u in E ) ::_thesis: ( ( for u being Element of E holds union u in E ) implies E |= the_axiom_of_unions )
proof
set f0 = the Function of VAR,E;
assume A2: E |= the_axiom_of_unions ; ::_thesis: for u being Element of E holds union u in E
let u be Element of E; ::_thesis: union u in E
set f = the Function of VAR,E +* ((x. 0),u);
 E |= Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))) by A2, ZF_MODEL:23;
then  E, the Function of VAR,E +* ((x. 0),u) |= Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))) by ZF_MODEL:def_5;
then consider g being Function of VAR,E such that
A3: for x being Variable st g . x <> ( the Function of VAR,E +* ((x. 0),u)) . x holds
x. 1 = x and
A4: E,g |= All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) by ZF_MODEL:20;
A5: ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) = u by FUNCT_7:128;
 for a being set holds
( a in g . (x. 1) iff ex X being set st
( a in X & X in u ) )
proof
let a be set ; ::_thesis: ( a in g . (x. 1) iff ex X being set st
( a in X & X in u ) )
A6: g . (x. 0) = ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) by A3;
thus  ( a in g . (x. 1) implies ex X being set st
( a in X & X in u ) ) ::_thesis: ( ex X being set st
( a in X & X in u ) implies a in g . (x. 1) )
proof
assume A7: a in g . (x. 1) ; ::_thesis: ex X being set st
( a in X & X in u )
 g . (x. 1) c= E by A1;
then reconsider a9 = a as Element of E by A7;
set h = g +* ((x. 2),a9);
A8: (g +* ((x. 2),a9)) . (x. 2) = a9 by FUNCT_7:128;
 for x being Variable st (g +* ((x. 2),a9)) . x <> g . x holds
x. 2 = x by FUNCT_7:32;
then A9: E,g +* ((x. 2),a9) |= ((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) by A4, ZF_MODEL:16;
 (g +* ((x. 2),a9)) . (x. 1) = g . (x. 1) by FUNCT_7:32;
then  E,g +* ((x. 2),a9) |= (x. 2) 'in' (x. 1) by A7, A8, ZF_MODEL:13;
then  E,g +* ((x. 2),a9) |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) by A9, ZF_MODEL:19;
then consider m being Function of VAR,E such that
A10: for x being Variable st m . x <> (g +* ((x. 2),a9)) . x holds
x. 3 = x and
A11: E,m |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) by ZF_MODEL:20;
A12: ( m . (x. 0) = (g +* ((x. 2),a9)) . (x. 0) & m . (x. 2) = (g +* ((x. 2),a9)) . (x. 2) ) by A10;
reconsider X = m . (x. 3) as set ;
take  X ; ::_thesis: ( a in X & X in u )
A13: ( (g +* ((x. 2),a9)) . (x. 0) = g . (x. 0) & g . (x. 0) = ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) ) by A3, FUNCT_7:32;
 ( E,m |= (x. 2) 'in' (x. 3) & E,m |= (x. 3) 'in' (x. 0) ) by A11, ZF_MODEL:15;
hence  ( a in X & X in u ) by A5, A8, A13, A12, ZF_MODEL:13; ::_thesis: verum
end;
given X being set  such that A14: a in X and
A15: X in u ; ::_thesis: a in g . (x. 1)
 u c= E by A1;
then reconsider X = X as Element of E by A15;
 X c= E by A1;
then reconsider a9 = a as Element of E by A14;
set h = g +* ((x. 2),a9);
set m = (g +* ((x. 2),a9)) +* ((x. 3),X);
A16: ((g +* ((x. 2),a9)) +* ((x. 3),X)) . (x. 3) = X by FUNCT_7:128;
 ( ((g +* ((x. 2),a9)) +* ((x. 3),X)) . (x. 0) = (g +* ((x. 2),a9)) . (x. 0) & (g +* ((x. 2),a9)) . (x. 0) = g . (x. 0) ) by FUNCT_7:32;
then A17: E,(g +* ((x. 2),a9)) +* ((x. 3),X) |= (x. 3) 'in' (x. 0) by A5, A15, A16, A6, ZF_MODEL:13;
A18: (g +* ((x. 2),a9)) . (x. 2) = a9 by FUNCT_7:128;
 for x being Variable st (g +* ((x. 2),a9)) . x <> g . x holds
x. 2 = x by FUNCT_7:32;
then A19: E,g +* ((x. 2),a9) |= ((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) by A4, ZF_MODEL:16;
 ((g +* ((x. 2),a9)) +* ((x. 3),X)) . (x. 2) = (g +* ((x. 2),a9)) . (x. 2) by FUNCT_7:32;
then  E,(g +* ((x. 2),a9)) +* ((x. 3),X) |= (x. 2) 'in' (x. 3) by A14, A18, A16, ZF_MODEL:13;
then  ( ( for x being Variable st ((g +* ((x. 2),a9)) +* ((x. 3),X)) . x <> (g +* ((x. 2),a9)) . x holds
x. 3 = x ) & E,(g +* ((x. 2),a9)) +* ((x. 3),X) |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) ) by A17, FUNCT_7:32, ZF_MODEL:15;
then  E,g +* ((x. 2),a9) |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) by ZF_MODEL:20;
then  E,g +* ((x. 2),a9) |= (x. 2) 'in' (x. 1) by A19, ZF_MODEL:19;
then  (g +* ((x. 2),a9)) . (x. 2) in (g +* ((x. 2),a9)) . (x. 1) by ZF_MODEL:13;
hence  a in g . (x. 1) by A18, FUNCT_7:32; ::_thesis: verum
end;
then  g . (x. 1) = union u by TARSKI:def_4;
hence  union u in E ; ::_thesis: verum
end;
assume A20: for u being Element of E holds union u in E ; ::_thesis: E |= the_axiom_of_unions
now__::_thesis:_for_f_being_Function_of_VAR,E_holds_E,f_|=_Ex_((x._1),(All_((x._2),(((x._2)_'in'_(x._1))_<=>_(Ex_((x._3),(((x._2)_'in'_(x._3))_'&'_((x._3)_'in'_(x._0)))))))))
let f be Function of VAR,E; ::_thesis: E,f |= Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))))
reconsider v = union (f . (x. 0)) as Element of E by A20;
set g = f +* ((x. 1),v);
A21: (f +* ((x. 1),v)) . (x. 1) = v by FUNCT_7:128;
now__::_thesis:_for_h_being_Function_of_VAR,E_st_(_for_x_being_Variable_st_h_._x_<>_(f_+*_((x._1),v))_._x_holds_
x._2_=_x_)_holds_
E,h_|=_((x._2)_'in'_(x._1))_<=>_(Ex_((x._3),(((x._2)_'in'_(x._3))_'&'_((x._3)_'in'_(x._0)))))
let h be Function of VAR,E; ::_thesis: ( ( for x being Variable st h . x <> (f +* ((x. 1),v)) . x holds
x. 2 = x ) implies E,h |= ((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) )
assume A22: for x being Variable st h . x <> (f +* ((x. 1),v)) . x holds
x. 2 = x ; ::_thesis: E,h |= ((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))
then A23: h . (x. 1) = (f +* ((x. 1),v)) . (x. 1) ;
 ( E,h |= (x. 2) 'in' (x. 1) iff E,h |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) )
proof
thus  ( E,h |= (x. 2) 'in' (x. 1) implies E,h |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) ) ::_thesis: ( E,h |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) implies E,h |= (x. 2) 'in' (x. 1) )
proof
assume  E,h |= (x. 2) 'in' (x. 1) ; ::_thesis: E,h |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))
then  h . (x. 2) in h . (x. 1) by ZF_MODEL:13;
then consider X being set  such that
A24: h . (x. 2) in X and
A25: X in f . (x. 0) by A21, A23, TARSKI:def_4;
 f . (x. 0) c= E by A1;
then reconsider X = X as Element of E by A25;
set m = h +* ((x. 3),X);
A26: (h +* ((x. 3),X)) . (x. 3) = X by FUNCT_7:128;
A27: (f +* ((x. 1),v)) . (x. 0) = f . (x. 0) by FUNCT_7:32;
 (h +* ((x. 3),X)) . (x. 2) = h . (x. 2) by FUNCT_7:32;
then A28: E,h +* ((x. 3),X) |= (x. 2) 'in' (x. 3) by A24, A26, ZF_MODEL:13;
 ( (h +* ((x. 3),X)) . (x. 0) = h . (x. 0) & h . (x. 0) = (f +* ((x. 1),v)) . (x. 0) ) by A22, FUNCT_7:32;
then  E,h +* ((x. 3),X) |= (x. 3) 'in' (x. 0) by A25, A26, A27, ZF_MODEL:13;
then  ( ( for x being Variable st (h +* ((x. 3),X)) . x <> h . x holds
x. 3 = x ) & E,h +* ((x. 3),X) |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) ) by A28, FUNCT_7:32, ZF_MODEL:15;
hence  E,h |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) by ZF_MODEL:20; ::_thesis: verum
end;
assume  E,h |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) ; ::_thesis: E,h |= (x. 2) 'in' (x. 1)
then consider m being Function of VAR,E such that
A29: for x being Variable st m . x <> h . x holds
x. 3 = x and
A30: E,m |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) by ZF_MODEL:20;
 E,m |= (x. 3) 'in' (x. 0) by A30, ZF_MODEL:15;
then A31: m . (x. 3) in m . (x. 0) by ZF_MODEL:13;
 E,m |= (x. 2) 'in' (x. 3) by A30, ZF_MODEL:15;
then  m . (x. 2) in m . (x. 3) by ZF_MODEL:13;
then A32: m . (x. 2) in union (m . (x. 0)) by A31, TARSKI:def_4;
A33: h . (x. 1) = (f +* ((x. 1),v)) . (x. 1) by A22;
A34: ( h . (x. 0) = (f +* ((x. 1),v)) . (x. 0) & (f +* ((x. 1),v)) . (x. 0) = f . (x. 0) ) by A22, FUNCT_7:32;
 ( m . (x. 2) = h . (x. 2) & m . (x. 0) = h . (x. 0) ) by A29;
hence  E,h |= (x. 2) 'in' (x. 1) by A21, A32, A34, A33, ZF_MODEL:13; ::_thesis: verum
end;
hence  E,h |= ((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) by ZF_MODEL:19; ::_thesis: verum
end;
then  ( ( for x being Variable st (f +* ((x. 1),v)) . x <> f . x holds
x. 1 = x ) & E,f +* ((x. 1),v) |= All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) ) by FUNCT_7:32, ZF_MODEL:16;
hence  E,f |= Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))) by ZF_MODEL:20; ::_thesis: verum
end;
then  E |= Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))) by ZF_MODEL:def_5;
hence  E |= the_axiom_of_unions by ZF_MODEL:23; ::_thesis: verum
end;

theorem :: ZFMODEL1:5
for E being non empty set st E is epsilon-transitive holds
( E |= the_axiom_of_unions iff for X being set st X in E holds
union X in E )
proof
let E be non empty set ; ::_thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_unions iff for X being set st X in E holds
union X in E ) )
assume A1: E is epsilon-transitive ; ::_thesis: ( E |= the_axiom_of_unions iff for X being set st X in E holds
union X in E )
hence  ( E |= the_axiom_of_unions implies for X being set st X in E holds
union X in E ) by Th4; ::_thesis: ( ( for X being set st X in E holds
union X in E ) implies E |= the_axiom_of_unions )
assume  for X being set st X in E holds
union X in E ; ::_thesis: E |= the_axiom_of_unions
then  for u being Element of E holds union u in E ;
hence  E |= the_axiom_of_unions by A1, Th4; ::_thesis: verum
end;

theorem Th6: :: ZFMODEL1:6
for E being non empty set st E is epsilon-transitive holds
( E |= the_axiom_of_infinity iff ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) )
proof
let E be non empty set ; ::_thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_infinity iff ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) ) )
assume A1: for X being set st X in E holds
X c= E ; :: according to ORDINAL1:def_2 ::_thesis: ( E |= the_axiom_of_infinity iff ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) )
thus  ( E |= the_axiom_of_infinity implies ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) ) ::_thesis: ( ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) implies E |= the_axiom_of_infinity )
proof
set f = the Function of VAR,E;
assume  for g being Function of VAR,E holds E,g |= the_axiom_of_infinity ; :: according to ZF_MODEL:def_5 ::_thesis: ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) )
then  E, the Function of VAR,E |= the_axiom_of_infinity ;
then consider g being Function of VAR,E such that
 for x being Variable holds
( not g . x <> the Function of VAR,E . x or x. 0 = x or x. 1 = x ) and
A2: E,g |= ((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))) by ZF_MODEL:22;
take u = g . (x. 0); ::_thesis: ( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) )
 E,g |= (x. 1) 'in' (x. 0) by A2, ZF_MODEL:15;
hence  u <> {} by ZF_MODEL:13; ::_thesis: for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u )
let v be Element of E; ::_thesis: ( v in u implies ex w being Element of E st
( v c< w & w in u ) )
assume A3: v in u ; ::_thesis: ex w being Element of E st
( v c< w & w in u )
set h = g +* ((x. 2),v);
 ( ( for x being Variable st (g +* ((x. 2),v)) . x <> g . x holds
x. 2 = x ) & E,g |= All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) ) by A2, FUNCT_7:32, ZF_MODEL:15;
then A4: E,g +* ((x. 2),v) |= ((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) by ZF_MODEL:16;
A5: (g +* ((x. 2),v)) . (x. 2) = v by FUNCT_7:128;
 (g +* ((x. 2),v)) . (x. 0) = g . (x. 0) by FUNCT_7:32;
then  E,g +* ((x. 2),v) |= (x. 2) 'in' (x. 0) by A3, A5, ZF_MODEL:13;
then  E,g +* ((x. 2),v) |= Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))) by A4, ZF_MODEL:18;
then consider f being Function of VAR,E such that
A6: for x being Variable st f . x <> (g +* ((x. 2),v)) . x holds
x. 3 = x and
A7: E,f |= (((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))) by ZF_MODEL:20;
A8: f . (x. 0) = (g +* ((x. 2),v)) . (x. 0) by A6;
take w = f . (x. 3); ::_thesis: ( v c< w & w in u )
A9: E,f |= All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))) by A7, ZF_MODEL:15;
thus  v c= w :: according to XBOOLE_0:def_8 ::_thesis: ( not v = w & w in u )
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in v or a in w )
assume A10: a in v ; ::_thesis: a in w
 v c= E by A1;
then reconsider a9 = a as Element of E by A10;
set m = f +* ((x. 4),a9);
A11: (f +* ((x. 4),a9)) . (x. 4) = a9 by FUNCT_7:128;
 for x being Variable st (f +* ((x. 4),a9)) . x <> f . x holds
x. 4 = x by FUNCT_7:32;
then A12: E,f +* ((x. 4),a9) |= ((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)) by A9, ZF_MODEL:16;
 ( (f +* ((x. 4),a9)) . (x. 2) = f . (x. 2) & f . (x. 2) = (g +* ((x. 2),v)) . (x. 2) ) by A6, FUNCT_7:32;
then  E,f +* ((x. 4),a9) |= (x. 4) 'in' (x. 2) by A5, A10, A11, ZF_MODEL:13;
then  E,f +* ((x. 4),a9) |= (x. 4) 'in' (x. 3) by A12, ZF_MODEL:18;
then  (f +* ((x. 4),a9)) . (x. 4) in (f +* ((x. 4),a9)) . (x. 3) by ZF_MODEL:13;
hence  a in w by A11, FUNCT_7:32; ::_thesis: verum
end;
A13: E,f |= ((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2))) by A7, ZF_MODEL:15;
then  E,f |= 'not' ((x. 3) '=' (x. 2)) by ZF_MODEL:15;
then  not E,f |= (x. 3) '=' (x. 2) by ZF_MODEL:14;
then  f . (x. 3) <> f . (x. 2) by ZF_MODEL:12;
hence  v <> w by A5, A6; ::_thesis: w in u
A14: (g +* ((x. 2),v)) . (x. 0) = g . (x. 0) by FUNCT_7:32;
 E,f |= (x. 3) 'in' (x. 0) by A13, ZF_MODEL:15;
hence  w in u by A8, A14, ZF_MODEL:13; ::_thesis: verum
end;
given u being Element of E such that A15: u <> {} and
A16: for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ; ::_thesis: E |= the_axiom_of_infinity
set a = the Element of u;
 u c= E by A1;
then reconsider a = the Element of u as Element of E by A15, TARSKI:def_3;
let f0 be Function of VAR,E; :: according to ZF_MODEL:def_5 ::_thesis: E,f0 |= the_axiom_of_infinity
set f1 = f0 +* ((x. 0),u);
set f2 = (f0 +* ((x. 0),u)) +* ((x. 1),a);
A17: (f0 +* ((x. 0),u)) . (x. 0) = u by FUNCT_7:128;
now__::_thesis:_for_f_being_Function_of_VAR,E_st_(_for_x_being_Variable_st_f_._x_<>_((f0_+*_((x._0),u))_+*_((x._1),a))_._x_holds_
x._2_=_x_)_holds_
E,f_|=_((x._2)_'in'_(x._0))_=>_(Ex_((x._3),((((x._3)_'in'_(x._0))_'&'_('not'_((x._3)_'='_(x._2))))_'&'_(All_((x._4),(((x._4)_'in'_(x._2))_=>_((x._4)_'in'_(x._3))))))))
let f be Function of VAR,E; ::_thesis: ( ( for x being Variable st f . x <> ((f0 +* ((x. 0),u)) +* ((x. 1),a)) . x holds
x. 2 = x ) implies E,f |= ((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) )
assume A18: for x being Variable st f . x <> ((f0 +* ((x. 0),u)) +* ((x. 1),a)) . x holds
x. 2 = x ; ::_thesis: E,f |= ((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))
now__::_thesis:_(_E,f_|=_(x._2)_'in'_(x._0)_implies_E,f_|=_Ex_((x._3),((((x._3)_'in'_(x._0))_'&'_('not'_((x._3)_'='_(x._2))))_'&'_(All_((x._4),(((x._4)_'in'_(x._2))_=>_((x._4)_'in'_(x._3)))))))_)
assume  E,f |= (x. 2) 'in' (x. 0) ; ::_thesis: E,f |= Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))
then A19: f . (x. 2) in f . (x. 0) by ZF_MODEL:13;
 ( f . (x. 0) = ((f0 +* ((x. 0),u)) +* ((x. 1),a)) . (x. 0) & ((f0 +* ((x. 0),u)) +* ((x. 1),a)) . (x. 0) = (f0 +* ((x. 0),u)) . (x. 0) ) by A18, FUNCT_7:32;
then consider w being Element of E such that
A20: f . (x. 2) c< w and
A21: w in u by A16, A17, A19;
set g = f +* ((x. 3),w);
A22: (f +* ((x. 3),w)) . (x. 3) = w by FUNCT_7:128;
A23: f . (x. 2) c= w by A20, XBOOLE_0:def_8;
now__::_thesis:_for_h_being_Function_of_VAR,E_st_(_for_x_being_Variable_st_h_._x_<>_(f_+*_((x._3),w))_._x_holds_
x._4_=_x_)_holds_
E,h_|=_((x._4)_'in'_(x._2))_=>_((x._4)_'in'_(x._3))
let h be Function of VAR,E; ::_thesis: ( ( for x being Variable st h . x <> (f +* ((x. 3),w)) . x holds
x. 4 = x ) implies E,h |= ((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)) )
assume A24: for x being Variable st h . x <> (f +* ((x. 3),w)) . x holds
x. 4 = x ; ::_thesis: E,h |= ((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))
now__::_thesis:_(_E,h_|=_(x._4)_'in'_(x._2)_implies_E,h_|=_(x._4)_'in'_(x._3)_)
assume  E,h |= (x. 4) 'in' (x. 2) ; ::_thesis: E,h |= (x. 4) 'in' (x. 3)
then A25: h . (x. 4) in h . (x. 2) by ZF_MODEL:13;
A26: h . (x. 3) = (f +* ((x. 3),w)) . (x. 3) by A24;
 ( h . (x. 2) = (f +* ((x. 3),w)) . (x. 2) & (f +* ((x. 3),w)) . (x. 2) = f . (x. 2) ) by A24, FUNCT_7:32;
hence  E,h |= (x. 4) 'in' (x. 3) by A23, A22, A25, A26, ZF_MODEL:13; ::_thesis: verum
end;
hence  E,h |= ((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)) by ZF_MODEL:18; ::_thesis: verum
end;
then A27: E,f +* ((x. 3),w) |= All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))) by ZF_MODEL:16;
A28: ((f0 +* ((x. 0),u)) +* ((x. 1),a)) . (x. 0) = (f0 +* ((x. 0),u)) . (x. 0) by FUNCT_7:32;
 (f +* ((x. 3),w)) . (x. 2) = f . (x. 2) by FUNCT_7:32;
then  not E,f +* ((x. 3),w) |= (x. 3) '=' (x. 2) by A20, A22, ZF_MODEL:12;
then A29: E,f +* ((x. 3),w) |= 'not' ((x. 3) '=' (x. 2)) by ZF_MODEL:14;
 ( (f +* ((x. 3),w)) . (x. 0) = f . (x. 0) & f . (x. 0) = ((f0 +* ((x. 0),u)) +* ((x. 1),a)) . (x. 0) ) by A18, FUNCT_7:32;
then  E,f +* ((x. 3),w) |= (x. 3) 'in' (x. 0) by A17, A21, A22, A28, ZF_MODEL:13;
then  E,f +* ((x. 3),w) |= ((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2))) by A29, ZF_MODEL:15;
then  ( ( for x being Variable st (f +* ((x. 3),w)) . x <> f . x holds
x. 3 = x ) & E,f +* ((x. 3),w) |= (((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))) ) by A27, FUNCT_7:32, ZF_MODEL:15;
hence  E,f |= Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))) by ZF_MODEL:20; ::_thesis: verum
end;
hence  E,f |= ((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) by ZF_MODEL:18; ::_thesis: verum
end;
then A30: E,(f0 +* ((x. 0),u)) +* ((x. 1),a) |= All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) by ZF_MODEL:16;
 ( ((f0 +* ((x. 0),u)) +* ((x. 1),a)) . (x. 1) = a & ((f0 +* ((x. 0),u)) +* ((x. 1),a)) . (x. 0) = (f0 +* ((x. 0),u)) . (x. 0) ) by FUNCT_7:32, FUNCT_7:128;
then  E,(f0 +* ((x. 0),u)) +* ((x. 1),a) |= (x. 1) 'in' (x. 0) by A15, A17, ZF_MODEL:13;
then  ( ( for x being Variable st ((f0 +* ((x. 0),u)) +* ((x. 1),a)) . x <> (f0 +* ((x. 0),u)) . x holds
x. 1 = x ) & E,(f0 +* ((x. 0),u)) +* ((x. 1),a) |= ((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))) ) by A30, FUNCT_7:32, ZF_MODEL:15;
then  ( ( for x being Variable st (f0 +* ((x. 0),u)) . x <> f0 . x holds
x. 0 = x ) & E,f0 +* ((x. 0),u) |= Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))) ) by FUNCT_7:32, ZF_MODEL:20;
hence  E,f0 |= the_axiom_of_infinity by ZF_MODEL:20; ::_thesis: verum
end;

theorem :: ZFMODEL1:7
for E being non empty set st E is epsilon-transitive holds
( E |= the_axiom_of_infinity iff ex X being set st
( X in E & X <> {} & ( for Y being set st Y in X holds
ex Z being set st
( Y c< Z & Z in X ) ) ) )
proof
let E be non empty set ; ::_thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_infinity iff ex X being set st
( X in E & X <> {} & ( for Y being set st Y in X holds
ex Z being set st
( Y c< Z & Z in X ) ) ) ) )
assume A1: E is epsilon-transitive ; ::_thesis: ( E |= the_axiom_of_infinity iff ex X being set st
( X in E & X <> {} & ( for Y being set st Y in X holds
ex Z being set st
( Y c< Z & Z in X ) ) ) )
thus  ( E |= the_axiom_of_infinity implies ex X being set st
( X in E & X <> {} & ( for Y being set st Y in X holds
ex Z being set st
( Y c< Z & Z in X ) ) ) ) ::_thesis: ( ex X being set st
( X in E & X <> {} & ( for Y being set st Y in X holds
ex Z being set st
( Y c< Z & Z in X ) ) ) implies E |= the_axiom_of_infinity )
proof
assume  E |= the_axiom_of_infinity ; ::_thesis: ex X being set st
( X in E & X <> {} & ( for Y being set st Y in X holds
ex Z being set st
( Y c< Z & Z in X ) ) )
then consider u being Element of E such that
A2: u <> {} and
A3: for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) by A1, Th6;
reconsider X = u as set ;
take  X ; ::_thesis: ( X in E & X <> {} & ( for Y being set st Y in X holds
ex Z being set st
( Y c< Z & Z in X ) ) )
thus  ( X in E & X <> {} ) by A2; ::_thesis: for Y being set st Y in X holds
ex Z being set st
( Y c< Z & Z in X )
let Y be set ; ::_thesis: ( Y in X implies ex Z being set st
( Y c< Z & Z in X ) )
assume A4: Y in X ; ::_thesis: ex Z being set st
( Y c< Z & Z in X )
 X c= E by A1, ORDINAL1:def_2;
then reconsider v = Y as Element of E by A4;
consider w being Element of E such that
A5: ( v c< w & w in u ) by A3, A4;
reconsider w = w as set ;
take  w ; ::_thesis: ( Y c< w & w in X )
thus  ( Y c< w & w in X ) by A5; ::_thesis: verum
end;
given X being set  such that A6: X in E and
A7: X <> {} and
A8: for Y being set st Y in X holds
ex Z being set st
( Y c< Z & Z in X ) ; ::_thesis: E |= the_axiom_of_infinity
 ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) )
proof
reconsider u = X as Element of E by A6;
take  u ; ::_thesis: ( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) )
thus  u <> {} by A7; ::_thesis: for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u )
let v be Element of E; ::_thesis: ( v in u implies ex w being Element of E st
( v c< w & w in u ) )
assume  v in u ; ::_thesis: ex w being Element of E st
( v c< w & w in u )
then consider Z being set  such that
A9: v c< Z and
A10: Z in X by A8;
 X c= E by A1, A6, ORDINAL1:def_2;
then reconsider w = Z as Element of E by A10;
take  w ; ::_thesis: ( v c< w & w in u )
thus  ( v c< w & w in u ) by A9, A10; ::_thesis: verum
end;
hence  E |= the_axiom_of_infinity by A1, Th6; ::_thesis: verum
end;

theorem Th8: :: ZFMODEL1:8
for E being non empty set st E is epsilon-transitive holds
( E |= the_axiom_of_power_sets iff for u being Element of E holds E /\ (bool u) in E )
proof
let E be non empty set ; ::_thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_power_sets iff for u being Element of E holds E /\ (bool u) in E ) )
assume A1: for X being set st X in E holds
X c= E ; :: according to ORDINAL1:def_2 ::_thesis: ( E |= the_axiom_of_power_sets iff for u being Element of E holds E /\ (bool u) in E )
thus  ( E |= the_axiom_of_power_sets implies for u being Element of E holds E /\ (bool u) in E ) ::_thesis: ( ( for u being Element of E holds E /\ (bool u) in E ) implies E |= the_axiom_of_power_sets )
proof
set f0 = the Function of VAR,E;
assume A2: E |= the_axiom_of_power_sets ; ::_thesis: for u being Element of E holds E /\ (bool u) in E
let u be Element of E; ::_thesis: E /\ (bool u) in E
set f = the Function of VAR,E +* ((x. 0),u);
 E |= Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))))) by A2, ZF_MODEL:23;
then  E, the Function of VAR,E +* ((x. 0),u) |= Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))))) by ZF_MODEL:def_5;
then consider g being Function of VAR,E such that
A3: for x being Variable st g . x <> ( the Function of VAR,E +* ((x. 0),u)) . x holds
x. 1 = x and
A4: E,g |= All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))) by ZF_MODEL:20;
A5: ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) = u by FUNCT_7:128;
 g . (x. 1) = E /\ (bool u)
proof
thus  for a being set st a in g . (x. 1) holds
a in E /\ (bool u) :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: E /\ (bool u) c= g . (x. 1)
proof
let a be set ; ::_thesis: ( a in g . (x. 1) implies a in E /\ (bool u) )
assume A6: a in g . (x. 1) ; ::_thesis: a in E /\ (bool u)
 g . (x. 1) c= E by A1;
then reconsider a9 = a as Element of E by A6;
set h = g +* ((x. 2),a9);
A7: (g +* ((x. 2),a9)) . (x. 2) = a9 by FUNCT_7:128;
 for x being Variable st (g +* ((x. 2),a9)) . x <> g . x holds
x. 2 = x by FUNCT_7:32;
then A8: E,g +* ((x. 2),a9) |= ((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) by A4, ZF_MODEL:16;
 (g +* ((x. 2),a9)) . (x. 1) = g . (x. 1) by FUNCT_7:32;
then  E,g +* ((x. 2),a9) |= (x. 2) 'in' (x. 1) by A6, A7, ZF_MODEL:13;
then A9: E,g +* ((x. 2),a9) |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))) by A8, ZF_MODEL:19;
 a9 c= u
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in a9 or b in u )
assume A10: b in a9 ; ::_thesis: b in u
 a9 c= E by A1;
then reconsider b9 = b as Element of E by A10;
set m = (g +* ((x. 2),a9)) +* ((x. 3),b9);
A11: ((g +* ((x. 2),a9)) +* ((x. 3),b9)) . (x. 3) = b9 by FUNCT_7:128;
 for x being Variable st ((g +* ((x. 2),a9)) +* ((x. 3),b9)) . x <> (g +* ((x. 2),a9)) . x holds
x. 3 = x by FUNCT_7:32;
then A12: E,(g +* ((x. 2),a9)) +* ((x. 3),b9) |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)) by A9, ZF_MODEL:16;
 ((g +* ((x. 2),a9)) +* ((x. 3),b9)) . (x. 2) = (g +* ((x. 2),a9)) . (x. 2) by FUNCT_7:32;
then  E,(g +* ((x. 2),a9)) +* ((x. 3),b9) |= (x. 3) 'in' (x. 2) by A7, A10, A11, ZF_MODEL:13;
then A13: E,(g +* ((x. 2),a9)) +* ((x. 3),b9) |= (x. 3) 'in' (x. 0) by A12, ZF_MODEL:18;
A14: ( ((g +* ((x. 2),a9)) +* ((x. 3),b9)) . (x. 0) = (g +* ((x. 2),a9)) . (x. 0) & (g +* ((x. 2),a9)) . (x. 0) = g . (x. 0) ) by FUNCT_7:32;
 g . (x. 0) = ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) by A3;
hence  b in u by A5, A11, A13, A14, ZF_MODEL:13; ::_thesis: verum
end;
hence  a in E /\ (bool u) by XBOOLE_0:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in E /\ (bool u) or a in g . (x. 1) )
assume A15: a in E /\ (bool u) ; ::_thesis: a in g . (x. 1)
then A16: a in bool u by XBOOLE_0:def_4;
reconsider a = a as Element of E by A15, XBOOLE_0:def_4;
set h = g +* ((x. 2),a);
A17: (g +* ((x. 2),a)) . (x. 2) = a by FUNCT_7:128;
now__::_thesis:_for_m_being_Function_of_VAR,E_st_(_for_x_being_Variable_st_m_._x_<>_(g_+*_((x._2),a))_._x_holds_
x._3_=_x_)_holds_
E,m_|=_((x._3)_'in'_(x._2))_=>_((x._3)_'in'_(x._0))
let m be Function of VAR,E; ::_thesis: ( ( for x being Variable st m . x <> (g +* ((x. 2),a)) . x holds
x. 3 = x ) implies E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)) )
assume A18: for x being Variable st m . x <> (g +* ((x. 2),a)) . x holds
x. 3 = x ; ::_thesis: E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))
now__::_thesis:_(_E,m_|=_(x._3)_'in'_(x._2)_implies_E,m_|=_(x._3)_'in'_(x._0)_)
assume  E,m |= (x. 3) 'in' (x. 2) ; ::_thesis: E,m |= (x. 3) 'in' (x. 0)
then A19: m . (x. 3) in m . (x. 2) by ZF_MODEL:13;
A20: ( (g +* ((x. 2),a)) . (x. 0) = g . (x. 0) & g . (x. 0) = ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) ) by A3, FUNCT_7:32;
 ( m . (x. 2) = (g +* ((x. 2),a)) . (x. 2) & m . (x. 0) = (g +* ((x. 2),a)) . (x. 0) ) by A18;
hence  E,m |= (x. 3) 'in' (x. 0) by A5, A16, A17, A19, A20, ZF_MODEL:13; ::_thesis: verum
end;
hence  E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)) by ZF_MODEL:18; ::_thesis: verum
end;
then A21: E,g +* ((x. 2),a) |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))) by ZF_MODEL:16;
A22: (g +* ((x. 2),a)) . (x. 1) = g . (x. 1) by FUNCT_7:32;
 for x being Variable st (g +* ((x. 2),a)) . x <> g . x holds
x. 2 = x by FUNCT_7:32;
then  E,g +* ((x. 2),a) |= ((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) by A4, ZF_MODEL:16;
then  E,g +* ((x. 2),a) |= (x. 2) 'in' (x. 1) by A21, ZF_MODEL:19;
hence  a in g . (x. 1) by A17, A22, ZF_MODEL:13; ::_thesis: verum
end;
hence  E /\ (bool u) in E ; ::_thesis: verum
end;
assume A23: for u being Element of E holds E /\ (bool u) in E ; ::_thesis: E |= the_axiom_of_power_sets
 E |= Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))))))
proof
let f be Function of VAR,E; :: according to ZF_MODEL:def_5 ::_thesis: E,f |= Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))))))
reconsider v = E /\ (bool (f . (x. 0))) as Element of E by A23;
set g = f +* ((x. 1),v);
A24: (f +* ((x. 1),v)) . (x. 1) = v by FUNCT_7:128;
now__::_thesis:_for_h_being_Function_of_VAR,E_st_(_for_x_being_Variable_st_h_._x_<>_(f_+*_((x._1),v))_._x_holds_
x._2_=_x_)_holds_
E,h_|=_((x._2)_'in'_(x._1))_<=>_(All_((x._3),(((x._3)_'in'_(x._2))_=>_((x._3)_'in'_(x._0)))))
let h be Function of VAR,E; ::_thesis: ( ( for x being Variable st h . x <> (f +* ((x. 1),v)) . x holds
x. 2 = x ) implies E,h |= ((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) )
assume A25: for x being Variable st h . x <> (f +* ((x. 1),v)) . x holds
x. 2 = x ; ::_thesis: E,h |= ((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))
now__::_thesis:_(_(_E,h_|=_(x._2)_'in'_(x._1)_implies_E,h_|=_All_((x._3),(((x._3)_'in'_(x._2))_=>_((x._3)_'in'_(x._0))))_)_&_(_E,h_|=_All_((x._3),(((x._3)_'in'_(x._2))_=>_((x._3)_'in'_(x._0))))_implies_E,h_|=_(x._2)_'in'_(x._1)_)_)
thus  ( E,h |= (x. 2) 'in' (x. 1) implies E,h |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))) ) ::_thesis: ( E,h |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))) implies E,h |= (x. 2) 'in' (x. 1) )
proof
assume  E,h |= (x. 2) 'in' (x. 1) ; ::_thesis: E,h |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))
then A26: h . (x. 2) in h . (x. 1) by ZF_MODEL:13;
 h . (x. 1) = v by A24, A25;
then A27: h . (x. 2) in bool (f . (x. 0)) by A26, XBOOLE_0:def_4;
now__::_thesis:_for_m_being_Function_of_VAR,E_st_(_for_x_being_Variable_st_m_._x_<>_h_._x_holds_
x._3_=_x_)_holds_
E,m_|=_((x._3)_'in'_(x._2))_=>_((x._3)_'in'_(x._0))
let m be Function of VAR,E; ::_thesis: ( ( for x being Variable st m . x <> h . x holds
x. 3 = x ) implies E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)) )
assume A28: for x being Variable st m . x <> h . x holds
x. 3 = x ; ::_thesis: E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))
now__::_thesis:_(_E,m_|=_(x._3)_'in'_(x._2)_implies_E,m_|=_(x._3)_'in'_(x._0)_)
assume  E,m |= (x. 3) 'in' (x. 2) ; ::_thesis: E,m |= (x. 3) 'in' (x. 0)
then A29: m . (x. 3) in m . (x. 2) by ZF_MODEL:13;
A30: ( m . (x. 2) = h . (x. 2) & f . (x. 0) = (f +* ((x. 1),v)) . (x. 0) ) by A28, FUNCT_7:32;
 ( (f +* ((x. 1),v)) . (x. 0) = h . (x. 0) & h . (x. 0) = m . (x. 0) ) by A25, A28;
hence  E,m |= (x. 3) 'in' (x. 0) by A27, A29, A30, ZF_MODEL:13; ::_thesis: verum
end;
hence  E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)) by ZF_MODEL:18; ::_thesis: verum
end;
hence  E,h |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))) by ZF_MODEL:16; ::_thesis: verum
end;
assume A31: E,h |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))) ; ::_thesis: E,h |= (x. 2) 'in' (x. 1)
A32: h . (x. 2) c= f . (x. 0)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in h . (x. 2) or a in f . (x. 0) )
assume A33: a in h . (x. 2) ; ::_thesis: a in f . (x. 0)
 h . (x. 2) c= E by A1;
then reconsider a9 = a as Element of E by A33;
set m = h +* ((x. 3),a9);
A34: (h +* ((x. 3),a9)) . (x. 3) = a9 by FUNCT_7:128;
 for x being Variable st (h +* ((x. 3),a9)) . x <> h . x holds
x. 3 = x by FUNCT_7:32;
then A35: E,h +* ((x. 3),a9) |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)) by A31, ZF_MODEL:16;
 (h +* ((x. 3),a9)) . (x. 2) = h . (x. 2) by FUNCT_7:32;
then  E,h +* ((x. 3),a9) |= (x. 3) 'in' (x. 2) by A33, A34, ZF_MODEL:13;
then  E,h +* ((x. 3),a9) |= (x. 3) 'in' (x. 0) by A35, ZF_MODEL:18;
then A36: (h +* ((x. 3),a9)) . (x. 3) in (h +* ((x. 3),a9)) . (x. 0) by ZF_MODEL:13;
 ( (h +* ((x. 3),a9)) . (x. 0) = h . (x. 0) & (f +* ((x. 1),v)) . (x. 0) = f . (x. 0) ) by FUNCT_7:32;
hence  a in f . (x. 0) by A25, A34, A36; ::_thesis: verum
end;
 h . (x. 1) = (f +* ((x. 1),v)) . (x. 1) by A25;
then  h . (x. 2) in h . (x. 1) by A24, A32, XBOOLE_0:def_4;
hence  E,h |= (x. 2) 'in' (x. 1) by ZF_MODEL:13; ::_thesis: verum
end;
hence  E,h |= ((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) by ZF_MODEL:19; ::_thesis: verum
end;
then A37: E,f +* ((x. 1),v) |= All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))) by ZF_MODEL:16;
 for x being Variable st (f +* ((x. 1),v)) . x <> f . x holds
x. 1 = x by FUNCT_7:32;
hence  E,f |= Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))))) by A37, ZF_MODEL:20; ::_thesis: verum
end;
hence  E |= the_axiom_of_power_sets by ZF_MODEL:23; ::_thesis: verum
end;

theorem :: ZFMODEL1:9
for E being non empty set st E is epsilon-transitive holds
( E |= the_axiom_of_power_sets iff for X being set st X in E holds
E /\ (bool X) in E )
proof
let E be non empty set ; ::_thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_power_sets iff for X being set st X in E holds
E /\ (bool X) in E ) )
assume A1: E is epsilon-transitive ; ::_thesis: ( E |= the_axiom_of_power_sets iff for X being set st X in E holds
E /\ (bool X) in E )
hence  ( E |= the_axiom_of_power_sets implies for X being set st X in E holds
E /\ (bool X) in E ) by Th8; ::_thesis: ( ( for X being set st X in E holds
E /\ (bool X) in E ) implies E |= the_axiom_of_power_sets )
assume  for X being set st X in E holds
E /\ (bool X) in E ; ::_thesis: E |= the_axiom_of_power_sets
then  for u being Element of E holds E /\ (bool u) in E ;
hence  E |= the_axiom_of_power_sets by A1, Th8; ::_thesis: verum
end;

defpred S1[ Nat] means  for x being Variable
for E being non empty set
for H being ZF-formula
for f being Function of VAR,E st len H = $1 & not x in Free H & E,f |= H holds
E,f |= All (x,H);

Lm1:  for n being Nat st ( for k being Nat st k < n holds
S1[k] ) holds
S1[n]
proof
let n be Nat; ::_thesis: ( ( for k being Nat st k < n holds
S1[k] ) implies S1[n] )
assume A1: for k being Nat st k < n holds
for x being Variable
for E being non empty set
for H being ZF-formula
for f being Function of VAR,E st len H = k & not x in Free H & E,f |= H holds
E,f |= All (x,H) ; ::_thesis: S1[n]
let x be Variable; ::_thesis: for E being non empty set
for H being ZF-formula
for f being Function of VAR,E st len H = n & not x in Free H & E,f |= H holds
E,f |= All (x,H)
let E be non empty set ; ::_thesis: for H being ZF-formula
for f being Function of VAR,E st len H = n & not x in Free H & E,f |= H holds
E,f |= All (x,H)
let H be ZF-formula; ::_thesis: for f being Function of VAR,E st len H = n & not x in Free H & E,f |= H holds
E,f |= All (x,H)
let f be Function of VAR,E; ::_thesis: ( len H = n & not x in Free H & E,f |= H implies E,f |= All (x,H) )
assume that
A2: len H = n and
A3: not x in Free H and
A4: E,f |= H ; ::_thesis: E,f |= All (x,H)
A5: now__::_thesis:_(_H_is_being_equality_implies_E,f_|=_All_(x,H)_)
assume A6: H is being_equality ; ::_thesis: E,f |= All (x,H)
then  Free H = {(Var1 H),(Var2 H)} by ZF_MODEL:1;
then A7: ( x <> Var1 H & x <> Var2 H ) by A3, TARSKI:def_2;
A8: H = (Var1 H) '=' (Var2 H) by A6, ZF_LANG:36;
then A9: f . (Var1 H) = f . (Var2 H) by A4, ZF_MODEL:12;
now__::_thesis:_for_g_being_Function_of_VAR,E_st_(_for_y_being_Variable_st_g_._y_<>_f_._y_holds_
x_=_y_)_holds_
E,g_|=_H
let g be Function of VAR,E; ::_thesis: ( ( for y being Variable st g . y <> f . y holds
x = y ) implies E,g |= H )
assume  for y being Variable st g . y <> f . y holds
x = y ; ::_thesis: E,g |= H
then  ( g . (Var1 H) = f . (Var1 H) & g . (Var2 H) = f . (Var2 H) ) by A7;
hence  E,g |= H by A8, A9, ZF_MODEL:12; ::_thesis: verum
end;
hence  E,f |= All (x,H) by ZF_MODEL:16; ::_thesis: verum
end;
A10: now__::_thesis:_(_H_is_universal_implies_E,f_|=_All_(x,H)_)
assume A11: H is universal ; ::_thesis: E,f |= All (x,H)
then A12: H = All ((bound_in H),(the_scope_of H)) by ZF_LANG:44;
 Free H = (Free (the_scope_of H)) \ {(bound_in H)} by A11, ZF_MODEL:1;
then A13: ( not x in Free (the_scope_of H) or x in {(bound_in H)} ) by A3, XBOOLE_0:def_5;
A14: now__::_thesis:_(_x_<>_bound_in_H_implies_E,f_|=_All_(x,H)_)
assume A15: x <> bound_in H ; ::_thesis: E,f |= All (x,H)
assume  not E,f |= All (x,H) ; ::_thesis: contradiction
then consider g being Function of VAR,E such that
A16: for y being Variable st g . y <> f . y holds
x = y and
A17: not E,g |= H by ZF_MODEL:16;
consider h being Function of VAR,E such that
A18: for y being Variable st h . y <> g . y holds
bound_in H = y and
A19: not E,h |= the_scope_of H by A12, A17, ZF_MODEL:16;
set m = f +* ((bound_in H),(h . (bound_in H)));
A20: now__::_thesis:_for_y_being_Variable_st_h_._y_<>_(f_+*_((bound_in_H),(h_._(bound_in_H))))_._y_holds_
not_x_<>_y
let y be Variable; ::_thesis: ( h . y <> (f +* ((bound_in H),(h . (bound_in H)))) . y implies not x <> y )
assume A21: h . y <> (f +* ((bound_in H),(h . (bound_in H)))) . y ; ::_thesis: not x <> y
assume  x <> y ; ::_thesis: contradiction
then A22: f . y = g . y by A16;
A23: y <> bound_in H by A21, FUNCT_7:128;
then  (f +* ((bound_in H),(h . (bound_in H)))) . y = f . y by FUNCT_7:32;
hence  contradiction by A18, A21, A23, A22; ::_thesis: verum
end;
 the_scope_of H is_immediate_constituent_of H by A12, ZF_LANG:def_39;
then A24: len (the_scope_of H) < len H by ZF_LANG:60;
 for y being Variable st (f +* ((bound_in H),(h . (bound_in H)))) . y <> f . y holds
bound_in H = y by FUNCT_7:32;
then  E,f +* ((bound_in H),(h . (bound_in H))) |= the_scope_of H by A4, A12, ZF_MODEL:16;
then  E,f +* ((bound_in H),(h . (bound_in H))) |= All (x,(the_scope_of H)) by A1, A2, A13, A15, A24, TARSKI:def_1;
hence  contradiction by A19, A20, ZF_MODEL:16; ::_thesis: verum
end;
now__::_thesis:_(_x_=_bound_in_H_implies_E,f_|=_All_(x,H)_)
assume A25: x = bound_in H ; ::_thesis: E,f |= All (x,H)
now__::_thesis:_for_g_being_Function_of_VAR,E_st_(_for_y_being_Variable_holds_
(_not_g_._y_<>_f_._y_or_x_=_y_or_bound_in_H_=_y_)_)_holds_
E,g_|=_the_scope_of_H
let g be Function of VAR,E; ::_thesis: ( ( for y being Variable holds
( not g . y <> f . y or x = y or bound_in H = y ) ) implies E,g |= the_scope_of H )
assume  for y being Variable holds
( not g . y <> f . y or x = y or bound_in H = y ) ; ::_thesis: E,g |= the_scope_of H
then  for y being Variable st g . y <> f . y holds
bound_in H = y by A25;
hence  E,g |= the_scope_of H by A4, A12, ZF_MODEL:16; ::_thesis: verum
end;
then  E,f |= All (x,(bound_in H),(the_scope_of H)) by ZF_MODEL:21;
hence  E,f |= All (x,H) by A11, ZF_LANG:44; ::_thesis: verum
end;
hence  E,f |= All (x,H) by A14; ::_thesis: verum
end;
A26: now__::_thesis:_(_H_is_conjunctive_implies_E,f_|=_All_(x,H)_)
assume A27: H is conjunctive ; ::_thesis: E,f |= All (x,H)
then A28: H = (the_left_argument_of H) '&' (the_right_argument_of H) by ZF_LANG:40;
then  the_right_argument_of H is_immediate_constituent_of H by ZF_LANG:def_39;
then A29: len (the_right_argument_of H) < len H by ZF_LANG:60;
 the_left_argument_of H is_immediate_constituent_of H by A28, ZF_LANG:def_39;
then A30: len (the_left_argument_of H) < len H by ZF_LANG:60;
A31: Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H)) by A27, ZF_MODEL:1;
then A32: not x in Free (the_left_argument_of H) by A3, XBOOLE_0:def_3;
A33: not x in Free (the_right_argument_of H) by A3, A31, XBOOLE_0:def_3;
 E,f |= the_right_argument_of H by A4, A28, ZF_MODEL:15;
then A34: E,f |= All (x,(the_right_argument_of H)) by A1, A2, A33, A29;
 E,f |= the_left_argument_of H by A4, A28, ZF_MODEL:15;
then A35: E,f |= All (x,(the_left_argument_of H)) by A1, A2, A32, A30;
now__::_thesis:_for_g_being_Function_of_VAR,E_st_(_for_y_being_Variable_st_g_._y_<>_f_._y_holds_
x_=_y_)_holds_
E,g_|=_H
let g be Function of VAR,E; ::_thesis: ( ( for y being Variable st g . y <> f . y holds
x = y ) implies E,g |= H )
assume  for y being Variable st g . y <> f . y holds
x = y ; ::_thesis: E,g |= H
then  ( E,g |= the_left_argument_of H & E,g |= the_right_argument_of H ) by A35, A34, ZF_MODEL:16;
hence  E,g |= H by A28, ZF_MODEL:15; ::_thesis: verum
end;
hence  E,f |= All (x,H) by ZF_MODEL:16; ::_thesis: verum
end;
A36: now__::_thesis:_(_H_is_being_membership_implies_E,f_|=_All_(x,H)_)
assume A37: H is being_membership ; ::_thesis: E,f |= All (x,H)
then  Free H = {(Var1 H),(Var2 H)} by ZF_MODEL:1;
then A38: ( x <> Var1 H & x <> Var2 H ) by A3, TARSKI:def_2;
A39: H = (Var1 H) 'in' (Var2 H) by A37, ZF_LANG:37;
then A40: f . (Var1 H) in f . (Var2 H) by A4, ZF_MODEL:13;
now__::_thesis:_for_g_being_Function_of_VAR,E_st_(_for_y_being_Variable_st_g_._y_<>_f_._y_holds_
x_=_y_)_holds_
E,g_|=_H
let g be Function of VAR,E; ::_thesis: ( ( for y being Variable st g . y <> f . y holds
x = y ) implies E,g |= H )
assume  for y being Variable st g . y <> f . y holds
x = y ; ::_thesis: E,g |= H
then  ( g . (Var1 H) = f . (Var1 H) & g . (Var2 H) = f . (Var2 H) ) by A38;
hence  E,g |= H by A39, A40, ZF_MODEL:13; ::_thesis: verum
end;
hence  E,f |= All (x,H) by ZF_MODEL:16; ::_thesis: verum
end;
now__::_thesis:_(_H_is_negative_implies_E,f_|=_All_(x,H)_)
assume A41: H is negative ; ::_thesis: E,f |= All (x,H)
then A42: H = 'not' (the_argument_of H) by ZF_LANG:def_30;
then  the_argument_of H is_immediate_constituent_of H by ZF_LANG:def_39;
then A43: len (the_argument_of H) < len H by ZF_LANG:60;
A44: not x in Free (the_argument_of H) by A3, A41, ZF_MODEL:1;
assume  not E,f |= All (x,H) ; ::_thesis: contradiction
then consider g being Function of VAR,E such that
A45: for y being Variable st g . y <> f . y holds
x = y and
A46: not E,g |= H by ZF_MODEL:16;
 E,g |= the_argument_of H by A42, A46, ZF_MODEL:14;
then  E,g |= All (x,(the_argument_of H)) by A1, A2, A43, A44;
then  E,f |= the_argument_of H by A45, ZF_MODEL:16;
hence  contradiction by A4, A42, ZF_MODEL:14; ::_thesis: verum
end;
hence  E,f |= All (x,H) by A5, A36, A26, A10, ZF_LANG:9; ::_thesis: verum
end;

theorem Th10: :: ZFMODEL1:10
for x being Variable
for H being ZF-formula
for E being non empty set
for f being Function of VAR,E st not x in Free H & E,f |= H holds
E,f |= All (x,H)
proof
let x be Variable; ::_thesis: for H being ZF-formula
for E being non empty set
for f being Function of VAR,E st not x in Free H & E,f |= H holds
E,f |= All (x,H)
let H be ZF-formula; ::_thesis: for E being non empty set
for f being Function of VAR,E st not x in Free H & E,f |= H holds
E,f |= All (x,H)
let E be non empty set ; ::_thesis: for f being Function of VAR,E st not x in Free H & E,f |= H holds
E,f |= All (x,H)
let f be Function of VAR,E; ::_thesis: ( not x in Free H & E,f |= H implies E,f |= All (x,H) )
A1: len H = len H ;
 for n being Nat holds S1[n] from NAT_1:sch_4(Lm1);
hence  ( not x in Free H & E,f |= H implies E,f |= All (x,H) ) by A1; ::_thesis: verum
end;

Lm2:  for x being Variable
for H being ZF-formula holds
( the_scope_of (All (x,H)) = H & bound_in (All (x,H)) = x )
proof
let x be Variable; ::_thesis: for H being ZF-formula holds
( the_scope_of (All (x,H)) = H & bound_in (All (x,H)) = x )
let H be ZF-formula; ::_thesis: ( the_scope_of (All (x,H)) = H & bound_in (All (x,H)) = x )
 All (x,H) is universal by ZF_LANG:5;
then  All (x,H) = All ((bound_in (All (x,H))),(the_scope_of (All (x,H)))) by ZF_LANG:44;
hence  ( the_scope_of (All (x,H)) = H & bound_in (All (x,H)) = x ) by ZF_LANG:3; ::_thesis: verum
end;

theorem Th11: :: ZFMODEL1:11
for x, y being Variable
for H being ZF-formula
for E being non empty set
for f being Function of VAR,E st {x,y} misses Free H & E,f |= H holds
E,f |= All (x,y,H)
proof
let x, y be Variable; ::_thesis: for H being ZF-formula
for E being non empty set
for f being Function of VAR,E st {x,y} misses Free H & E,f |= H holds
E,f |= All (x,y,H)
let H be ZF-formula; ::_thesis: for E being non empty set
for f being Function of VAR,E st {x,y} misses Free H & E,f |= H holds
E,f |= All (x,y,H)
let E be non empty set ; ::_thesis: for f being Function of VAR,E st {x,y} misses Free H & E,f |= H holds
E,f |= All (x,y,H)
let f be Function of VAR,E; ::_thesis: ( {x,y} misses Free H & E,f |= H implies E,f |= All (x,y,H) )
assume that
A1: {x,y} misses Free H and
A2: E,f |= H ; ::_thesis: E,f |= All (x,y,H)
A3: bound_in (All (y,H)) = y by Lm2;
 ( All (y,H) is universal & the_scope_of (All (y,H)) = H ) by Lm2, ZF_LANG:5;
then A4: Free (All (y,H)) = (Free H) \ {y} by A3, ZF_MODEL:1;
 x in {x,y} by TARSKI:def_2;
then  not x in Free H by A1, XBOOLE_0:3;
then A5: not x in Free (All (y,H)) by A4, XBOOLE_0:def_5;
 y in {x,y} by TARSKI:def_2;
then  not y in Free H by A1, XBOOLE_0:3;
then  E,f |= All (y,H) by A2, Th10;
hence  E,f |= All (x,y,H) by A5, Th10; ::_thesis: verum
end;

theorem :: ZFMODEL1:12
for x, y, z being Variable
for H being ZF-formula
for E being non empty set
for f being Function of VAR,E st {x,y,z} misses Free H & E,f |= H holds
E,f |= All (x,y,z,H)
proof
let x, y, z be Variable; ::_thesis: for H being ZF-formula
for E being non empty set
for f being Function of VAR,E st {x,y,z} misses Free H & E,f |= H holds
E,f |= All (x,y,z,H)
let H be ZF-formula; ::_thesis: for E being non empty set
for f being Function of VAR,E st {x,y,z} misses Free H & E,f |= H holds
E,f |= All (x,y,z,H)
let E be non empty set ; ::_thesis: for f being Function of VAR,E st {x,y,z} misses Free H & E,f |= H holds
E,f |= All (x,y,z,H)
let f be Function of VAR,E; ::_thesis: ( {x,y,z} misses Free H & E,f |= H implies E,f |= All (x,y,z,H) )
assume that
A1: {x,y,z} misses Free H and
A2: E,f |= H ; ::_thesis: E,f |= All (x,y,z,H)
A3: bound_in (All (y,(All (z,H)))) = y by Lm2;
now__::_thesis:_for_a_being_set_st_a_in_{y,z}_holds_
not_a_in_Free_H
let a be set ; ::_thesis: ( a in {y,z} implies not a in Free H )
assume  a in {y,z} ; ::_thesis: not a in Free H
then  ( a = y or a = z ) by TARSKI:def_2;
then  a in {x,y,z} by ENUMSET1:def_1;
hence  not a in Free H by A1, XBOOLE_0:3; ::_thesis: verum
end;
then  {y,z} misses Free H by XBOOLE_0:3;
then A4: E,f |= All (y,z,H) by A2, Th11;
A5: ( All (z,H) is universal & the_scope_of (All (z,H)) = H ) by Lm2, ZF_LANG:5;
 x in {x,y,z} by ENUMSET1:def_1;
then  not x in Free H by A1, XBOOLE_0:3;
then  not x in (Free H) \ {z} by XBOOLE_0:def_5;
then A6: not x in ((Free H) \ {z}) \ {y} by XBOOLE_0:def_5;
A7: bound_in (All (z,H)) = z by Lm2;
 ( All (y,(All (z,H))) is universal & the_scope_of (All (y,(All (z,H)))) = All (z,H) ) by Lm2, ZF_LANG:5;
then  Free (All (y,z,H)) = (Free (All (z,H))) \ {y} by A3, ZF_MODEL:1
.= ((Free H) \ {z}) \ {y} by A5, A7, ZF_MODEL:1 ;
hence  E,f |= All (x,y,z,H) by A4, A6, Th10; ::_thesis: verum
end;

definition
let H be ZF-formula;
let E be non empty set ;
let val be Function of VAR,E;
assume that
A1: not x. 0 in Free H and
A2: E,val |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ;
func def_func' (H,val) ->  Function of E,E means :Def1: :: ZFMODEL1:def 1
 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 it . (g . (x. 3)) = g . (x. 4) );
existence
 ex b1 being Function of E,E st
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 b1 . (g . (x. 3)) = g . (x. 4) )
proof
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:87;
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:32;
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:128;
set g1 = g +* ((x. 4),b9);
A9: (g +* ((x. 4),b9)) . (x. 4) = b9 by FUNCT_7:128;
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:32;
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:32;
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:32;
 ( [a,b] `1 = a9 & [a,b] `2 = b9 ) ;
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:128;
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:32;
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:32;
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:32;
 ( [a,c] `1 = a9 & [a,c] `2 = c9 ) ;
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:32;
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_3;
 [a,b] in F by A26, FUNCT_1:1;
then  [a,b] in [:E,E:] by A3;
hence  b in E by ZFMISC_1:87; ::_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:32;
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:128;
A31: now__::_thesis:_for_f_being_Function_of_VAR,E_st_S2[f]_&_f_._(x._3)_=_[a9,(h_._(x._0))]_`1_&_f_._(x._4)_=_[a9,(h_._(x._0))]_`2_holds_
E,f_|=_H
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:128;
A36: now__::_thesis:_for_x_being_Variable_st_f_._x_<>_(h_+*_((x._4),(h_._(x._0))))_._x_holds_
not_x._0_<>_x
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;
then A39: (h +* ((x. 4),(h . (x. 0)))) . x = h . x by FUNCT_7:32;
 ( (val +* ((x. 3),a9)) . (x. 3) = h . (x. 3) & h . (x. 3) = (h +* ((x. 4),(h . (x. 0)))) . (x. 3) ) by A28, FUNCT_7:32;
then A40: x <> x. 3 by A30, A33, A37;
then A41: (val +* ((x. 3),a9)) . x = val . x by FUNCT_7:32;
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:32;
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:32;
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:87;
then  [a9,(h . (x. 0))] in X by A3, A31;
hence  a in dom F by FUNCT_1:1; ::_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 XTUPLE_0:def_12;
 [a,b] in [:E,E:] by A3, A44;
hence  a in E by ZFMISC_1:87; ::_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:4;
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__::_thesis:_for_g_being_Function_of_VAR,E_st_S2[g]_&_g_._(x._3)_=_[(f_._(x._3)),(f_._(x._4))]_`1_&_g_._(x._4)_=_[(f_._(x._3)),(f_._(x._4))]_`2_holds_
E,g_|=_H
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__::_thesis:_for_x_being_Variable_st_g_._x_<>_f_._x_holds_
not_x._0_<>_x
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;
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:87;
then  [(f . (x. 3)),(f . (x. 4))] in X by A3, A47;
hence  F . (f . (x. 3)) = f . (x. 4) by FUNCT_1:1; ::_thesis: verum
end;
A53: ( [(f . (x. 3)),(f . (x. 4))] `1 = f . (x. 3) & [(f . (x. 3)),(f . (x. 4))] `2 = f . (x. 4) ) ;
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:1;
hence  E,f |= H by A3, A45, A53; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of E,E st ( 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 b1 . (g . (x. 3)) = g . (x. 4) ) ) & ( 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 b2 . (g . (x. 3)) = g . (x. 4) ) ) holds
b1 = b2
proof
let F1, F2 be Function of E,E; ::_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 F1 . (g . (x. 3)) = g . (x. 4) ) ) & ( 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 F2 . (g . (x. 3)) = g . (x. 4) ) ) implies F1 = F2 )
assume that
A55: 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 F1 . (g . (x. 3)) = g . (x. 4) ) and
A56: 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 F2 . (g . (x. 3)) = g . (x. 4) ) ; ::_thesis: F1 = F2
let a be Element of E; :: according to FUNCT_2:def_8 ::_thesis: F1 . a = F2 . a
set f = val +* ((x. 3),a);
 for x being Variable st (val +* ((x. 3),a)) . x <> val . x holds
x. 3 = x by FUNCT_7:32;
then  E,val +* ((x. 3),a) |= 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
A57: for x being Variable st g . x <> (val +* ((x. 3),a)) . x holds
x. 0 = x and
A58: E,g |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_MODEL:20;
A59: g . (x. 3) = (val +* ((x. 3),a)) . (x. 3) by A57;
set h = g +* ((x. 4),(g . (x. 0)));
A60: now__::_thesis:_for_x_being_Variable_st_(g_+*_((x._4),(g_._(x._0))))_._x_<>_val_._x_&_x._0_<>_x_&_x._3_<>_x_holds_
not_x._4_<>_x
let x be Variable; ::_thesis: ( (g +* ((x. 4),(g . (x. 0)))) . x <> val . x & x. 0 <> x & x. 3 <> x implies not x. 4 <> x )
assume that
A61: ( (g +* ((x. 4),(g . (x. 0)))) . x <> val . x & x. 0 <> x ) and
A62: ( x. 3 <> x & x. 4 <> x ) ; ::_thesis: contradiction
 ( (val +* ((x. 3),a)) . x = val . x & (g +* ((x. 4),(g . (x. 0)))) . x = g . x ) by A62, FUNCT_7:32;
hence  contradiction by A57, A61; ::_thesis: verum
end;
 ( (g +* ((x. 4),(g . (x. 0)))) . (x. 4) = g . (x. 0) & (g +* ((x. 4),(g . (x. 0)))) . (x. 0) = g . (x. 0) ) by FUNCT_7:32, FUNCT_7:128;
then A63: E,g +* ((x. 4),(g . (x. 0))) |= (x. 4) '=' (x. 0) by ZF_MODEL:12;
A64: ( (val +* ((x. 3),a)) . (x. 3) = a & (g +* ((x. 4),(g . (x. 0)))) . (x. 3) = g . (x. 3) ) by FUNCT_7:32, FUNCT_7:128;
 for x being Variable st (g +* ((x. 4),(g . (x. 0)))) . x <> g . x holds
x. 4 = x by FUNCT_7:32;
then  E,g +* ((x. 4),(g . (x. 0))) |= H <=> ((x. 4) '=' (x. 0)) by A58, ZF_MODEL:16;
then A65: E,g +* ((x. 4),(g . (x. 0))) |= H by A63, ZF_MODEL:19;
then  F1 . ((g +* ((x. 4),(g . (x. 0)))) . (x. 3)) = (g +* ((x. 4),(g . (x. 0)))) . (x. 4) by A55, A60;
hence  F1 . a = F2 . a by A56, A65, A60, A64, A59; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines def_func' ZFMODEL1:def_1_:_
 for H being ZF-formula
for E being non empty set
for val being Function of VAR,E st not x. 0 in Free H & E,val |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for b4 being Function of E,E holds
( b4 = def_func' (H,val) iff 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 b4 . (g . (x. 3)) = g . (x. 4) ) );

theorem Th13: :: ZFMODEL1:13
for E being non empty set
for H being ZF-formula
for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds
not x in Free H ) & E,f |= H holds
E,g |= H
proof
let E be non empty set ; ::_thesis: for H being ZF-formula
for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds
not x in Free H ) & E,f |= H holds
E,g |= H
defpred S2[ ZF-formula] means  for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds
not x in Free $1 ) & E,f |= $1 holds
E,g |= $1;
A1: for H being ZF-formula st H is atomic holds
S2[H]
proof
let H be ZF-formula; ::_thesis: ( H is atomic implies S2[H] )
assume A2: ( H is being_equality or H is being_membership ) ; :: according to ZF_LANG:def_15 ::_thesis: S2[H]
let f, g be Function of VAR,E; ::_thesis: ( ( for x being Variable st f . x <> g . x holds
not x in Free H ) & E,f |= H implies E,g |= H )
assume that
A3: for x being Variable st f . x <> g . x holds
not x in Free H and
A4: E,f |= H ; ::_thesis: E,g |= H
A5: now__::_thesis:_(_H_is_being_membership_implies_E,g_|=_H_)
assume A6: H is being_membership ; ::_thesis: E,g |= H
then A7: Free H = {(Var1 H),(Var2 H)} by ZF_MODEL:1;
then  Var1 H in Free H by TARSKI:def_2;
then A8: f . (Var1 H) = g . (Var1 H) by A3;
 Var2 H in Free H by A7, TARSKI:def_2;
then A9: f . (Var2 H) = g . (Var2 H) by A3;
A10: H = (Var1 H) 'in' (Var2 H) by A6, ZF_LANG:37;
then  f . (Var1 H) in f . (Var2 H) by A4, ZF_MODEL:13;
hence  E,g |= H by A10, A8, A9, ZF_MODEL:13; ::_thesis: verum
end;
now__::_thesis:_(_H_is_being_equality_implies_E,g_|=_H_)
assume A11: H is being_equality ; ::_thesis: E,g |= H
then A12: Free H = {(Var1 H),(Var2 H)} by ZF_MODEL:1;
then  Var1 H in Free H by TARSKI:def_2;
then A13: f . (Var1 H) = g . (Var1 H) by A3;
 Var2 H in Free H by A12, TARSKI:def_2;
then A14: f . (Var2 H) = g . (Var2 H) by A3;
A15: H = (Var1 H) '=' (Var2 H) by A11, ZF_LANG:36;
then  f . (Var1 H) = f . (Var2 H) by A4, ZF_MODEL:12;
hence  E,g |= H by A15, A13, A14, ZF_MODEL:12; ::_thesis: verum
end;
hence  E,g |= H by A2, A5; ::_thesis: verum
end;
A16: for H being ZF-formula st H is conjunctive & S2[ the_left_argument_of H] & S2[ the_right_argument_of H] holds
S2[H]
proof
let H be ZF-formula; ::_thesis: ( H is conjunctive & S2[ the_left_argument_of H] & S2[ the_right_argument_of H] implies S2[H] )
assume A17: H is conjunctive ; ::_thesis: ( not S2[ the_left_argument_of H] or not S2[ the_right_argument_of H] or S2[H] )
then A18: H = (the_left_argument_of H) '&' (the_right_argument_of H) by ZF_LANG:40;
assume that
A19: for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds
not x in Free (the_left_argument_of H) ) & E,f |= the_left_argument_of H holds
E,g |= the_left_argument_of H and
A20: for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds
not x in Free (the_right_argument_of H) ) & E,f |= the_right_argument_of H holds
E,g |= the_right_argument_of H ; ::_thesis: S2[H]
let f, g be Function of VAR,E; ::_thesis: ( ( for x being Variable st f . x <> g . x holds
not x in Free H ) & E,f |= H implies E,g |= H )
assume that
A21: for x being Variable st f . x <> g . x holds
not x in Free H and
A22: E,f |= H ; ::_thesis: E,g |= H
A23: Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H)) by A17, ZF_MODEL:1;
A24: now__::_thesis:_for_x_being_Variable_st_f_._x_<>_g_._x_holds_
not_x_in_Free_(the_right_argument_of_H)
let x be Variable; ::_thesis: ( f . x <> g . x implies not x in Free (the_right_argument_of H) )
assume  f . x <> g . x ; ::_thesis: not x in Free (the_right_argument_of H)
then  not x in Free H by A21;
hence  not x in Free (the_right_argument_of H) by A23, XBOOLE_0:def_3; ::_thesis: verum
end;
A25: now__::_thesis:_for_x_being_Variable_st_f_._x_<>_g_._x_holds_
not_x_in_Free_(the_left_argument_of_H)
let x be Variable; ::_thesis: ( f . x <> g . x implies not x in Free (the_left_argument_of H) )
assume  f . x <> g . x ; ::_thesis: not x in Free (the_left_argument_of H)
then  not x in Free H by A21;
hence  not x in Free (the_left_argument_of H) by A23, XBOOLE_0:def_3; ::_thesis: verum
end;
 E,f |= the_right_argument_of H by A18, A22, ZF_MODEL:15;
then A26: E,g |= the_right_argument_of H by A20, A24;
 E,f |= the_left_argument_of H by A18, A22, ZF_MODEL:15;
then  E,g |= the_left_argument_of H by A19, A25;
hence  E,g |= H by A18, A26, ZF_MODEL:15; ::_thesis: verum
end;
A27: for H being ZF-formula st H is universal & S2[ the_scope_of H] holds
S2[H]
proof
let H be ZF-formula; ::_thesis: ( H is universal & S2[ the_scope_of H] implies S2[H] )
assume A28: H is universal ; ::_thesis: ( not S2[ the_scope_of H] or S2[H] )
then A29: H = All ((bound_in H),(the_scope_of H)) by ZF_LANG:44;
assume A30: for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds
not x in Free (the_scope_of H) ) & E,f |= the_scope_of H holds
E,g |= the_scope_of H ; ::_thesis: S2[H]
let f, g be Function of VAR,E; ::_thesis: ( ( for x being Variable st f . x <> g . x holds
not x in Free H ) & E,f |= H implies E,g |= H )
assume that
A31: for x being Variable st f . x <> g . x holds
not x in Free H and
A32: E,f |= H ; ::_thesis: E,g |= H
A33: Free H = (Free (the_scope_of H)) \ {(bound_in H)} by A28, ZF_MODEL:1;
now__::_thesis:_for_j_being_Function_of_VAR,E_st_(_for_x_being_Variable_st_j_._x_<>_g_._x_holds_
bound_in_H_=_x_)_holds_
E,j_|=_the_scope_of_H
let j be Function of VAR,E; ::_thesis: ( ( for x being Variable st j . x <> g . x holds
bound_in H = x ) implies E,j |= the_scope_of H )
assume A34: for x being Variable st j . x <> g . x holds
bound_in H = x ; ::_thesis: E,j |= the_scope_of H
set h = f +* ((bound_in H),(j . (bound_in H)));
A35: now__::_thesis:_for_x_being_Variable_st_(f_+*_((bound_in_H),(j_._(bound_in_H))))_._x_<>_j_._x_holds_
not_x_in_Free_(the_scope_of_H)
let x be Variable; ::_thesis: ( (f +* ((bound_in H),(j . (bound_in H)))) . x <> j . x implies not x in Free (the_scope_of H) )
assume A36: (f +* ((bound_in H),(j . (bound_in H)))) . x <> j . x ; ::_thesis: not x in Free (the_scope_of H)
then A37: x <> bound_in H by FUNCT_7:128;
then  ( (f +* ((bound_in H),(j . (bound_in H)))) . x = f . x & j . x = g . x ) by A34, FUNCT_7:32;
then A38: not x in Free H by A31, A36;
 not x in {(bound_in H)} by A37, TARSKI:def_1;
hence  not x in Free (the_scope_of H) by A33, A38, XBOOLE_0:def_5; ::_thesis: verum
end;
 for x being Variable st (f +* ((bound_in H),(j . (bound_in H)))) . x <> f . x holds
bound_in H = x by FUNCT_7:32;
then  E,f +* ((bound_in H),(j . (bound_in H))) |= the_scope_of H by A29, A32, ZF_MODEL:16;
hence  E,j |= the_scope_of H by A30, A35; ::_thesis: verum
end;
hence  E,g |= H by A29, ZF_MODEL:16; ::_thesis: verum
end;
A39: for H being ZF-formula st H is negative & S2[ the_argument_of H] holds
S2[H]
proof
let H be ZF-formula; ::_thesis: ( H is negative & S2[ the_argument_of H] implies S2[H] )
assume A40: H is negative ; ::_thesis: ( not S2[ the_argument_of H] or S2[H] )
then A41: Free H = Free (the_argument_of H) by ZF_MODEL:1;
assume A42: for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds
not x in Free (the_argument_of H) ) & E,f |= the_argument_of H holds
E,g |= the_argument_of H ; ::_thesis: S2[H]
let f, g be Function of VAR,E; ::_thesis: ( ( for x being Variable st f . x <> g . x holds
not x in Free H ) & E,f |= H implies E,g |= H )
assume that
A43: for x being Variable st f . x <> g . x holds
not x in Free H and
A44: E,f |= H and
A45: not E,g |= H ; ::_thesis: contradiction
A46: H = 'not' (the_argument_of H) by A40, ZF_LANG:def_30;
then  E,g |= the_argument_of H by A45, ZF_MODEL:14;
then  E,f |= the_argument_of H by A41, A42, A43;
hence  contradiction by A46, A44, ZF_MODEL:14; ::_thesis: verum
end;
thus  for H being ZF-formula holds S2[H] from ZF_LANG:sch_1(A1, A39, A16, A27); ::_thesis: verum
end;

definition
let H be ZF-formula;
let E be non empty set ;
assume that
A1: Free H c= {(x. 3),(x. 4)} and
A2: E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ;
func def_func (H,E) ->  Function of E,E means :Def2: :: ZFMODEL1:def 2
 for g being Function of VAR,E holds
( E,g |= H iff it . (g . (x. 3)) = g . (x. 4) );
existence
 ex b1 being Function of E,E st
for g being Function of VAR,E holds
( E,g |= H iff b1 . (g . (x. 3)) = g . (x. 4) )
proof
set f = the Function of VAR,E;
take F = def_func' (H, the Function of VAR,E); ::_thesis: for g being Function of VAR,E holds
( E,g |= H iff F . (g . (x. 3)) = g . (x. 4) )
let g be Function of VAR,E; ::_thesis: ( E,g |= H iff F . (g . (x. 3)) = g . (x. 4) )
set j = the Function of VAR,E +* ((x. 3),(g . (x. 3)));
set h = ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)));
A3: now__::_thesis:_for_x_being_Variable_st_((_the_Function_of_VAR,E_+*_((x._3),(g_._(x._3))))_+*_((x._4),(g_._(x._4))))_._x_<>_the_Function_of_VAR,E_._x_&_x._0_<>_x_&_x._3_<>_x_holds_
not_x._4_<>_x
let x be Variable; ::_thesis: ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x & x. 0 <> x & x. 3 <> x implies not x. 4 <> x )
assume that
A4: (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x and
 x. 0 <> x and
A5: x. 3 <> x and
A6: x. 4 <> x ; ::_thesis: contradiction
(( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x = ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) . x by A6, FUNCT_7:32
.= the Function of VAR,E . x by A5, FUNCT_7:32 ;
hence  contradiction by A4; ::_thesis: verum
end;
A7: ( not x. 0 in Free H & E, the Function of VAR,E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ) by A1, A2, TARSKI:def_2, ZF_MODEL:def_5;
thus  ( E,g |= H implies F . (g . (x. 3)) = g . (x. 4) ) ::_thesis: ( F . (g . (x. 3)) = g . (x. 4) implies E,g |= H )
proof
set g3 = the Function of VAR,E +* ((x. 3),(g . (x. 3)));
set g4 = ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)));
A8: now__::_thesis:_for_x_being_Variable_st_((_the_Function_of_VAR,E_+*_((x._3),(g_._(x._3))))_+*_((x._4),(g_._(x._4))))_._x_<>_the_Function_of_VAR,E_._x_&_x._0_<>_x_&_x._3_<>_x_holds_
not_x._4_<>_x
let x be Variable; ::_thesis: ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x & x. 0 <> x & x. 3 <> x implies not x. 4 <> x )
assume that
A9: (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> the Function of VAR,E . x and
 x. 0 <> x and
A10: x. 3 <> x and
A11: x. 4 <> x ; ::_thesis: contradiction
(( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x = ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) . x by A11, FUNCT_7:32
.= the Function of VAR,E . x by A10, FUNCT_7:32 ;
hence  contradiction by A9; ::_thesis: verum
end;
A12: ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) . (x. 3) = g . (x. 3) by FUNCT_7:128;
A13: now__::_thesis:_for_x_being_Variable_st_g_._x_<>_((_the_Function_of_VAR,E_+*_((x._3),(g_._(x._3))))_+*_((x._4),(g_._(x._4))))_._x_holds_
not_x_in_Free_H
let x be Variable; ::_thesis: ( g . x <> (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x implies not x in Free H )
assume  g . x <> (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x ; ::_thesis: not x in Free H
then  ( x. 4 <> x & x. 3 <> x ) by A12, FUNCT_7:32, FUNCT_7:128;
hence  not x in Free H by A1, TARSKI:def_2; ::_thesis: verum
end;
assume  E,g |= H ; ::_thesis: F . (g . (x. 3)) = g . (x. 4)
then  E,( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4))) |= H by A13, Th13;
then  ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 4) = g . (x. 4) & F . ((( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 3)) = (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 4) ) by A7, A8, Def1, FUNCT_7:128;
hence  F . (g . (x. 3)) = g . (x. 4) by A12, FUNCT_7:32; ::_thesis: verum
end;
assume that
A14: F . (g . (x. 3)) = g . (x. 4) and
A15: not E,g |= H ; ::_thesis: contradiction
A16: ( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) . (x. 3) = g . (x. 3) by FUNCT_7:128;
now__::_thesis:_for_x_being_Variable_st_((_the_Function_of_VAR,E_+*_((x._3),(g_._(x._3))))_+*_((x._4),(g_._(x._4))))_._x_<>_g_._x_holds_
not_x_in_Free_H
let x be Variable; ::_thesis: ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> g . x implies not x in Free H )
assume  (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . x <> g . x ; ::_thesis: not x in Free H
then  ( x. 4 <> x & x. 3 <> x ) by A16, FUNCT_7:32, FUNCT_7:128;
hence  not x in Free H by A1, TARSKI:def_2; ::_thesis: verum
end;
then  not E,( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4))) |= H by A15, Th13;
then  ( (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 4) = g . (x. 4) & F . ((( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 3)) <> (( the Function of VAR,E +* ((x. 3),(g . (x. 3)))) +* ((x. 4),(g . (x. 4)))) . (x. 4) ) by A7, A3, Def1, FUNCT_7:128;
hence  contradiction by A14, A16, FUNCT_7:32; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of E,E st ( for g being Function of VAR,E holds
( E,g |= H iff b1 . (g . (x. 3)) = g . (x. 4) ) ) & ( for g being Function of VAR,E holds
( E,g |= H iff b2 . (g . (x. 3)) = g . (x. 4) ) ) holds
b1 = b2
proof
set f = the Function of VAR,E;
let F1, F2 be Function of E,E; ::_thesis: ( ( for g being Function of VAR,E holds
( E,g |= H iff F1 . (g . (x. 3)) = g . (x. 4) ) ) & ( for g being Function of VAR,E holds
( E,g |= H iff F2 . (g . (x. 3)) = g . (x. 4) ) ) implies F1 = F2 )
assume that
A17: for g being Function of VAR,E holds
( E,g |= H iff F1 . (g . (x. 3)) = g . (x. 4) ) and
A18: for g being Function of VAR,E holds
( E,g |= H iff F2 . (g . (x. 3)) = g . (x. 4) ) ; ::_thesis: F1 = F2
let a be Element of E; :: according to FUNCT_2:def_8 ::_thesis: F1 . a = F2 . a
set g = the Function of VAR,E +* ((x. 3),a);
 E |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by A2, ZF_MODEL:23;
then  E, the Function of VAR,E +* ((x. 3),a) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by ZF_MODEL:def_5;
then consider h being Function of VAR,E such that
A19: for x being Variable st h . x <> ( the Function of VAR,E +* ((x. 3),a)) . x holds
x. 0 = x and
A20: E,h |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_MODEL:20;
A21: h . (x. 3) = ( the Function of VAR,E +* ((x. 3),a)) . (x. 3) by A19;
set j = h +* ((x. 4),(h . (x. 0)));
A22: ( ( the Function of VAR,E +* ((x. 3),a)) . (x. 3) = a & (h +* ((x. 4),(h . (x. 0)))) . (x. 3) = h . (x. 3) ) by FUNCT_7:32, FUNCT_7:128;
 ( (h +* ((x. 4),(h . (x. 0)))) . (x. 4) = h . (x. 0) & (h +* ((x. 4),(h . (x. 0)))) . (x. 0) = h . (x. 0) ) by FUNCT_7:32, FUNCT_7:128;
then A23: E,h +* ((x. 4),(h . (x. 0))) |= (x. 4) '=' (x. 0) by ZF_MODEL:12;
 for x being Variable st (h +* ((x. 4),(h . (x. 0)))) . x <> h . x holds
x. 4 = x by FUNCT_7:32;
then  E,h +* ((x. 4),(h . (x. 0))) |= H <=> ((x. 4) '=' (x. 0)) by A20, ZF_MODEL:16;
then A24: E,h +* ((x. 4),(h . (x. 0))) |= H by A23, ZF_MODEL:19;
then  F1 . ((h +* ((x. 4),(h . (x. 0)))) . (x. 3)) = (h +* ((x. 4),(h . (x. 0)))) . (x. 4) by A17;
hence  F1 . a = F2 . a by A18, A24, A22, A21; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines def_func ZFMODEL1:def_2_:_
 for H being ZF-formula
for E being non empty set st Free H c= {(x. 3),(x. 4)} & E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for b3 being Function of E,E holds
( b3 = def_func (H,E) iff for g being Function of VAR,E holds
( E,g |= H iff b3 . (g . (x. 3)) = g . (x. 4) ) );

definition
let F be Function;
let E be non empty set ;
predF is_definable_in E means :: ZFMODEL1:def 3
 ex H being ZF-formula st
( Free H c= {(x. 3),(x. 4)} & E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func (H,E) );
predF is_parametrically_definable_in E means :Def4: :: ZFMODEL1:def 4
 ex H being ZF-formula ex f being Function of VAR,E st
( {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func' (H,f) );
end;

:: deftheorem  defines is_definable_in ZFMODEL1:def_3_:_
 for F being Function
for E being non empty set holds
( F is_definable_in E iff ex H being ZF-formula st
( Free H c= {(x. 3),(x. 4)} & E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func (H,E) ) );

:: deftheorem Def4 defines is_parametrically_definable_in ZFMODEL1:def_4_:_
 for F being Function
for E being non empty set holds
( F is_parametrically_definable_in E iff ex H being ZF-formula ex f being Function of VAR,E st
( {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func' (H,f) ) );

theorem :: ZFMODEL1:14
for E being non empty set
for F being Function st F is_definable_in E holds
F is_parametrically_definable_in E
proof
let E be non empty set ; ::_thesis: for F being Function st F is_definable_in E holds
F is_parametrically_definable_in E
set f = the Function of VAR,E;
let F be Function; ::_thesis: ( F is_definable_in E implies F is_parametrically_definable_in E )
given H being ZF-formula such that A1: Free H c= {(x. 3),(x. 4)} and
A2: E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) and
A3: F = def_func (H,E) ; :: according to ZFMODEL1:def_3 ::_thesis: F is_parametrically_definable_in E
take  H ; :: according to ZFMODEL1:def_4 ::_thesis: ex f being Function of VAR,E st
( {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func' (H,f) )
take  the Function of VAR,E ; ::_thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free H & E, the Function of VAR,E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func' (H, the Function of VAR,E) )
A4: now__::_thesis:_for_a_being_set_st_a_in_{(x._0),(x._1),(x._2)}_holds_
not_a_in_Free_H
let a be set ; ::_thesis: ( a in {(x. 0),(x. 1),(x. 2)} implies not a in Free H )
assume  a in {(x. 0),(x. 1),(x. 2)} ; ::_thesis: not a in Free H
then  ( a <> x. 3 & a <> x. 4 ) by ENUMSET1:def_1;
hence  not a in Free H by A1, TARSKI:def_2; ::_thesis: verum
end;
hence  {(x. 0),(x. 1),(x. 2)} misses Free H by XBOOLE_0:3; ::_thesis: ( E, the Function of VAR,E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func' (H, the Function of VAR,E) )
thus A5: E, the Function of VAR,E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) by A2, ZF_MODEL:def_5; ::_thesis: F = def_func' (H, the Function of VAR,E)
reconsider F1 = F as Function of E,E by A3;
A6: now__::_thesis:_not_x._0_in_Free_H
assume  x. 0 in Free H ; ::_thesis: contradiction
then  not x. 0 in {(x. 0),(x. 1),(x. 2)} by A4;
hence  contradiction by ENUMSET1:def_1; ::_thesis: verum
end;
 for g being Function of VAR,E st ( for y being Variable holds
( not g . y <> the Function of VAR,E . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds
( E,g |= H iff F1 . (g . (x. 3)) = g . (x. 4) ) by A1, A2, A3, Def2;
hence  F = def_func' (H, the Function of VAR,E) by A6, A5, Def1; ::_thesis: verum
end;

theorem Th15: :: ZFMODEL1:15
for E being non empty set st E is epsilon-transitive holds
( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) iff for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E )
proof
let E be non empty set ; ::_thesis: ( E is epsilon-transitive implies ( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) iff for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E ) )
assume A1: for X being set st X in E holds
X c= E ; :: according to ORDINAL1:def_2 ::_thesis: ( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) iff for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E )
A2: now__::_thesis:_(_(_for_H_being_ZF-formula_st_{(x._0),(x._1),(x._2)}_misses_Free_H_holds_
E_|=_the_axiom_of_substitution_for_H_)_implies_for_H_being_ZF-formula
for_f_being_Function_of_VAR,E_st_{(x._0),(x._1),(x._2)}_misses_Free_H_&_E,f_|=_All_((x._3),(Ex_((x._0),(All_((x._4),(H_<=>_((x._4)_'='_(x._0))))))))_holds_
for_u_being_Element_of_E_holds_(def_func'_(H,f))_.:_u_in_E_)
assume A3: for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ; ::_thesis: for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E
let H be ZF-formula; ::_thesis: for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E
let f be Function of VAR,E; ::_thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies for u being Element of E holds (def_func' (H,f)) .: u in E )
assume that
A4: {(x. 0),(x. 1),(x. 2)} misses Free H and
A5: E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; ::_thesis: for u being Element of E holds (def_func' (H,f)) .: u in E
 E |= the_axiom_of_substitution_for H by A3, A4;
then  E,f |= the_axiom_of_substitution_for H by ZF_MODEL:def_5;
then A6: E,f |= All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H))))))))) by A5, ZF_MODEL:18;
let u be Element of E; ::_thesis: (def_func' (H,f)) .: u in E
set g = f +* ((x. 1),u);
 x. 0 in {(x. 0),(x. 1),(x. 2)} by ENUMSET1:def_1;
then A7: not x. 0 in Free H by A4, XBOOLE_0:3;
now__::_thesis:_for_a_being_set_st_a_in_{(x._1),(x._2)}_holds_
not_a_in_Free_H
let a be set ; ::_thesis: ( a in {(x. 1),(x. 2)} implies not a in Free H )
assume  a in {(x. 1),(x. 2)} ; ::_thesis: not a in Free H
then  ( a = x. 1 or a = x. 2 ) by TARSKI:def_2;
then  a in {(x. 0),(x. 1),(x. 2)} by ENUMSET1:def_1;
hence  not a in Free H by A4, XBOOLE_0:3; ::_thesis: verum
end;
then A8: {(x. 1),(x. 2)} misses Free H by XBOOLE_0:3;
 for x being Variable st (f +* ((x. 1),u)) . x <> f . x holds
x. 1 = x by FUNCT_7:32;
then  E,f +* ((x. 1),u) |= Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H))))))) by A6, ZF_MODEL:16;
then consider h being Function of VAR,E such that
A9: for x being Variable st h . x <> (f +* ((x. 1),u)) . x holds
x. 2 = x and
A10: E,h |= All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H))))) by ZF_MODEL:20;
set v = h . (x. 2);
A11: (f +* ((x. 1),u)) . (x. 1) = u by FUNCT_7:128;
A12: (def_func' (H,f)) .: u c= h . (x. 2)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (def_func' (H,f)) .: u or a in h . (x. 2) )
assume A13: a in (def_func' (H,f)) .: u ; ::_thesis: a in h . (x. 2)
then consider b being set  such that
A14: b in dom (def_func' (H,f)) and
A15: b in u and
A16: (def_func' (H,f)) . b = a by FUNCT_1:def_6;
reconsider b = b as Element of E by A14;
reconsider e = a as Element of E by A13;
set i = h +* ((x. 4),e);
set j = (h +* ((x. 4),e)) +* ((x. 3),b);
A17: ((h +* ((x. 4),e)) +* ((x. 3),b)) . (x. 3) = b by FUNCT_7:128;
A18: h . (x. 1) = (f +* ((x. 1),u)) . (x. 1) by A9;
 ( ((h +* ((x. 4),e)) +* ((x. 3),b)) . (x. 1) = (h +* ((x. 4),e)) . (x. 1) & (h +* ((x. 4),e)) . (x. 1) = h . (x. 1) ) by FUNCT_7:32;
then A19: E,(h +* ((x. 4),e)) +* ((x. 3),b) |= (x. 3) 'in' (x. 1) by A11, A15, A17, A18, ZF_MODEL:13;
set m1 = f +* ((x. 3),b);
A20: (h +* ((x. 4),e)) . (x. 4) = e by FUNCT_7:128;
set m = (f +* ((x. 3),b)) +* ((x. 4),e);
A21: (f +* ((x. 3),b)) . (x. 3) = b by FUNCT_7:128;
set k = ((f +* ((x. 3),b)) +* ((x. 4),e)) +* ((x. 1),(((h +* ((x. 4),e)) +* ((x. 3),b)) . (x. 1)));
A22: ((f +* ((x. 3),b)) +* ((x. 4),e)) . (x. 4) = e by FUNCT_7:128;
A23: ((f +* ((x. 3),b)) +* ((x. 4),e)) . (x. 3) = (f +* ((x. 3),b)) . (x. 3) by FUNCT_7:32;
A24: now__::_thesis:_for_x_being_Variable_st_((h_+*_((x._4),e))_+*_((x._3),b))_._x_<>_(((f_+*_((x._3),b))_+*_((x._4),e))_+*_((x._1),(((h_+*_((x._4),e))_+*_((x._3),b))_._(x._1))))_._x_holds_
not_x._2_<>_x
let x be Variable; ::_thesis: ( ((h +* ((x. 4),e)) +* ((x. 3),b)) . x <> (((f +* ((x. 3),b)) +* ((x. 4),e)) +* ((x. 1),(((h +* ((x. 4),e)) +* ((x. 3),b)) . (x. 1)))) . x implies not x. 2 <> x )
assume that
A25: ((h +* ((x. 4),e)) +* ((x. 3),b)) . x <> (((f +* ((x. 3),b)) +* ((x. 4),e)) +* ((x. 1),(((h +* ((x. 4),e)) +* ((x. 3),b)) . (x. 1)))) . x and
A26: x. 2 <> x ; ::_thesis: contradiction
A27: x <> x. 3 by A17, A21, A23, A25, FUNCT_7:32;
 (((f +* ((x. 3),b)) +* ((x. 4),e)) +* ((x. 1),(((h +* ((x. 4),e)) +* ((x. 3),b)) . (x. 1)))) . (x. 4) = ((f +* ((x. 3),b)) +* ((x. 4),e)) . (x. 4) by FUNCT_7:32;
then A28: x <> x. 4 by A20, A22, A25, FUNCT_7:32;
A29: x <> x. 1 by A25, FUNCT_7:128;
then (((f +* ((x. 3),b)) +* ((x. 4),e)) +* ((x. 1),(((h +* ((x. 4),e)) +* ((x. 3),b)) . (x. 1)))) . x = ((f +* ((x. 3),b)) +* ((x. 4),e)) . x by FUNCT_7:32
.= (f +* ((x. 3),b)) . x by A28, FUNCT_7:32
.= f . x by A27, FUNCT_7:32
.= (f +* ((x. 1),u)) . x by A29, FUNCT_7:32
.= h . x by A9, A26
.= (h +* ((x. 4),e)) . x by A28, FUNCT_7:32
.= ((h +* ((x. 4),e)) +* ((x. 3),b)) . x by A27, FUNCT_7:32 ;
hence  contradiction by A25; ::_thesis: verum
end;
A30: for x being Variable st (((f +* ((x. 3),b)) +* ((x. 4),e)) +* ((x. 1),(((h +* ((x. 4),e)) +* ((x. 3),b)) . (x. 1)))) . x <> ((f +* ((x. 3),b)) +* ((x. 4),e)) . x holds
x. 1 = x by FUNCT_7:32;
now__::_thesis:_for_y_being_Variable_st_((f_+*_((x._3),b))_+*_((x._4),e))_._y_<>_f_._y_&_x._0_<>_y_&_x._3_<>_y_holds_
not_x._4_<>_y
let y be Variable; ::_thesis: ( ((f +* ((x. 3),b)) +* ((x. 4),e)) . y <> f . y & x. 0 <> y & x. 3 <> y implies not x. 4 <> y )
assume A31: ((f +* ((x. 3),b)) +* ((x. 4),e)) . y <> f . y ; ::_thesis: ( x. 0 <> y & x. 3 <> y implies not x. 4 <> y )
assume that
 x. 0 <> y and
A32: x. 3 <> y and
A33: x. 4 <> y ; ::_thesis: contradiction
 ((f +* ((x. 3),b)) +* ((x. 4),e)) . y = (f +* ((x. 3),b)) . y by A33, FUNCT_7:32;
hence  contradiction by A31, A32, FUNCT_7:32; ::_thesis: verum
end;
then  ( E,(f +* ((x. 3),b)) +* ((x. 4),e) |= H iff (def_func' (H,f)) . (((f +* ((x. 3),b)) +* ((x. 4),e)) . (x. 3)) = ((f +* ((x. 3),b)) +* ((x. 4),e)) . (x. 4) ) by A5, A7, Def1;
then  E,(f +* ((x. 3),b)) +* ((x. 4),e) |= All ((x. 1),(x. 2),H) by A8, A16, A21, A22, Th11, FUNCT_7:32;
then  E,((f +* ((x. 3),b)) +* ((x. 4),e)) +* ((x. 1),(((h +* ((x. 4),e)) +* ((x. 3),b)) . (x. 1))) |= All ((x. 2),H) by A30, ZF_MODEL:16;
then  E,(h +* ((x. 4),e)) +* ((x. 3),b) |= H by A24, ZF_MODEL:16;
then A34: E,(h +* ((x. 4),e)) +* ((x. 3),b) |= ((x. 3) 'in' (x. 1)) '&' H by A19, ZF_MODEL:15;
 for x being Variable st (h +* ((x. 4),e)) . x <> h . x holds
x. 4 = x by FUNCT_7:32;
then A35: E,h +* ((x. 4),e) |= ((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H))) by A10, ZF_MODEL:16;
A36: (h +* ((x. 4),e)) . (x. 2) = h . (x. 2) by FUNCT_7:32;
 for x being Variable st (h +* ((x. 4),e)) . x <> ((h +* ((x. 4),e)) +* ((x. 3),b)) . x holds
x. 3 = x by FUNCT_7:32;
then  E,h +* ((x. 4),e) |= Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H)) by A34, ZF_MODEL:20;
then  E,h +* ((x. 4),e) |= (x. 4) 'in' (x. 2) by A35, ZF_MODEL:19;
hence  a in h . (x. 2) by A20, A36, ZF_MODEL:13; ::_thesis: verum
end;
 h . (x. 2) c= (def_func' (H,f)) .: u
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in h . (x. 2) or a in (def_func' (H,f)) .: u )
assume A37: a in h . (x. 2) ; ::_thesis: a in (def_func' (H,f)) .: u
 h . (x. 2) c= E by A1;
then reconsider e = a as Element of E by A37;
set i = h +* ((x. 4),e);
A38: (h +* ((x. 4),e)) . (x. 4) = e by FUNCT_7:128;
 for x being Variable st (h +* ((x. 4),e)) . x <> h . x holds
x. 4 = x by FUNCT_7:32;
then A39: E,h +* ((x. 4),e) |= ((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H))) by A10, ZF_MODEL:16;
 (h +* ((x. 4),e)) . (x. 2) = h . (x. 2) by FUNCT_7:32;
then  E,h +* ((x. 4),e) |= (x. 4) 'in' (x. 2) by A37, A38, ZF_MODEL:13;
then  E,h +* ((x. 4),e) |= Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H)) by A39, ZF_MODEL:19;
then consider j being Function of VAR,E such that
A40: for x being Variable st j . x <> (h +* ((x. 4),e)) . x holds
x. 3 = x and
A41: E,j |= ((x. 3) 'in' (x. 1)) '&' H by ZF_MODEL:20;
A42: j . (x. 1) = (h +* ((x. 4),e)) . (x. 1) by A40;
set m1 = f +* ((x. 3),(j . (x. 3)));
set m = (f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e);
A43: ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 4) = e by FUNCT_7:128;
set k = j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 1)));
A44: (f +* ((x. 3),(j . (x. 3)))) . (x. 3) = j . (x. 3) by FUNCT_7:128;
A45: now__::_thesis:_for_x_being_Variable_st_((f_+*_((x._3),(j_._(x._3))))_+*_((x._4),e))_._x_<>_(j_+*_((x._1),(((f_+*_((x._3),(j_._(x._3))))_+*_((x._4),e))_._(x._1))))_._x_holds_
not_x._2_<>_x
let x be Variable; ::_thesis: ( ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . x <> (j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 1)))) . x implies not x. 2 <> x )
assume that
A46: ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . x <> (j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 1)))) . x and
A47: x. 2 <> x ; ::_thesis: contradiction
 (j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 1)))) . (x. 3) = j . (x. 3) by FUNCT_7:32;
then A48: x. 3 <> x by A44, A46, FUNCT_7:32;
 (j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 1)))) . (x. 4) = j . (x. 4) by FUNCT_7:32;
then A49: x. 4 <> x by A38, A40, A43, A46;
A50: x. 1 <> x by A46, FUNCT_7:128;
then (j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 1)))) . x = j . x by FUNCT_7:32
.= (h +* ((x. 4),e)) . x by A40, A48
.= h . x by A49, FUNCT_7:32
.= (f +* ((x. 1),u)) . x by A9, A47
.= f . x by A50, FUNCT_7:32
.= (f +* ((x. 3),(j . (x. 3)))) . x by A48, FUNCT_7:32
.= ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . x by A49, FUNCT_7:32 ;
hence  contradiction by A46; ::_thesis: verum
end;
now__::_thesis:_for_y_being_Variable_st_((f_+*_((x._3),(j_._(x._3))))_+*_((x._4),e))_._y_<>_f_._y_&_x._0_<>_y_&_x._3_<>_y_holds_
not_x._4_<>_y
let y be Variable; ::_thesis: ( ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . y <> f . y & x. 0 <> y & x. 3 <> y implies not x. 4 <> y )
assume A51: ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . y <> f . y ; ::_thesis: ( x. 0 <> y & x. 3 <> y implies not x. 4 <> y )
assume that
 x. 0 <> y and
A52: x. 3 <> y and
A53: x. 4 <> y ; ::_thesis: contradiction
 ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . y = (f +* ((x. 3),(j . (x. 3)))) . y by A53, FUNCT_7:32;
hence  contradiction by A51, A52, FUNCT_7:32; ::_thesis: verum
end;
then A54: ( E,(f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e) |= H iff (def_func' (H,f)) . (((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 3)) = ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 4) ) by A5, A7, Def1;
 E,j |= (x. 3) 'in' (x. 1) by A41, ZF_MODEL:15;
then A55: j . (x. 3) in j . (x. 1) by ZF_MODEL:13;
 E,j |= H by A41, ZF_MODEL:15;
then A56: E,j |= All ((x. 1),(x. 2),H) by A8, Th11;
A57: ( (h +* ((x. 4),e)) . (x. 1) = h . (x. 1) & h . (x. 1) = (f +* ((x. 1),u)) . (x. 1) ) by A9, FUNCT_7:32;
A58: dom (def_func' (H,f)) = E by FUNCT_2:def_1;
 for x being Variable st (j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 1)))) . x <> j . x holds
x. 1 = x by FUNCT_7:32;
then  E,j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),e)) . (x. 1))) |= All ((x. 2),H) by A56, ZF_MODEL:16;
then  (def_func' (H,f)) . (j . (x. 3)) = a by A44, A43, A54, A45, FUNCT_7:32, ZF_MODEL:16;
hence  a in (def_func' (H,f)) .: u by A11, A55, A42, A57, A58, FUNCT_1:def_6; ::_thesis: verum
end;
then  (def_func' (H,f)) .: u = h . (x. 2) by A12, XBOOLE_0:def_10;
hence  (def_func' (H,f)) .: u in E ; ::_thesis: verum
end;
now__::_thesis:_(_(_for_H_being_ZF-formula
for_f_being_Function_of_VAR,E_st_{(x._0),(x._1),(x._2)}_misses_Free_H_&_E,f_|=_All_((x._3),(Ex_((x._0),(All_((x._4),(H_<=>_((x._4)_'='_(x._0))))))))_holds_
for_u_being_Element_of_E_holds_(def_func'_(H,f))_.:_u_in_E_)_implies_for_H_being_ZF-formula_st_{(x._0),(x._1),(x._2)}_misses_Free_H_holds_
E_|=_the_axiom_of_substitution_for_H_)
assume A59: for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E ; ::_thesis: for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H
let H be ZF-formula; ::_thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free H implies E |= the_axiom_of_substitution_for H )
assume A60: {(x. 0),(x. 1),(x. 2)} misses Free H ; ::_thesis: E |= the_axiom_of_substitution_for H
now__::_thesis:_for_a_being_set_st_a_in_{(x._1),(x._2)}_holds_
not_a_in_Free_H
let a be set ; ::_thesis: ( a in {(x. 1),(x. 2)} implies not a in Free H )
assume  a in {(x. 1),(x. 2)} ; ::_thesis: not a in Free H
then  ( a = x. 1 or a = x. 2 ) by TARSKI:def_2;
then  a in {(x. 0),(x. 1),(x. 2)} by ENUMSET1:def_1;
hence  not a in Free H by A60, XBOOLE_0:3; ::_thesis: verum
end;
then A61: {(x. 1),(x. 2)} misses Free H by XBOOLE_0:3;
 x. 0 in {(x. 0),(x. 1),(x. 2)} by ENUMSET1:def_1;
then A62: not x. 0 in Free H by A60, XBOOLE_0:3;
thus  E |= the_axiom_of_substitution_for H ::_thesis: verum
proof
let f be Function of VAR,E; :: according to ZF_MODEL:def_5 ::_thesis: E,f |= the_axiom_of_substitution_for H
now__::_thesis:_(_E,f_|=_All_((x._3),(Ex_((x._0),(All_((x._4),(H_<=>_((x._4)_'='_(x._0))))))))_implies_E,f_|=_All_((x._1),(Ex_((x._2),(All_((x._4),(((x._4)_'in'_(x._2))_<=>_(Ex_((x._3),(((x._3)_'in'_(x._1))_'&'_H)))))))))_)
assume A63: E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; ::_thesis: E,f |= All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H)))))))))
now__::_thesis:_for_g_being_Function_of_VAR,E_st_(_for_x_being_Variable_st_g_._x_<>_f_._x_holds_
x._1_=_x_)_holds_
E,g_|=_Ex_((x._2),(All_((x._4),(((x._4)_'in'_(x._2))_<=>_(Ex_((x._3),(((x._3)_'in'_(x._1))_'&'_H)))))))
let g be Function of VAR,E; ::_thesis: ( ( for x being Variable st g . x <> f . x holds
x. 1 = x ) implies E,g |= Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H))))))) )
assume A64: for x being Variable st g . x <> f . x holds
x. 1 = x ; ::_thesis: E,g |= Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H)))))))
reconsider v = (def_func' (H,f)) .: (g . (x. 1)) as Element of E by A59, A60, A63;
set h = g +* ((x. 2),v);
A65: (g +* ((x. 2),v)) . (x. 2) = v by FUNCT_7:128;
now__::_thesis:_for_i_being_Function_of_VAR,E_st_(_for_x_being_Variable_st_i_._x_<>_(g_+*_((x._2),v))_._x_holds_
x._4_=_x_)_holds_
E,i_|=_((x._4)_'in'_(x._2))_<=>_(Ex_((x._3),(((x._3)_'in'_(x._1))_'&'_H)))
let i be Function of VAR,E; ::_thesis: ( ( for x being Variable st i . x <> (g +* ((x. 2),v)) . x holds
x. 4 = x ) implies E,i |= ((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H))) )
assume A66: for x being Variable st i . x <> (g +* ((x. 2),v)) . x holds
x. 4 = x ; ::_thesis: E,i |= ((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H)))
A67: now__::_thesis:_(_E,i_|=_(x._4)_'in'_(x._2)_implies_E,i_|=_Ex_((x._3),(((x._3)_'in'_(x._1))_'&'_H))_)
assume  E,i |= (x. 4) 'in' (x. 2) ; ::_thesis: E,i |= Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H))
then A68: i . (x. 4) in i . (x. 2) by ZF_MODEL:13;
 i . (x. 2) = (g +* ((x. 2),v)) . (x. 2) by A66;
then consider a being set  such that
A69: a in dom (def_func' (H,f)) and
A70: a in g . (x. 1) and
A71: i . (x. 4) = (def_func' (H,f)) . a by A65, A68, FUNCT_1:def_6;
reconsider a = a as Element of E by A69;
set j = i +* ((x. 3),a);
A72: (i +* ((x. 3),a)) . (x. 3) = a by FUNCT_7:128;
set m1 = f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)));
set m = (f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)));
A73: ((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 4) = i . (x. 4) by FUNCT_7:128;
set k = ((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) +* ((x. 1),((i +* ((x. 3),a)) . (x. 1)));
A74: (f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) . (x. 3) = (i +* ((x. 3),a)) . (x. 3) by FUNCT_7:128;
A75: now__::_thesis:_for_x_being_Variable_st_(i_+*_((x._3),a))_._x_<>_(((f_+*_((x._3),((i_+*_((x._3),a))_._(x._3))))_+*_((x._4),(i_._(x._4))))_+*_((x._1),((i_+*_((x._3),a))_._(x._1))))_._x_holds_
not_x._2_<>_x
let x be Variable; ::_thesis: ( (i +* ((x. 3),a)) . x <> (((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) +* ((x. 1),((i +* ((x. 3),a)) . (x. 1)))) . x implies not x. 2 <> x )
assume that
A76: (i +* ((x. 3),a)) . x <> (((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) +* ((x. 1),((i +* ((x. 3),a)) . (x. 1)))) . x and
A77: x. 2 <> x ; ::_thesis: contradiction
A78: x. 1 <> x by A76, FUNCT_7:128;
 (i +* ((x. 3),a)) . (x. 4) = i . (x. 4) by FUNCT_7:32;
then A79: x. 4 <> x by A73, A76, FUNCT_7:32;
 (((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) +* ((x. 1),((i +* ((x. 3),a)) . (x. 1)))) . (x. 3) = ((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 3) by FUNCT_7:32;
then A80: x. 3 <> x by A74, A76, FUNCT_7:32;
then (i +* ((x. 3),a)) . x = i . x by FUNCT_7:32
.= (g +* ((x. 2),v)) . x by A66, A79
.= g . x by A77, FUNCT_7:32
.= f . x by A64, A78
.= (f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) . x by A80, FUNCT_7:32
.= ((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . x by A79, FUNCT_7:32
.= (((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) +* ((x. 1),((i +* ((x. 3),a)) . (x. 1)))) . x by A78, FUNCT_7:32 ;
hence  contradiction by A76; ::_thesis: verum
end;
A81: for x being Variable st (((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) +* ((x. 1),((i +* ((x. 3),a)) . (x. 1)))) . x <> ((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . x holds
x. 1 = x by FUNCT_7:32;
now__::_thesis:_for_x_being_Variable_st_((f_+*_((x._3),((i_+*_((x._3),a))_._(x._3))))_+*_((x._4),(i_._(x._4))))_._x_<>_f_._x_&_x._0_<>_x_&_x._3_<>_x_holds_
not_x._4_<>_x
let x be Variable; ::_thesis: ( ((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . x <> f . x & x. 0 <> x & x. 3 <> x implies not x. 4 <> x )
assume that
A82: ((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . x <> f . x and
 x. 0 <> x and
A83: x. 3 <> x and
A84: x. 4 <> x ; ::_thesis: contradiction
 ((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . x = (f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) . x by A84, FUNCT_7:32;
hence  contradiction by A82, A83, FUNCT_7:32; ::_thesis: verum
end;
then  ( E,(f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4))) |= H iff (def_func' (H,f)) . (((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 3)) = ((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 4) ) by A62, A63, Def1;
then  E,(f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4))) |= All ((x. 1),(x. 2),H) by A61, A71, A72, A74, A73, Th11, FUNCT_7:32;
then  E,((f +* ((x. 3),((i +* ((x. 3),a)) . (x. 3)))) +* ((x. 4),(i . (x. 4)))) +* ((x. 1),((i +* ((x. 3),a)) . (x. 1))) |= All ((x. 2),H) by A81, ZF_MODEL:16;
then A85: E,i +* ((x. 3),a) |= H by A75, ZF_MODEL:16;
A86: (g +* ((x. 2),v)) . (x. 1) = g . (x. 1) by FUNCT_7:32;
 ( (i +* ((x. 3),a)) . (x. 1) = i . (x. 1) & i . (x. 1) = (g +* ((x. 2),v)) . (x. 1) ) by A66, FUNCT_7:32;
then  E,i +* ((x. 3),a) |= (x. 3) 'in' (x. 1) by A70, A72, A86, ZF_MODEL:13;
then A87: E,i +* ((x. 3),a) |= ((x. 3) 'in' (x. 1)) '&' H by A85, ZF_MODEL:15;
 for x being Variable st (i +* ((x. 3),a)) . x <> i . x holds
x. 3 = x by FUNCT_7:32;
hence  E,i |= Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H)) by A87, ZF_MODEL:20; ::_thesis: verum
end;
now__::_thesis:_(_E,i_|=_Ex_((x._3),(((x._3)_'in'_(x._1))_'&'_H))_implies_E,i_|=_(x._4)_'in'_(x._2)_)
assume  E,i |= Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H)) ; ::_thesis: E,i |= (x. 4) 'in' (x. 2)
then consider j being Function of VAR,E such that
A88: for x being Variable st j . x <> i . x holds
x. 3 = x and
A89: E,j |= ((x. 3) 'in' (x. 1)) '&' H by ZF_MODEL:20;
set m1 = f +* ((x. 3),(j . (x. 3)));
set m = (f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)));
A90: ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 4) = i . (x. 4) by FUNCT_7:128;
set k = j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 1)));
A91: (f +* ((x. 3),(j . (x. 3)))) . (x. 3) = j . (x. 3) by FUNCT_7:128;
A92: now__::_thesis:_for_x_being_Variable_st_((f_+*_((x._3),(j_._(x._3))))_+*_((x._4),(i_._(x._4))))_._x_<>_(j_+*_((x._1),(((f_+*_((x._3),(j_._(x._3))))_+*_((x._4),(i_._(x._4))))_._(x._1))))_._x_holds_
not_x._2_<>_x
let x be Variable; ::_thesis: ( ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . x <> (j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 1)))) . x implies not x. 2 <> x )
assume that
A93: ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . x <> (j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 1)))) . x and
A94: x. 2 <> x ; ::_thesis: contradiction
A95: x. 1 <> x by A93, FUNCT_7:128;
 ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 3) = (f +* ((x. 3),(j . (x. 3)))) . (x. 3) by FUNCT_7:32;
then A96: x. 3 <> x by A91, A93, FUNCT_7:32;
 (j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 1)))) . (x. 4) = j . (x. 4) by FUNCT_7:32;
then A97: x. 4 <> x by A88, A90, A93;
then ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . x = (f +* ((x. 3),(j . (x. 3)))) . x by FUNCT_7:32
.= f . x by A96, FUNCT_7:32
.= g . x by A64, A95
.= (g +* ((x. 2),v)) . x by A94, FUNCT_7:32
.= i . x by A66, A97
.= j . x by A88, A96
.= (j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 1)))) . x by A95, FUNCT_7:32 ;
hence  contradiction by A93; ::_thesis: verum
end;
A98: i . (x. 2) = (g +* ((x. 2),v)) . (x. 2) by A66;
A99: ( (g +* ((x. 2),v)) . (x. 1) = g . (x. 1) & dom (def_func' (H,f)) = E ) by FUNCT_2:def_1, FUNCT_7:32;
 E,j |= (x. 3) 'in' (x. 1) by A89, ZF_MODEL:15;
then A100: j . (x. 3) in j . (x. 1) by ZF_MODEL:13;
A101: now__::_thesis:_for_x_being_Variable_st_((f_+*_((x._3),(j_._(x._3))))_+*_((x._4),(i_._(x._4))))_._x_<>_f_._x_&_x._0_<>_x_&_x._3_<>_x_holds_
not_x._4_<>_x
let x be Variable; ::_thesis: ( ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . x <> f . x & x. 0 <> x & x. 3 <> x implies not x. 4 <> x )
assume that
A102: ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . x <> f . x and
 x. 0 <> x and
A103: x. 3 <> x and
A104: x. 4 <> x ; ::_thesis: contradiction
f . x = (f +* ((x. 3),(j . (x. 3)))) . x by A103, FUNCT_7:32
.= ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . x by A104, FUNCT_7:32 ;
hence  contradiction by A102; ::_thesis: verum
end;
 E,j |= H by A89, ZF_MODEL:15;
then A105: E,j |= All ((x. 1),(x. 2),H) by A61, Th11;
A106: ( ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 3) = (f +* ((x. 3),(j . (x. 3)))) . (x. 3) & i . (x. 1) = (g +* ((x. 2),v)) . (x. 1) ) by A66, FUNCT_7:32;
 for x being Variable st (j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 1)))) . x <> j . x holds
x. 1 = x by FUNCT_7:32;
then  E,j +* ((x. 1),(((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 1))) |= All ((x. 2),H) by A105, ZF_MODEL:16;
then  E,(f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4))) |= H by A92, ZF_MODEL:16;
then A107: (def_func' (H,f)) . (((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 3)) = ((f +* ((x. 3),(j . (x. 3)))) +* ((x. 4),(i . (x. 4)))) . (x. 4) by A62, A63, A101, Def1;
 j . (x. 1) = i . (x. 1) by A88;
then  i . (x. 4) in (def_func' (H,f)) .: (g . (x. 1)) by A91, A90, A107, A100, A106, A99, FUNCT_1:def_6;
hence  E,i |= (x. 4) 'in' (x. 2) by A65, A98, ZF_MODEL:13; ::_thesis: verum
end;
hence  E,i |= ((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H))) by A67, ZF_MODEL:19; ::_thesis: verum
end;
then A108: E,g +* ((x. 2),v) |= All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H))))) by ZF_MODEL:16;
 for x being Variable st (g +* ((x. 2),v)) . x <> g . x holds
x. 2 = x by FUNCT_7:32;
hence  E,g |= Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H))))))) by A108, ZF_MODEL:20; ::_thesis: verum
end;
hence  E,f |= All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H))))))))) by ZF_MODEL:16; ::_thesis: verum
end;
hence  E,f |= the_axiom_of_substitution_for H by ZF_MODEL:18; ::_thesis: verum
end;
end;
hence  ( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) iff for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E ) by A2; ::_thesis: verum
end;

theorem :: ZFMODEL1:16
for E being non empty set st E is epsilon-transitive holds
( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) iff for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E )
proof
let E be non empty set ; ::_thesis: ( E is epsilon-transitive implies ( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) iff for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E ) )
assume A1: E is epsilon-transitive ; ::_thesis: ( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) iff for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E )
thus  ( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) implies for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E ) ::_thesis: ( ( for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E ) implies for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H )
proof
assume A2: for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ; ::_thesis: for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E
let F be Function; ::_thesis: ( F is_parametrically_definable_in E implies for X being set st X in E holds
F .: X in E )
given H being ZF-formula, f being Function of VAR,E such that A3: ( {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ) and
A4: F = def_func' (H,f) ; :: according to ZFMODEL1:def_4 ::_thesis: for X being set st X in E holds
F .: X in E
let X be set ; ::_thesis: ( X in E implies F .: X in E )
assume  X in E ; ::_thesis: F .: X in E
then reconsider u = X as Element of E ;
 (def_func' (H,f)) .: u in E by A1, A2, A3, Th15;
hence  F .: X in E by A4; ::_thesis: verum
end;
assume A5: for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E ; ::_thesis: for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H
 for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E
proof
let H be ZF-formula; ::_thesis: for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E
let f be Function of VAR,E; ::_thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies for u being Element of E holds (def_func' (H,f)) .: u in E )
assume A6: ( {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ) ; ::_thesis: for u being Element of E holds (def_func' (H,f)) .: u in E
let u be Element of E; ::_thesis: (def_func' (H,f)) .: u in E
 def_func' (H,f) is_parametrically_definable_in E by A6, Def4;
hence  (def_func' (H,f)) .: u in E by A5; ::_thesis: verum
end;
hence  for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H by A1, Th15; ::_thesis: verum
end;

Lm3:  for E being non empty set st E is epsilon-transitive holds
for u, v being Element of E st ( for w being Element of E holds
( w in u iff w in v ) ) holds
u = v
proof
let E be non empty set ; ::_thesis: ( E is epsilon-transitive implies for u, v being Element of E st ( for w being Element of E holds
( w in u iff w in v ) ) holds
u = v )
assume A1: for X being set st X in E holds
X c= E ; :: according to ORDINAL1:def_2 ::_thesis: for u, v being Element of E st ( for w being Element of E holds
( w in u iff w in v ) ) holds
u = v
let u, v be Element of E; ::_thesis: ( ( for w being Element of E holds
( w in u iff w in v ) ) implies u = v )
assume A2: for w being Element of E holds
( w in u iff w in v ) ; ::_thesis: u = v
A3: u c= E by A1;
thus  u c= v :: according to XBOOLE_0:def_10 ::_thesis: v c= u
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in u or a in v )
assume A4: a in u ; ::_thesis: a in v
then reconsider e = a as Element of E by A3;
 e in v by A2, A4;
hence  a in v ; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in v or a in u )
assume A5: a in v ; ::_thesis: a in u
 v c= E by A1;
then reconsider e = a as Element of E by A5;
 e in u by A2, A5;
hence  a in u ; ::_thesis: verum
end;

theorem :: ZFMODEL1:17
for E being non empty set st E is being_a_model_of_ZF holds
( E is epsilon-transitive & ( for u, v being Element of E st ( for w being Element of E holds
( w in u iff w in v ) ) holds
u = v ) & ( for u, v being Element of E holds {u,v} in E ) & ( for u being Element of E holds union u in E ) & ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) & ( for u being Element of E holds E /\ (bool u) in E ) & ( for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E ) )
proof
let E be non empty set ; ::_thesis: ( E is being_a_model_of_ZF implies ( E is epsilon-transitive & ( for u, v being Element of E st ( for w being Element of E holds
( w in u iff w in v ) ) holds
u = v ) & ( for u, v being Element of E holds {u,v} in E ) & ( for u being Element of E holds union u in E ) & ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) & ( for u being Element of E holds E /\ (bool u) in E ) & ( for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E ) ) )
assume  ( E is epsilon-transitive & E |= the_axiom_of_pairs & E |= the_axiom_of_unions & E |= the_axiom_of_infinity & E |= the_axiom_of_power_sets & ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) ) ; :: according to ZF_MODEL:def_12 ::_thesis: ( E is epsilon-transitive & ( for u, v being Element of E st ( for w being Element of E holds
( w in u iff w in v ) ) holds
u = v ) & ( for u, v being Element of E holds {u,v} in E ) & ( for u being Element of E holds union u in E ) & ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) & ( for u being Element of E holds E /\ (bool u) in E ) & ( for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E ) )
hence  ( E is epsilon-transitive & ( for u, v being Element of E st ( for w being Element of E holds
( w in u iff w in v ) ) holds
u = v ) & ( for u, v being Element of E holds {u,v} in E ) & ( for u being Element of E holds union u in E ) & ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) & ( for u being Element of E holds E /\ (bool u) in E ) & ( for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E ) ) by Lm3, Th2, Th4, Th6, Th8, Th15; ::_thesis: verum
end;

theorem :: ZFMODEL1:18
for E being non empty set st E is epsilon-transitive & ( for u, v being Element of E holds {u,v} in E ) & ( for u being Element of E holds union u in E ) & ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) & ( for u being Element of E holds E /\ (bool u) in E ) & ( for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E ) holds
E is being_a_model_of_ZF
proof
let E be non empty set ; ::_thesis: ( E is epsilon-transitive & ( for u, v being Element of E holds {u,v} in E ) & ( for u being Element of E holds union u in E ) & ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) & ( for u being Element of E holds E /\ (bool u) in E ) & ( for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E ) implies E is being_a_model_of_ZF )
assume  ( E is epsilon-transitive & ( for u, v being Element of E holds {u,v} in E ) & ( for u being Element of E holds union u in E ) & ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) & ( for u being Element of E holds E /\ (bool u) in E ) & ( for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E ) ) ; ::_thesis: E is being_a_model_of_ZF
hence  ( E is epsilon-transitive & E |= the_axiom_of_pairs & E |= the_axiom_of_unions & E |= the_axiom_of_infinity & E |= the_axiom_of_power_sets & ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) ) by Th2, Th4, Th6, Th8, Th15; :: according to ZF_MODEL:def_12 ::_thesis: verum
end;