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

scheme :: ZF_MODEL:sch 1
ZFschex{ F1( Variable, Variable) -> set , F2( Variable, Variable) -> set , F3( set ) -> set , F4( set , set ) -> set , F5( Variable, set ) -> set , F6() -> ZF-formula } :
ex a, A being set st
( ( for x, y being Variable holds
( [(x '=' y),F1(x,y)] in A & [(x 'in' y),F2(x,y)] in A ) ) & [F6(),a] in A & ( for H being ZF-formula
for a being set st [H,a] in A holds
( ( H is_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st
( a = F3(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) )
proof end;

scheme :: ZF_MODEL:sch 2
ZFschuniq{ F1( Variable, Variable) -> set , F2( Variable, Variable) -> set , F3( set ) -> set , F4( set , set ) -> set , F5( Variable, set ) -> set , F6() -> ZF-formula, F7() -> set , F8() -> set } :
F7() = F8()
provided
A1: ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),F1(x,y)] in A & [(x 'in' y),F2(x,y)] in A ) ) & [F6(),F7()] in A & ( for H being ZF-formula
for a being set st [H,a] in A holds
( ( H is_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st
( a = F3(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) ) and
A2: ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),F1(x,y)] in A & [(x 'in' y),F2(x,y)] in A ) ) & [F6(),F8()] in A & ( for H being ZF-formula
for a being set st [H,a] in A holds
( ( H is_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st
( a = F3(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) )
proof end;

scheme :: ZF_MODEL:sch 3
ZFschresult{ F1( Variable, Variable) -> set , F2( Variable, Variable) -> set , F3( set ) -> set , F4( set , set ) -> set , F5( Variable, set ) -> set , F6() -> ZF-formula, F7( ZF-formula) -> set } :
( ( F6() is_equality implies F7(F6()) = F1((Var1 F6()),(Var2 F6())) ) & ( F6() is_membership implies F7(F6()) = F2((Var1 F6()),(Var2 F6())) ) & ( F6() is negative implies F7(F6()) = F3(F7((the_argument_of F6()))) ) & ( F6() is conjunctive implies for a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds
F7(F6()) = F4(a,b) ) & ( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) ) )
provided
A1: for H' being ZF-formula
for a being set holds
( a = F7(H') iff ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),F1(x,y)] in A & [(x 'in' y),F2(x,y)] in A ) ) & [H',a] in A & ( for H being ZF-formula
for a being set st [H,a] in A holds
( ( H is_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st
( a = F3(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) ) )
proof end;

scheme :: ZF_MODEL:sch 4
ZFschproperty{ F1( Variable, Variable) -> set , F2( Variable, Variable) -> set , F3( set ) -> set , F4( set , set ) -> set , F5( Variable, set ) -> set , F6( ZF-formula) -> set , F7() -> ZF-formula, P1[ set ] } :
P1[F6(F7())]
provided
A1: for H' being ZF-formula
for a being set holds
( a = F6(H') iff ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),F1(x,y)] in A & [(x 'in' y),F2(x,y)] in A ) ) & [H',a] in A & ( for H being ZF-formula
for a being set st [H,a] in A holds
( ( H is_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st
( a = F3(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) ) ) and
A2: for x, y being Variable holds
( P1[F1(x,y)] & P1[F2(x,y)] ) and
A3: for a being set st P1[a] holds
P1[F3(a)] and
A4: for a, b being set st P1[a] & P1[b] holds
P1[F4(a,b)] and
A5: for a being set
for x being Variable st P1[a] holds
P1[F5(x,a)]
proof end;

deffunc H1( Variable, Variable) -> set = {$1,$2};

deffunc H2( Variable, Variable) -> set = {$1,$2};

deffunc H3( set ) -> set = $1;

deffunc H4( set , set ) -> set = union {$1,$2};

deffunc H5( Variable, set ) -> set = (union {$2}) \ {$1};

definition
let H be ZF-formula;
func Free H -> set means :Def1: :: ZF_MODEL:def 1
ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,it] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = {(Var1 H'),(Var2 H')} ) & ( H' is_membership implies a = {(Var1 H'),(Var2 H')} ) & ( H' is negative implies ex b being set st
( a = b & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = union {b,c} & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = (union {b}) \ {(bound_in H')} & [(the_scope_of H'),b] in A ) ) ) ) );
existence
ex b1, A being set st
( ( for x, y being Variable holds
( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b1] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = {(Var1 H'),(Var2 H')} ) & ( H' is_membership implies a = {(Var1 H'),(Var2 H')} ) & ( H' is negative implies ex b being set st
( a = b & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = union {b,c} & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = (union {b}) \ {(bound_in H')} & [(the_scope_of H'),b] in A ) ) ) ) )
proof end;
uniqueness
for b1, b2 being set st ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b1] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = {(Var1 H'),(Var2 H')} ) & ( H' is_membership implies a = {(Var1 H'),(Var2 H')} ) & ( H' is negative implies ex b being set st
( a = b & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = union {b,c} & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = (union {b}) \ {(bound_in H')} & [(the_scope_of H'),b] in A ) ) ) ) ) & ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b2] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = {(Var1 H'),(Var2 H')} ) & ( H' is_membership implies a = {(Var1 H'),(Var2 H')} ) & ( H' is negative implies ex b being set st
( a = b & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = union {b,c} & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = (union {b}) \ {(bound_in H')} & [(the_scope_of H'),b] in A ) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Free ZF_MODEL:def 1 :
for H being ZF-formula
for b2 being set holds
( b2 = Free H iff ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b2] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = {(Var1 H'),(Var2 H')} ) & ( H' is_membership implies a = {(Var1 H'),(Var2 H')} ) & ( H' is negative implies ex b being set st
( a = b & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = union {b,c} & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = (union {b}) \ {(bound_in H')} & [(the_scope_of H'),b] in A ) ) ) ) ) );

deffunc H6( ZF-formula) -> set = Free $1;

Lm1: for H being ZF-formula
for a1 being set holds
( a1 = H6(H) iff ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),H1(x,y)] in A & [(x 'in' y),H2(x,y)] in A ) ) & [H,a1] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = H1( Var1 H', Var2 H') ) & ( H' is_membership implies a = H2( Var1 H', Var2 H') ) & ( H' is negative implies ex b being set st
( a = H3(b) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = H4(b,c) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = H5( bound_in H',b) & [(the_scope_of H'),b] in A ) ) ) ) ) )
by Def1;

Lm2: now
let H be ZF-formula; :: thesis: ( ( H is_equality implies H6(H) = H1( Var1 H, Var2 H) ) & ( H is_membership implies H6(H) = H2( Var1 H, Var2 H) ) & ( H is negative implies H6(H) = H3(H6( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H6( the_left_argument_of H) & b = H6( the_right_argument_of H) holds
H6(H) = H4(a,b) ) & ( H is universal implies H6(H) = H5( bound_in H,H6( the_scope_of H)) ) )

thus ( ( H is_equality implies H6(H) = H1( Var1 H, Var2 H) ) & ( H is_membership implies H6(H) = H2( Var1 H, Var2 H) ) & ( H is negative implies H6(H) = H3(H6( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H6( the_left_argument_of H) & b = H6( the_right_argument_of H) holds
H6(H) = H4(a,b) ) & ( H is universal implies H6(H) = H5( bound_in H,H6( the_scope_of H)) ) ) from ZF_MODEL:sch 3( E , Lm1); :: thesis: verum
end;

definition
let H be ZF-formula;
:: original: Free
redefine func Free H -> Subset of VAR ;
coherence
Free H is Subset of VAR
proof end;
end;

theorem :: ZF_MODEL:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being ZF-formula holds
( ( H is_equality implies Free H = {(Var1 H),(Var2 H)} ) & ( H is_membership implies Free H = {(Var1 H),(Var2 H)} ) & ( H is negative implies Free H = Free (the_argument_of H) ) & ( H is conjunctive implies Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H)) ) & ( H is universal implies Free H = (Free (the_scope_of H)) \ {(bound_in H)} ) )
proof end;

definition
let D be non empty set ;
func VAL D -> set means :Def2: :: ZF_MODEL:def 2
for a being set holds
( a in it iff a is Function of VAR ,D );
existence
ex b1 being set st
for a being set holds
( a in b1 iff a is Function of VAR ,D )
proof end;
uniqueness
for b1, b2 being set st ( for a being set holds
( a in b1 iff a is Function of VAR ,D ) ) & ( for a being set holds
( a in b2 iff a is Function of VAR ,D ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines VAL ZF_MODEL:def 2 :
for D being non empty set
for b2 being set holds
( b2 = VAL D iff for a being set holds
( a in b2 iff a is Function of VAR ,D ) );

registration
let D be non empty set ;
cluster VAL D -> non empty ;
coherence
not VAL D is empty
proof end;
end;

definition
let H be ZF-formula;
let E be non empty set ;
deffunc H7( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . $1 = f . $2
}
;
deffunc H8( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . $1 in f . $2
}
;
deffunc H9( set ) -> set = (VAL E) \ (union {$1});
deffunc H10( set , set ) -> set = (union {$1}) /\ (union {$2});
deffunc H11( Variable, set ) -> set = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = $2 & f = v5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
$1 = y ) holds
g in X ) )
}
;
func St H,E -> set means :Def3: :: ZF_MODEL:def 3
ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{ v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y
}
]
in A & [(x 'in' y),{ v2 where v2 is Element of VAL E : for f being Function of VAR ,E st f = v2 holds
f . x in f . y
}
]
in A ) ) & [H,it] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . (Var1 H') = f . (Var2 H')
}
) & ( H' is_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR ,E st f = v4 holds
f . (Var1 H') in f . (Var2 H')
}
) & ( H' is negative implies ex b being set st
( a = (VAL E) \ (union {b}) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = b & f = v5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
bound_in H' = y ) holds
g in X ) )
}
& [(the_scope_of H'),b] in A ) ) ) ) );
existence
ex b1, A being set st
( ( for x, y being Variable holds
( [(x '=' y),{ v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y
}
]
in A & [(x 'in' y),{ v2 where v2 is Element of VAL E : for f being Function of VAR ,E st f = v2 holds
f . x in f . y
}
]
in A ) ) & [H,b1] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . (Var1 H') = f . (Var2 H')
}
) & ( H' is_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR ,E st f = v4 holds
f . (Var1 H') in f . (Var2 H')
}
) & ( H' is negative implies ex b being set st
( a = (VAL E) \ (union {b}) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = b & f = v5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
bound_in H' = y ) holds
g in X ) )
}
& [(the_scope_of H'),b] in A ) ) ) ) )
proof end;
uniqueness
for b1, b2 being set st ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{ v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y
}
]
in A & [(x 'in' y),{ v2 where v2 is Element of VAL E : for f being Function of VAR ,E st f = v2 holds
f . x in f . y
}
]
in A ) ) & [H,b1] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . (Var1 H') = f . (Var2 H')
}
) & ( H' is_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR ,E st f = v4 holds
f . (Var1 H') in f . (Var2 H')
}
) & ( H' is negative implies ex b being set st
( a = (VAL E) \ (union {b}) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = b & f = v5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
bound_in H' = y ) holds
g in X ) )
}
& [(the_scope_of H'),b] in A ) ) ) ) ) & ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{ v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y
}
]
in A & [(x 'in' y),{ v2 where v2 is Element of VAL E : for f being Function of VAR ,E st f = v2 holds
f . x in f . y
}
]
in A ) ) & [H,b2] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . (Var1 H') = f . (Var2 H')
}
) & ( H' is_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR ,E st f = v4 holds
f . (Var1 H') in f . (Var2 H')
}
) & ( H' is negative implies ex b being set st
( a = (VAL E) \ (union {b}) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = b & f = v5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
bound_in H' = y ) holds
g in X ) )
}
& [(the_scope_of H'),b] in A ) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines St ZF_MODEL:def 3 :
for H being ZF-formula
for E being non empty set
for b3 being set holds
( b3 = St H,E iff ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{ v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . x = f . y
}
]
in A & [(x 'in' y),{ v2 where v2 is Element of VAL E : for f being Function of VAR ,E st f = v2 holds
f . x in f . y
}
]
in A ) ) & [H,b3] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . (Var1 H') = f . (Var2 H')
}
) & ( H' is_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR ,E st f = v4 holds
f . (Var1 H') in f . (Var2 H')
}
) & ( H' is negative implies ex b being set st
( a = (VAL E) \ (union {b}) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = b & f = v5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
bound_in H' = y ) holds
g in X ) )
}
& [(the_scope_of H'),b] in A ) ) ) ) ) );

Lm3: now
let H be ZF-formula; :: thesis: for E being non empty set holds
( ( H is_equality implies H12(H) = H7( Var1 H, Var2 H) ) & ( H is_membership implies H12(H) = H8( Var1 H, Var2 H) ) & ( H is negative implies H12(H) = H9(H12( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H12( the_left_argument_of H) & b = H12( the_right_argument_of H) holds
H12(H) = H10(a,b) ) & ( H is universal implies H12(H) = H11( bound_in H,H12( the_scope_of H)) ) )

let E be non empty set ; :: thesis: ( ( H is_equality implies H12(H) = H7( Var1 H, Var2 H) ) & ( H is_membership implies H12(H) = H8( Var1 H, Var2 H) ) & ( H is negative implies H12(H) = H9(H12( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H12( the_left_argument_of H) & b = H12( the_right_argument_of H) holds
H12(H) = H10(a,b) ) & ( H is universal implies H12(H) = H11( bound_in H,H12( the_scope_of H)) ) )

deffunc H7( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . $1 = f . $2
}
;
deffunc H8( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR ,E st f = v3 holds
f . $1 in f . $2
}
;
deffunc H9( set ) -> set = (VAL E) \ (union {$1});
deffunc H10( set , set ) -> set = (union {$1}) /\ (union {$2});
deffunc H11( Variable, set ) -> set = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR ,E st X = $2 & f = v5 holds
( f in X & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
$1 = y ) holds
g in X ) )
}
;
deffunc H12( ZF-formula) -> set = St $1,E;
A1: for H being ZF-formula
for a being set holds
( a = H12(H) iff ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),H7(x,y)] in A & [(x 'in' y),H8(x,y)] in A ) ) & [H,a] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is_equality implies a = H7( Var1 H', Var2 H') ) & ( H' is_membership implies a = H8( Var1 H', Var2 H') ) & ( H' is negative implies ex b being set st
( a = H9(b) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = H10(b,c) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = H11( bound_in H',b) & [(the_scope_of H'),b] in A ) ) ) ) ) ) by Def3;
thus ( ( H is_equality implies H12(H) = H7( Var1 H, Var2 H) ) & ( H is_membership implies H12(H) = H8( Var1 H, Var2 H) ) & ( H is negative implies H12(H) = H9(H12( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H12( the_left_argument_of H) & b = H12( the_right_argument_of H) holds
H12(H) = H10(a,b) ) & ( H is universal implies H12(H) = H11( bound_in H,H12( the_scope_of H)) ) ) from ZF_MODEL:sch 3( E , A1); :: thesis: verum
end;

definition
let H be ZF-formula;
let E be non empty set ;
:: original: St
redefine func St H,E -> Subset of (VAL E);
coherence
St H,E is Subset of (VAL E)
proof end;
end;

theorem Th2: :: ZF_MODEL: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
for x, y being Variable
for f being Function of VAR ,E holds
( f . x = f . y iff f in St (x '=' y),E )
proof end;

theorem Th3: :: ZF_MODEL: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
for x, y being Variable
for f being Function of VAR ,E holds
( f . x in f . y iff f in St (x 'in' y),E )
proof end;

theorem Th4: :: ZF_MODEL: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
for H being ZF-formula
for f being Function of VAR ,E holds
( not f in St H,E iff f in St ('not' H),E )
proof end;

theorem Th5: :: ZF_MODEL: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
for H, H' being ZF-formula
for f being Function of VAR ,E holds
( ( f in St H,E & f in St H',E ) iff f in St (H '&' H'),E )
proof end;

theorem Th6: :: ZF_MODEL: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
for x being Variable
for H being ZF-formula
for f being Function of VAR ,E holds
( ( f in St H,E & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in St H,E ) ) iff f in St (All x,H),E )
proof end;

theorem :: ZF_MODEL:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being ZF-formula
for E being non empty set st H is_equality holds
for f being Function of VAR ,E holds
( f . (Var1 H) = f . (Var2 H) iff f in St H,E )
proof end;

theorem :: ZF_MODEL:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being ZF-formula
for E being non empty set st H is_membership holds
for f being Function of VAR ,E holds
( f . (Var1 H) in f . (Var2 H) iff f in St H,E )
proof end;

theorem :: ZF_MODEL:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being ZF-formula
for E being non empty set st H is negative holds
for f being Function of VAR ,E holds
( not f in St (the_argument_of H),E iff f in St H,E )
proof end;

theorem :: ZF_MODEL:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being ZF-formula
for E being non empty set st H is conjunctive holds
for f being Function of VAR ,E holds
( ( f in St (the_left_argument_of H),E & f in St (the_right_argument_of H),E ) iff f in St H,E )
proof end;

theorem :: ZF_MODEL:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being ZF-formula
for E being non empty set st H is universal holds
for f being Function of VAR ,E holds
( ( f in St (the_scope_of H),E & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
bound_in H = y ) holds
g in St (the_scope_of H),E ) ) iff f in St H,E )
proof end;

definition
let D be non empty set ;
let f be Function of VAR ,D;
let H be ZF-formula;
pred D,f |= H means :Def4: :: ZF_MODEL:def 4
f in St H,D;
end;

:: deftheorem Def4 defines |= ZF_MODEL:def 4 :
for D being non empty set
for f being Function of VAR ,D
for H being ZF-formula holds
( D,f |= H iff f in St H,D );

theorem :: ZF_MODEL:12  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 of VAR ,E
for x, y being Variable holds
( E,f |= x '=' y iff f . x = f . y )
proof end;

theorem :: ZF_MODEL:13  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 of VAR ,E
for x, y being Variable holds
( E,f |= x 'in' y iff f . x in f . y )
proof end;

theorem Th14: :: ZF_MODEL: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 f being Function of VAR ,E
for H being ZF-formula holds
( E,f |= H iff not E,f |= 'not' H )
proof end;

theorem Th15: :: ZF_MODEL:15  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 of VAR ,E
for H, H' being ZF-formula holds
( E,f |= H '&' H' iff ( E,f |= H & E,f |= H' ) )
proof end;

theorem Th16: :: ZF_MODEL:16  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 of VAR ,E
for H being ZF-formula
for x being Variable holds
( E,f |= All x,H iff for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
E,g |= H )
proof end;

theorem :: ZF_MODEL:17  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 of VAR ,E
for H, H' being ZF-formula holds
( E,f |= H 'or' H' iff ( E,f |= H or E,f |= H' ) )
proof end;

theorem Th18: :: ZF_MODEL: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 of VAR ,E
for H, H' being ZF-formula holds
( E,f |= H => H' iff ( E,f |= H implies E,f |= H' ) )
proof end;

theorem :: ZF_MODEL: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
for f being Function of VAR ,E
for H, H' being ZF-formula holds
( E,f |= H <=> H' iff ( E,f |= H iff E,f |= H' ) )
proof end;

theorem Th20: :: ZF_MODEL: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
for f being Function of VAR ,E
for H being ZF-formula
for x being Variable holds
( E,f |= Ex x,H iff ex g being Function of VAR ,E st
( ( for y being Variable st g . y <> f . y holds
x = y ) & E,g |= H ) )
proof end;

theorem Th21: :: ZF_MODEL: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
for f being Function of VAR ,E
for x being Variable
for e being Element of E ex g being Function of VAR ,E st
( g . x = e & ( for z being Variable st z <> x holds
g . z = f . z ) )
proof end;

theorem :: ZF_MODEL:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being ZF-formula
for x, y being Variable
for E being non empty set
for f being Function of VAR ,E holds
( E,f |= All x,y,H iff for g being Function of VAR ,E st ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) holds
E,g |= H )
proof end;

theorem :: ZF_MODEL:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being ZF-formula
for x, y being Variable
for E being non empty set
for f being Function of VAR ,E holds
( E,f |= Ex x,y,H iff ex g being Function of VAR ,E st
( ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) )
proof end;

definition
let E be non empty set ;
let H be ZF-formula;
pred E |= H means :Def5: :: ZF_MODEL:def 5
for f being Function of VAR ,E holds E,f |= H;
end;

:: deftheorem Def5 defines |= ZF_MODEL:def 5 :
for E being non empty set
for H being ZF-formula holds
( E |= H iff for f being Function of VAR ,E holds E,f |= H );

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

theorem :: ZF_MODEL:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being ZF-formula
for x being Variable
for E being non empty set holds
( E |= All x,H iff E |= H )
proof end;

definition
func the_axiom_of_extensionality -> ZF-formula equals :: ZF_MODEL:def 6
All (x. 0),(x. 1),((All (x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) => ((x. 0) '=' (x. 1)));
correctness
coherence
All (x. 0),(x. 1),((All (x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) => ((x. 0) '=' (x. 1))) is ZF-formula
;
;
func the_axiom_of_pairs -> ZF-formula equals :: ZF_MODEL:def 7
All (x. 0),(x. 1),(Ex (x. 2),(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))));
correctness
coherence
All (x. 0),(x. 1),(Ex (x. 2),(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))) is ZF-formula
;
;
func the_axiom_of_unions -> ZF-formula equals :: ZF_MODEL:def 8
All (x. 0),(Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))));
correctness
coherence
All (x. 0),(Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is ZF-formula
;
;
func the_axiom_of_infinity -> ZF-formula equals :: ZF_MODEL:def 9
Ex (x. 0),(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)))))))));
correctness
coherence
Ex (x. 0),(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))))))))) is ZF-formula
;
;
func the_axiom_of_power_sets -> ZF-formula equals :: ZF_MODEL:def 10
All (x. 0),(Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))));
correctness
coherence
All (x. 0),(Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))) is ZF-formula
;
;
end;

:: deftheorem defines the_axiom_of_extensionality ZF_MODEL:def 6 :
the_axiom_of_extensionality = All (x. 0),(x. 1),((All (x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) => ((x. 0) '=' (x. 1)));

:: deftheorem defines the_axiom_of_pairs ZF_MODEL:def 7 :
the_axiom_of_pairs = All (x. 0),(x. 1),(Ex (x. 2),(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))));

:: deftheorem defines the_axiom_of_unions ZF_MODEL:def 8 :
the_axiom_of_unions = All (x. 0),(Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))));

:: deftheorem defines the_axiom_of_infinity ZF_MODEL:def 9 :
the_axiom_of_infinity = Ex (x. 0),(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)))))))));

:: deftheorem defines the_axiom_of_power_sets ZF_MODEL:def 10 :
the_axiom_of_power_sets = All (x. 0),(Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))));

definition
let H be ZF-formula;
func the_axiom_of_substitution_for H -> ZF-formula equals :: ZF_MODEL:def 11
(All (x. 3),(Ex (x. 0),(All (x. 4),(H <=> ((x. 4) '=' (x. 0)))))) => (All (x. 1),(Ex (x. 2),(All (x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H))))));
correctness
coherence
(All (x. 3),(Ex (x. 0),(All (x. 4),(H <=> ((x. 4) '=' (x. 0)))))) => (All (x. 1),(Ex (x. 2),(All (x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H)))))) is ZF-formula
;
;
end;

:: deftheorem defines the_axiom_of_substitution_for ZF_MODEL:def 11 :
for H being ZF-formula holds the_axiom_of_substitution_for H = (All (x. 3),(Ex (x. 0),(All (x. 4),(H <=> ((x. 4) '=' (x. 0)))))) => (All (x. 1),(Ex (x. 2),(All (x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' H))))));

definition
let E be non empty set ;
attr E is being_a_model_of_ZF means :: ZF_MODEL:def 12
( 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 ) );
end;

:: deftheorem defines being_a_model_of_ZF ZF_MODEL:def 12 :
for E being non empty set holds
( E is being_a_model_of_ZF iff ( 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 ) ) );

notation
let E be non empty set ;
synonym E is_a_model_of_ZF for being_a_model_of_ZF E;
end;