:: ZF_MODEL semantic presentation begin scheme :: ZF_MODEL:sch 1 ZFschex{ F1( ($#m2_subset_1 :::"Variable":::) "," ($#m2_subset_1 :::"Variable":::)) -> ($#m1_hidden :::"set"::: ) , F2( ($#m2_subset_1 :::"Variable":::) "," ($#m2_subset_1 :::"Variable":::)) -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5( ($#m2_subset_1 :::"Variable":::) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F6() -> ($#m2_finseq_1 :::"ZF-formula":::) } : (Bool "ex" (Set (Var "a")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")) ")" ) "," (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")) ")" ) "," (Set F2 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" ) & (Bool (Set ($#k4_tarski :::"["::: ) (Set F6 "(" ")" ) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "H")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v2_zf_lang :::"being_equality"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H")) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H")) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v3_zf_lang :::"being_membership"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H")) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H")) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "b")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k20_zf_lang :::"the_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "b")) "," (Set (Var "c")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set "(" ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" ")" )) ")" ) ")" )) proof end; scheme :: ZF_MODEL:sch 2 ZFschuniq{ F1( ($#m2_subset_1 :::"Variable":::) "," ($#m2_subset_1 :::"Variable":::)) -> ($#m1_hidden :::"set"::: ) , F2( ($#m2_subset_1 :::"Variable":::) "," ($#m2_subset_1 :::"Variable":::)) -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5( ($#m2_subset_1 :::"Variable":::) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F6() -> ($#m2_finseq_1 :::"ZF-formula":::), F7() -> ($#m1_hidden :::"set"::: ) , F8() -> ($#m1_hidden :::"set"::: ) } : (Bool (Set F7 "(" ")" ) ($#r1_hidden :::"="::: ) (Set F8 "(" ")" )) provided (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")) ")" ) "," (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")) ")" ) "," (Set F2 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" ) & (Bool (Set ($#k4_tarski :::"["::: ) (Set F6 "(" ")" ) "," (Set F7 "(" ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "H")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v2_zf_lang :::"being_equality"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H")) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H")) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v3_zf_lang :::"being_membership"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H")) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H")) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "b")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k20_zf_lang :::"the_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "b")) "," (Set (Var "c")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set "(" ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" ")" )) ")" ) ")" )) and (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")) ")" ) "," (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")) ")" ) "," (Set F2 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" ) & (Bool (Set ($#k4_tarski :::"["::: ) (Set F6 "(" ")" ) "," (Set F8 "(" ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "H")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v2_zf_lang :::"being_equality"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H")) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H")) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v3_zf_lang :::"being_membership"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H")) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H")) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "b")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k20_zf_lang :::"the_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "b")) "," (Set (Var "c")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set "(" ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" ")" )) ")" ) ")" )) proof end; scheme :: ZF_MODEL:sch 3 ZFschresult{ F1( ($#m2_subset_1 :::"Variable":::) "," ($#m2_subset_1 :::"Variable":::)) -> ($#m1_hidden :::"set"::: ) , F2( ($#m2_subset_1 :::"Variable":::) "," ($#m2_subset_1 :::"Variable":::)) -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5( ($#m2_subset_1 :::"Variable":::) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F6() -> ($#m2_finseq_1 :::"ZF-formula":::), F7( ($#m2_finseq_1 :::"ZF-formula":::)) -> ($#m1_hidden :::"set"::: ) } : (Bool "(" "(" (Bool (Bool (Set F6 "(" ")" ) "is" ($#v2_zf_lang :::"being_equality"::: ) )) "implies" (Bool (Set F7 "(" (Set F6 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set F6 "(" ")" ) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set F6 "(" ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set F6 "(" ")" ) "is" ($#v3_zf_lang :::"being_membership"::: ) )) "implies" (Bool (Set F7 "(" (Set F6 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set F6 "(" ")" ) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set F6 "(" ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set F6 "(" ")" ) "is" ($#v4_zf_lang :::"negative"::: ) )) "implies" (Bool (Set F7 "(" (Set F6 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set F7 "(" (Set "(" ($#k20_zf_lang :::"the_argument_of"::: ) (Set F6 "(" ")" ) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Set F6 "(" ")" ) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "implies" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set "(" ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set F6 "(" ")" ) ")" ) ")" )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set "(" ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set F6 "(" ")" ) ")" ) ")" ))) "holds" (Bool (Set F7 "(" (Set F6 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) ")" & "(" (Bool (Bool (Set F6 "(" ")" ) "is" ($#v6_zf_lang :::"universal"::: ) )) "implies" (Bool (Set F7 "(" (Set F6 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set "(" ($#k23_zf_lang :::"bound_in"::: ) (Set F6 "(" ")" ) ")" ) "," (Set F7 "(" (Set "(" ($#k24_zf_lang :::"the_scope_of"::: ) (Set F6 "(" ")" ) ")" ) ")" ) ")" )) ")" ")" ) provided (Bool "for" (Set (Var "H9")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "H9")) ")" )) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")) ")" ) "," (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")) ")" ) "," (Set F2 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" ) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "H9")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "H")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v2_zf_lang :::"being_equality"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H")) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H")) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v3_zf_lang :::"being_membership"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H")) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H")) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "b")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k20_zf_lang :::"the_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "b")) "," (Set (Var "c")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set "(" ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" ")" )) ")" ) ")" )) ")" ))) proof end; scheme :: ZF_MODEL:sch 4 ZFschproperty{ F1( ($#m2_subset_1 :::"Variable":::) "," ($#m2_subset_1 :::"Variable":::)) -> ($#m1_hidden :::"set"::: ) , F2( ($#m2_subset_1 :::"Variable":::) "," ($#m2_subset_1 :::"Variable":::)) -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F5( ($#m2_subset_1 :::"Variable":::) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F6( ($#m2_finseq_1 :::"ZF-formula":::)) -> ($#m1_hidden :::"set"::: ) , F7() -> ($#m2_finseq_1 :::"ZF-formula":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool P1[(Set F6 "(" (Set F7 "(" ")" ) ")" )]) provided (Bool "for" (Set (Var "H9")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F6 "(" (Set (Var "H9")) ")" )) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")) ")" ) "," (Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")) ")" ) "," (Set F2 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" ) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "H9")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "H")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v2_zf_lang :::"being_equality"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F1 "(" (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H")) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H")) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v3_zf_lang :::"being_membership"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H")) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H")) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "b")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k20_zf_lang :::"the_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "b")) "," (Set (Var "c")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set "(" ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" ")" )) ")" ) ")" )) ")" ))) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool P1[(Set F1 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )]) & (Bool P1[(Set F2 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )]) ")" )) and (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool P1[(Set (Var "a"))])) "holds" (Bool P1[(Set F3 "(" (Set (Var "a")) ")" )])) and (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool P1[(Set (Var "a"))]) & (Bool P1[(Set (Var "b"))])) "holds" (Bool P1[(Set F4 "(" (Set (Var "a")) "," (Set (Var "b")) ")" )])) and (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Bool P1[(Set (Var "a"))])) "holds" (Bool P1[(Set F5 "(" (Set (Var "x")) "," (Set (Var "a")) ")" )]))) proof end; definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); func :::"Free"::: "H" -> ($#m1_hidden :::"set"::: ) means :: ZF_MODEL:def 1 (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")) ")" ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")) ")" ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" ) & (Bool (Set ($#k4_tarski :::"["::: ) "H" "," it ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "H9")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "H9")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H9")) "is" ($#v2_zf_lang :::"being_equality"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H9")) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H9")) ")" ) ($#k2_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v3_zf_lang :::"being_membership"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H9")) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H9")) ")" ) ($#k2_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v4_zf_lang :::"negative"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k20_zf_lang :::"the_argument_of"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k2_tarski :::"}"::: ) ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v6_zf_lang :::"universal"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tarski :::"union"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H9")) ")" ) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" ")" )) ")" ) ")" )); end; :: deftheorem defines :::"Free"::: ZF_MODEL:def 1 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_zf_model :::"Free"::: ) (Set (Var "H")))) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")) ")" ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")) ")" ) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" ) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "H")) "," (Set (Var "b2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "H9")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "H9")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H9")) "is" ($#v2_zf_lang :::"being_equality"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H9")) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H9")) ")" ) ($#k2_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v3_zf_lang :::"being_membership"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H9")) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H9")) ")" ) ($#k2_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v4_zf_lang :::"negative"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k20_zf_lang :::"the_argument_of"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k2_tarski :::"}"::: ) ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v6_zf_lang :::"universal"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tarski :::"union"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H9")) ")" ) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" ")" )) ")" ) ")" )) ")" ))); definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); :: original: :::"Free"::: redefine func :::"Free"::: "H" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ); end; theorem :: ZF_MODEL:1 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H")) "is" ($#v2_zf_lang :::"being_equality"::: ) )) "implies" (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H")) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H")) ")" ) ($#k2_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v3_zf_lang :::"being_membership"::: ) )) "implies" (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H")) ")" ) "," (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H")) ")" ) ($#k2_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) )) "implies" (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set "(" ($#k20_zf_lang :::"the_argument_of"::: ) (Set (Var "H")) ")" ))) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "implies" (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_zf_model :::"Free"::: ) (Set "(" ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_zf_model :::"Free"::: ) (Set "(" ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) "implies" (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_zf_model :::"Free"::: ) (Set "(" ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H")) ")" ) ($#k1_tarski :::"}"::: ) ))) ")" ")" )) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"VAL"::: "D" -> ($#m1_hidden :::"set"::: ) equals :: ZF_MODEL:def 2 (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," "D" ")" ); end; :: deftheorem defines :::"VAL"::: ZF_MODEL:def 2 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_zf_model :::"VAL"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "D")) ")" ))); registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_zf_model :::"VAL"::: ) "D") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); let "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"St"::: "(" "H" "," "E" ")" -> ($#m1_hidden :::"set"::: ) means :: ZF_MODEL:def 3 (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")) ")" ) "," "{" (Set (Var "v1")) where v1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zf_model :::"VAL"::: ) "E") : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," "E" "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "v1")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "}" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")) ")" ) "," "{" (Set (Var "v2")) where v2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zf_model :::"VAL"::: ) "E") : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," "E" "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "v2")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "}" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" ) & (Bool (Set ($#k4_tarski :::"["::: ) "H" "," it ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "H9")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "H9")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H9")) "is" ($#v2_zf_lang :::"being_equality"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) "{" (Set (Var "v3")) where v3 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zf_model :::"VAL"::: ) "E") : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," "E" "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "v3")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H9")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H9")) ")" )))) "}" ) ")" & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v3_zf_lang :::"being_membership"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) "{" (Set (Var "v4")) where v4 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zf_model :::"VAL"::: ) "E") : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," "E" "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "v4")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H9")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H9")) ")" )))) "}" ) ")" & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v4_zf_lang :::"negative"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_zf_model :::"VAL"::: ) "E" ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ) ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k20_zf_lang :::"the_argument_of"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tarski :::"union"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "c")) ($#k1_tarski :::"}"::: ) ) ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v6_zf_lang :::"universal"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) "{" (Set (Var "v5")) where v5 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zf_model :::"VAL"::: ) "E") : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," "E" "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "v5")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," "E" "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H9"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) "holds" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" ))) "}" ) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" ")" )) ")" ) ")" )); end; :: deftheorem defines :::"St"::: ZF_MODEL:def 3 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_zf_model :::"St"::: ) "(" (Set (Var "H")) "," (Set (Var "E")) ")" )) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")) ")" ) "," "{" (Set (Var "v1")) where v1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zf_model :::"VAL"::: ) (Set (Var "E"))) : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "v1")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "}" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")) ")" ) "," "{" (Set (Var "v2")) where v2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zf_model :::"VAL"::: ) (Set (Var "E"))) : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "v2")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "}" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" ) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "H")) "," (Set (Var "b3")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "H9")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "H9")) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "H9")) "is" ($#v2_zf_lang :::"being_equality"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) "{" (Set (Var "v3")) where v3 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zf_model :::"VAL"::: ) (Set (Var "E"))) : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "v3")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H9")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H9")) ")" )))) "}" ) ")" & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v3_zf_lang :::"being_membership"::: ) )) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) "{" (Set (Var "v4")) where v4 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zf_model :::"VAL"::: ) (Set (Var "E"))) : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "v4")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H9")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H9")) ")" )))) "}" ) ")" & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v4_zf_lang :::"negative"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_zf_model :::"VAL"::: ) (Set (Var "E")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ) ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k20_zf_lang :::"the_argument_of"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tarski :::"union"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "c")) ($#k1_tarski :::"}"::: ) ) ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "c")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" & "(" (Bool (Bool (Set (Var "H9")) "is" ($#v6_zf_lang :::"universal"::: ) )) "implies" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) "{" (Set (Var "v5")) where v5 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zf_model :::"VAL"::: ) (Set (Var "E"))) : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "v5")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H9"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) "holds" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" ))) "}" ) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) ")" ")" )) ")" ) ")" )) ")" )))); definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); let "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; :: original: :::"St"::: redefine func :::"St"::: "(" "H" "," "E" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_zf_model :::"VAL"::: ) "E" ")" ); end; theorem :: ZF_MODEL:2 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set "(" (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")) ")" ) "," (Set (Var "E")) ")" )) ")" )))) ; theorem :: ZF_MODEL:3 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set "(" (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")) ")" ) "," (Set (Var "E")) ")" )) ")" )))) ; theorem :: ZF_MODEL:4 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set (Var "H")) "," (Set (Var "E")) ")" ))) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set "(" ($#k6_zf_lang :::"'not'"::: ) (Set (Var "H")) ")" ) "," (Set (Var "E")) ")" )) ")" )))) ; theorem :: ZF_MODEL:5 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "H9")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set (Var "H")) "," (Set (Var "E")) ")" )) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set (Var "H9")) "," (Set (Var "E")) ")" )) ")" ) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set "(" (Set (Var "H")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "H9")) ")" ) "," (Set (Var "E")) ")" )) ")" )))) ; theorem :: ZF_MODEL:6 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set (Var "H")) "," (Set (Var "E")) ")" )) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) "holds" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set (Var "H")) "," (Set (Var "E")) ")" )) ")" ) ")" ) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" ")" ) "," (Set (Var "E")) ")" )) ")" ))))) ; theorem :: ZF_MODEL:7 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v2_zf_lang :::"being_equality"::: ) )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H")) ")" ))) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set (Var "H")) "," (Set (Var "E")) ")" )) ")" )))) ; theorem :: ZF_MODEL:8 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v3_zf_lang :::"being_membership"::: ) )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k18_zf_lang :::"Var1"::: ) (Set (Var "H")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k19_zf_lang :::"Var2"::: ) (Set (Var "H")) ")" ))) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set (Var "H")) "," (Set (Var "E")) ")" )) ")" )))) ; theorem :: ZF_MODEL:9 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v4_zf_lang :::"negative"::: ) )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set "(" ($#k20_zf_lang :::"the_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "E")) ")" ))) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set (Var "H")) "," (Set (Var "E")) ")" )) ")" )))) ; theorem :: ZF_MODEL:10 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v5_zf_lang :::"conjunctive"::: ) )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set "(" ($#k21_zf_lang :::"the_left_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "E")) ")" )) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set "(" ($#k22_zf_lang :::"the_right_argument_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "E")) ")" )) ")" ) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set (Var "H")) "," (Set (Var "E")) ")" )) ")" )))) ; theorem :: ZF_MODEL:11 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v6_zf_lang :::"universal"::: ) )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set "(" ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "E")) ")" )) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set ($#k23_zf_lang :::"bound_in"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) "holds" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set "(" ($#k24_zf_lang :::"the_scope_of"::: ) (Set (Var "H")) ")" ) "," (Set (Var "E")) ")" )) ")" ) ")" ) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set (Var "H")) "," (Set (Var "E")) ")" )) ")" )))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Const "D")); let "H" be ($#m2_finseq_1 :::"ZF-formula":::); pred "D" "," "f" :::"|="::: "H" means :: ZF_MODEL:def 4 (Bool "f" ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" "H" "," "D" ")" )); end; :: deftheorem defines :::"|="::: ZF_MODEL:def 4 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "D")) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "D")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k5_zf_model :::"St"::: ) "(" (Set (Var "H")) "," (Set (Var "D")) ")" )) ")" )))); theorem :: ZF_MODEL:12 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Set (Var "x")) ($#k4_zf_lang :::"'='"::: ) (Set (Var "y")))) "iff" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" )))) ; theorem :: ZF_MODEL:13 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Set (Var "x")) ($#k5_zf_lang :::"'in'"::: ) (Set (Var "y")))) "iff" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) ")" )))) ; theorem :: ZF_MODEL:14 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Bool "not" (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set ($#k6_zf_lang :::"'not'"::: ) (Set (Var "H"))))) ")" )))) ; theorem :: ZF_MODEL:15 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "H")) "," (Set (Var "H9")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Set (Var "H")) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "H9")))) "iff" (Bool "(" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) & (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Var "H9"))) ")" ) ")" )))) ; theorem :: ZF_MODEL:16 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" )) "iff" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) "holds" (Bool (Set (Var "E")) "," (Set (Var "g")) ($#r1_zf_model :::"|="::: ) (Set (Var "H")))) ")" ))))) ; theorem :: ZF_MODEL:17 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "H")) "," (Set (Var "H9")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Set (Var "H")) ($#k10_zf_lang :::"'or'"::: ) (Set (Var "H9")))) "iff" (Bool "(" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) "or" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Var "H9"))) ")" ) ")" )))) ; theorem :: ZF_MODEL:18 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "H")) "," (Set (Var "H9")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Set (Var "H")) ($#k11_zf_lang :::"=>"::: ) (Set (Var "H9")))) "iff" "(" (Bool (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Var "H")))) "implies" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Var "H9"))) ")" ")" )))) ; theorem :: ZF_MODEL:19 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "H")) "," (Set (Var "H9")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Set (Var "H")) ($#k12_zf_lang :::"<=>"::: ) (Set (Var "H9")))) "iff" (Bool "(" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Var "H9"))) ")" ) ")" )))) ; theorem :: ZF_MODEL:20 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set ($#k13_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" )) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "st" (Bool "(" (Bool "(" "for" (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) & (Bool (Set (Var "E")) "," (Set (Var "g")) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) ")" )) ")" ))))) ; theorem :: ZF_MODEL:21 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set ($#k14_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "H")) ")" )) "iff" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" "not" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "z")))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) "or" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" ) ")" )) "holds" (Bool (Set (Var "E")) "," (Set (Var "g")) ($#r1_zf_model :::"|="::: ) (Set (Var "H")))) ")" ))))) ; theorem :: ZF_MODEL:22 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set ($#k15_zf_lang :::"Ex"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "H")) ")" )) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "st" (Bool "(" (Bool "(" "for" (Set (Var "z")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool "(" "not" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "z")))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) "or" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" ) ")" ) & (Bool (Set (Var "E")) "," (Set (Var "g")) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) ")" )) ")" ))))) ; definitionlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "H" be ($#m2_finseq_1 :::"ZF-formula":::); pred "E" :::"|="::: "H" means :: ZF_MODEL:def 5 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," "E" "holds" (Bool "E" "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) "H")); end; :: deftheorem defines :::"|="::: ZF_MODEL:def 5 : (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "holds" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Var "H")))) ")" ))); theorem :: ZF_MODEL:23 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" )) "iff" (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set (Var "H"))) ")" )))) ; definitionfunc :::"the_axiom_of_extensionality"::: -> ($#m2_finseq_1 :::"ZF-formula":::) equals :: ZF_MODEL:def 6 (Set ($#k14_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) ")" ) ")" ) ")" ")" ) ($#k11_zf_lang :::"=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) ")" ) ")" ) ")" ); func :::"the_axiom_of_pairs"::: -> ($#m2_finseq_1 :::"ZF-formula":::) equals :: ZF_MODEL:def 7 (Set ($#k14_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ")" ) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k10_zf_lang :::"'or'"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" ); func :::"the_axiom_of_unions"::: -> ($#m2_finseq_1 :::"ZF-formula":::) equals :: ZF_MODEL:def 8 (Set ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) ")" ) ($#k12_zf_lang :::"<=>"::: ) (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ")" ) ($#k7_zf_lang :::"'&'"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ")" ) ")" ); func :::"the_axiom_of_infinity"::: -> ($#m2_finseq_1 :::"ZF-formula":::) equals :: ZF_MODEL:def 9 (Set ($#k15_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k7_zf_lang :::"'&'"::: ) (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k11_zf_lang :::"=>"::: ) (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k7_zf_lang :::"'&'"::: ) (Set "(" ($#k6_zf_lang :::"'not'"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ($#k7_zf_lang :::"'&'"::: ) (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ")" ) ($#k11_zf_lang :::"=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ")" ); func :::"the_axiom_of_power_sets"::: -> ($#m2_finseq_1 :::"ZF-formula":::) equals :: ZF_MODEL:def 10 (Set ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) ")" ) ($#k12_zf_lang :::"<=>"::: ) (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ")" ) ($#k11_zf_lang :::"=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ")" ) ")" ); end; :: deftheorem defines :::"the_axiom_of_extensionality"::: ZF_MODEL:def 6 : (Bool (Set ($#k6_zf_model :::"the_axiom_of_extensionality"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k14_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) ")" ) ")" ) ")" ")" ) ($#k11_zf_lang :::"=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) ")" ) ")" ) ")" )); :: deftheorem defines :::"the_axiom_of_pairs"::: ZF_MODEL:def 7 : (Bool (Set ($#k7_zf_model :::"the_axiom_of_pairs"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k14_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ")" ) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k10_zf_lang :::"'or'"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" )); :: deftheorem defines :::"the_axiom_of_unions"::: ZF_MODEL:def 8 : (Bool (Set ($#k8_zf_model :::"the_axiom_of_unions"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) ")" ) ($#k12_zf_lang :::"<=>"::: ) (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ")" ) ($#k7_zf_lang :::"'&'"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ")" ) ")" )); :: deftheorem defines :::"the_axiom_of_infinity"::: ZF_MODEL:def 9 : (Bool (Set ($#k9_zf_model :::"the_axiom_of_infinity"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k15_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k7_zf_lang :::"'&'"::: ) (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k11_zf_lang :::"=>"::: ) (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k7_zf_lang :::"'&'"::: ) (Set "(" ($#k6_zf_lang :::"'not'"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ($#k7_zf_lang :::"'&'"::: ) (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ")" ) ($#k11_zf_lang :::"=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ) ")" )); :: deftheorem defines :::"the_axiom_of_power_sets"::: ZF_MODEL:def 10 : (Bool (Set ($#k10_zf_model :::"the_axiom_of_power_sets"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) ")" ) ($#k12_zf_lang :::"<=>"::: ) (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ")" ) ($#k11_zf_lang :::"=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ")" ) ")" )); definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); func :::"the_axiom_of_substitution_for"::: "H" -> ($#m2_finseq_1 :::"ZF-formula":::) equals :: ZF_MODEL:def 11 (Set (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" "H" ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" ")" ) ($#k11_zf_lang :::"=>"::: ) (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ")" ) ($#k12_zf_lang :::"<=>"::: ) (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) ")" ) ($#k7_zf_lang :::"'&'"::: ) "H" ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ")" ) ")" ")" )); end; :: deftheorem defines :::"the_axiom_of_substitution_for"::: ZF_MODEL:def 11 : (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Set ($#k11_zf_model :::"the_axiom_of_substitution_for"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" (Set (Var "H")) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" ")" ) ($#k11_zf_lang :::"=>"::: ) (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ")" ) ($#k12_zf_lang :::"<=>"::: ) (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k5_zf_lang :::"'in'"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) ")" ) ($#k7_zf_lang :::"'&'"::: ) (Set (Var "H")) ")" ) ")" ")" ) ")" ) ")" ")" ) ")" ")" ) ")" ")" )))); definitionlet "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; attr "E" is :::"being_a_model_of_ZF"::: means :: ZF_MODEL:def 12 (Bool "(" (Bool "E" "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) ) & (Bool "E" ($#r2_zf_model :::"|="::: ) (Set ($#k7_zf_model :::"the_axiom_of_pairs"::: ) )) & (Bool "E" ($#r2_zf_model :::"|="::: ) (Set ($#k8_zf_model :::"the_axiom_of_unions"::: ) )) & (Bool "E" ($#r2_zf_model :::"|="::: ) (Set ($#k9_zf_model :::"the_axiom_of_infinity"::: ) )) & (Bool "E" ($#r2_zf_model :::"|="::: ) (Set ($#k10_zf_model :::"the_axiom_of_power_sets"::: ) )) & (Bool "(" "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k1_enumset1 :::"}"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))))) "holds" (Bool "E" ($#r2_zf_model :::"|="::: ) (Set ($#k11_zf_model :::"the_axiom_of_substitution_for"::: ) (Set (Var "H")))) ")" ) ")" ); end; :: deftheorem defines :::"being_a_model_of_ZF"::: ZF_MODEL:def 12 : (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "E")) "is" ($#v1_zf_model :::"being_a_model_of_ZF"::: ) ) "iff" (Bool "(" (Bool (Set (Var "E")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) ) & (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set ($#k7_zf_model :::"the_axiom_of_pairs"::: ) )) & (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set ($#k8_zf_model :::"the_axiom_of_unions"::: ) )) & (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set ($#k9_zf_model :::"the_axiom_of_infinity"::: ) )) & (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set ($#k10_zf_model :::"the_axiom_of_power_sets"::: ) )) & (Bool "(" "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k1_enumset1 :::"}"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set ($#k11_zf_model :::"the_axiom_of_substitution_for"::: ) (Set (Var "H")))) ")" ) ")" ) ")" ));