:: Models and Satisfiability. Defining by Structural Induction and Free Variables in ZF-formulae :: by Grzegorz Bancerek :: :: Received April 14, 1989 :: Copyright (c) 1990-2012 Association of Mizar Users begin 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 being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_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 ) ) ) ) ) proofend; 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 being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_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 being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_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 ) ) ) ) ) proofend; 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 being_equality implies F7(F6()) = F1((Var1 F6()),(Var2 F6())) ) & ( F6() is being_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 H9 being ZF-formula for a being set holds ( a = F7(H9) 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 ) ) & [H9,a] in A & ( for H being ZF-formula for a being set st [H,a] in A holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_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 ) ) ) ) ) ) proofend; 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 H9 being ZF-formula for a being set holds ( a = F6(H9) 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 ) ) & [H9,a] in A & ( for H being ZF-formula for a being set st [H,a] in A holds ( ( H is being_equality implies a = F1((Var1 H),(Var2 H)) ) & ( H is being_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)] proofend; 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 ) -> Element of K27((union {$2})) = (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 H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is being_membership implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is negative implies ex b being set st ( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = union {b,c} & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = (union {b}) \ {(bound_in H9)} & [(the_scope_of H9),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 H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is being_membership implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is negative implies ex b being set st ( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = union {b,c} & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = (union {b}) \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) proofend; 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 H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is being_membership implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is negative implies ex b being set st ( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = union {b,c} & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = (union {b}) \ {(bound_in H9)} & [(the_scope_of H9),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 H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is being_membership implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is negative implies ex b being set st ( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = union {b,c} & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = (union {b}) \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) holds b1 = b2 proofend; 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 H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is being_membership implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is negative implies ex b being set st ( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = union {b,c} & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = (union {b}) \ {(bound_in H9)} & [(the_scope_of H9),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 H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = H1( Var1 H9, Var2 H9) ) & ( H9 is being_membership implies a = H2( Var1 H9, Var2 H9) ) & ( H9 is negative implies ex b being set st ( a = H3(b) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = H4(b,c) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = H5( bound_in H9,b) & [(the_scope_of H9),b] in A ) ) ) ) ) ) by Def1; Lm2: now__::_thesis:_for_H_being_ZF-formula_holds_ (_(_H_is_being_equality_implies_H6(H)_=_H1(_Var1_H,_Var2_H)_)_&_(_H_is_being_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))_)_) let H be ZF-formula; ::_thesis: ( ( H is being_equality implies H6(H) = H1( Var1 H, Var2 H) ) & ( H is being_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 being_equality implies H6(H) = H1( Var1 H, Var2 H) ) & ( H is being_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(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 proofend; end; theorem :: ZF_MODEL:1 for H being ZF-formula holds ( ( H is being_equality implies Free H = {(Var1 H),(Var2 H)} ) & ( H is being_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)} ) ) proofend; :: The set of all valuations of variables in a model definition let D be non empty set ; func VAL D -> set equals :: ZF_MODEL:def 2 Funcs (VAR,D); coherence Funcs (VAR,D) is set ; end; :: deftheorem defines VAL ZF_MODEL:def_2_:_ for D being non empty set holds VAL D = Funcs (VAR,D); registration let D be non empty set ; cluster VAL D -> non empty ; coherence not VAL D is empty ; end; :: The set of all valuations which satisfy a ZF-formula in a model definition deffunc H7( set , set ) -> set = (union {$1}) /\ (union {$2}); let H be ZF-formula; let E be non empty set ; 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 = f . $2 } ; deffunc H9( 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 H10( set ) -> Element of K27((VAL E)) = (VAL E) \ (union {$1}); 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 H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st ( a = (VAL E) \ (union {b}) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 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 H9 = y ) holds g in X ) ) } & [(the_scope_of H9),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 H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st ( a = (VAL E) \ (union {b}) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 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 H9 = y ) holds g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ) proofend; 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 H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st ( a = (VAL E) \ (union {b}) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 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 H9 = y ) holds g in X ) ) } & [(the_scope_of H9),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 H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st ( a = (VAL E) \ (union {b}) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 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 H9 = y ) holds g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ) holds b1 = b2 proofend; 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 H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st ( a = (VAL E) \ (union {b}) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = (union {b}) /\ (union {c}) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 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 H9 = y ) holds g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ) ); Lm3: now__::_thesis:_for_H_being_ZF-formula for_E_being_non_empty_set_holds_ (_(_H_is_being_equality_implies_H12(H)_=_H8(_Var1_H,_Var2_H)_)_&_(_H_is_being_membership_implies_H12(H)_=_H9(_Var1_H,_Var2_H)_)_&_(_H_is_negative_implies_H12(H)_=_H10(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)_=_H7(a,b)_)_&_(_H_is_universal_implies_H12(H)_=_H11(_bound_in_H,H12(_the_scope_of_H))_)_) deffunc H7( set , set ) -> set = (union {$1}) /\ (union {$2}); let H be ZF-formula; ::_thesis: for E being non empty set holds ( ( H is being_equality implies H12(H) = H8( Var1 H, Var2 H) ) & ( H is being_membership implies H12(H) = H9( Var1 H, Var2 H) ) & ( H is negative implies H12(H) = H10(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) = H7(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 being_equality implies H12(H) = H8( Var1 H, Var2 H) ) & ( H is being_membership implies H12(H) = H9( Var1 H, Var2 H) ) & ( H is negative implies H12(H) = H10(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) = H7(a,b) ) & ( H is universal implies H12(H) = H11( bound_in H,H12( the_scope_of H)) ) ) 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 = f . $2 } ; deffunc H9( 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 H10( set ) -> Element of K27((VAL E)) = (VAL E) \ (union {$1}); 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),H8(x,y)] in A & [(x 'in' y),H9(x,y)] in A ) ) & [H,a] in A & ( for H9 being ZF-formula for a being set st [H9,a] in A holds ( ( H9 is being_equality implies a = H8( Var1 H9, Var2 H9) ) & ( H9 is being_membership implies a = H9( Var1 H9, Var2 H9) ) & ( H9 is negative implies ex b being set st ( a = H10(b) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st ( a = H7(b,c) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st ( a = H11( bound_in H9,b) & [(the_scope_of H9),b] in A ) ) ) ) ) ) by Def3; thus ( ( H is being_equality implies H12(H) = H8( Var1 H, Var2 H) ) & ( H is being_membership implies H12(H) = H9( Var1 H, Var2 H) ) & ( H is negative implies H12(H) = H10(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) = H7(a,b) ) & ( H is universal implies H12(H) = H11( bound_in H,H12( the_scope_of H)) ) ) from ZF_MODEL:sch_3(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) proofend; end; theorem Th2: :: ZF_MODEL:2 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) ) proofend; theorem Th3: :: ZF_MODEL:3 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) ) proofend; theorem Th4: :: ZF_MODEL:4 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) ) proofend; theorem Th5: :: ZF_MODEL:5 for E being non empty set for H, H9 being ZF-formula for f being Function of VAR,E holds ( ( f in St (H,E) & f in St (H9,E) ) iff f in St ((H '&' H9),E) ) proofend; theorem Th6: :: ZF_MODEL:6 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) ) proofend; theorem :: ZF_MODEL:7 for H being ZF-formula for E being non empty set st H is being_equality holds for f being Function of VAR,E holds ( f . (Var1 H) = f . (Var2 H) iff f in St (H,E) ) proofend; theorem :: ZF_MODEL:8 for H being ZF-formula for E being non empty set st H is being_membership holds for f being Function of VAR,E holds ( f . (Var1 H) in f . (Var2 H) iff f in St (H,E) ) proofend; theorem :: ZF_MODEL:9 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) ) proofend; theorem :: ZF_MODEL:10 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) ) proofend; theorem :: ZF_MODEL:11 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) ) proofend; :: The satisfaction of a ZF-formula in a model by a valuation definition let D be non empty set ; let f be Function of VAR,D; let H be ZF-formula; predD,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 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 ) proofend; theorem :: ZF_MODEL:13 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 ) proofend; theorem Th14: :: ZF_MODEL:14 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 ) proofend; theorem Th15: :: ZF_MODEL:15 for E being non empty set for f being Function of VAR,E for H, H9 being ZF-formula holds ( E,f |= H '&' H9 iff ( E,f |= H & E,f |= H9 ) ) proofend; theorem Th16: :: ZF_MODEL:16 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 ) proofend; theorem :: ZF_MODEL:17 for E being non empty set for f being Function of VAR,E for H, H9 being ZF-formula holds ( E,f |= H 'or' H9 iff ( E,f |= H or E,f |= H9 ) ) proofend; theorem Th18: :: ZF_MODEL:18 for E being non empty set for f being Function of VAR,E for H, H9 being ZF-formula holds ( E,f |= H => H9 iff ( E,f |= H implies E,f |= H9 ) ) proofend; theorem :: ZF_MODEL:19 for E being non empty set for f being Function of VAR,E for H, H9 being ZF-formula holds ( E,f |= H <=> H9 iff ( E,f |= H iff E,f |= H9 ) ) proofend; theorem Th20: :: ZF_MODEL:20 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 ) ) proofend; theorem :: ZF_MODEL:21 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 ) proofend; theorem :: ZF_MODEL:22 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 ) ) proofend; :: The satisfaction of a ZF-formula in a model definition let E be non empty set ; let H be ZF-formula; predE |= 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:23 for H being ZF-formula for x being Variable for E being non empty set holds ( E |= All (x,H) iff E |= H ) proofend; :: The axioms of ZF-language 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 ; attrE 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 ) ) );