:: ZFMODEL1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

set x0 = x. 0;

set x1 = x. 1;

set x2 = x. 2;

set x3 = x. 3;

set x4 = x. 4;

theorem :: ZFMODEL1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set st E is epsilon-transitive holds
E |= the_axiom_of_extensionality
proof end;

theorem Th2: :: ZFMODEL1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: ZFMODEL1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th4: :: ZFMODEL1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: ZFMODEL1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th6: :: ZFMODEL1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: ZFMODEL1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th8: :: ZFMODEL1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: ZFMODEL1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 end;

theorem Th10: :: ZFMODEL1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 end;

theorem Th11: :: ZFMODEL1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: ZFMODEL1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let H be ZF-formula;
let E be non empty set ;
let val be Function of VAR ,E;
assume A1: ( not x. 0 in Free H & 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 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 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 :: ZFMODEL1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th14: :: ZFMODEL1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let H be ZF-formula;
let E be non empty set ;
assume A1: ( Free H c= {(x. 3),(x. 4)} & 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 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 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 ;
pred F 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 );
pred F 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:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ZFMODEL1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ZFMODEL1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ZFMODEL1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set
for F being Function st F is_definable_in E holds
F is_parametrically_definable_in E
proof end;

theorem Th19: :: ZFMODEL1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: ZFMODEL1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 end;

theorem :: ZFMODEL1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set st E is_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 end;

theorem :: ZFMODEL1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_a_model_of_ZF
proof end;