:: ZFMODEL1 semantic presentation begin theorem :: ZFMODEL1:1 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "E")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set ($#k6_zf_model :::"the_axiom_of_extensionality"::: ) ))) ; theorem :: ZFMODEL1:2 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "E")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set ($#k7_zf_model :::"the_axiom_of_pairs"::: ) )) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) ")" )) ; theorem :: ZFMODEL1:3 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "E")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set ($#k7_zf_model :::"the_axiom_of_pairs"::: ) )) "iff" (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) ")" )) ; theorem :: ZFMODEL1:4 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "E")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set ($#k8_zf_model :::"the_axiom_of_unions"::: ) )) "iff" (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "u"))) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) ")" )) ; theorem :: ZFMODEL1:5 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "E")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set ($#k8_zf_model :::"the_axiom_of_unions"::: ) )) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) ")" )) ; theorem :: ZFMODEL1:6 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "E")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set ($#k9_zf_model :::"the_axiom_of_infinity"::: ) )) "iff" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "u")))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool "(" (Bool (Set (Var "v")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "w"))) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "u"))) ")" )) ")" ) ")" )) ")" )) ; theorem :: ZFMODEL1:7 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "E")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set ($#k9_zf_model :::"the_axiom_of_infinity"::: ) )) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "Z"))) & (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )) ")" ) ")" )) ")" )) ; theorem :: ZFMODEL1:8 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "E")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set ($#k10_zf_model :::"the_axiom_of_power_sets"::: ) )) "iff" (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "E")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "u")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) ")" )) ; theorem :: ZFMODEL1:9 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "E")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool "(" (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (Set ($#k10_zf_model :::"the_axiom_of_power_sets"::: ) )) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "E")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "X")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) ")" )) ; theorem :: ZFMODEL1:10 (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 "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")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))))) & (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" )))))) ; theorem :: ZFMODEL1:11 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "st" (Bool (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H")))) & (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set ($#k14_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "H")) ")" )))))) ; theorem :: ZFMODEL1:12 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_subset_1 :::"Variable":::) (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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "st" (Bool (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_enumset1 :::"}"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H")))) & (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set ($#k16_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "H")) ")" )))))) ; definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); let "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "val" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Const "E")); assume that (Bool (Bool "not" (Set ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Const "H"))))) and (Bool (Set (Const "E")) "," (Set (Const "val")) ($#r1_zf_model :::"|="::: ) (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 (Const "H")) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" )) ; func :::"def_func'"::: "(" "H" "," "val" ")" -> ($#m1_subset_1 :::"Function":::) "of" "E" "," "E" means :: ZFMODEL1:def 1 (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":::) "holds" (Bool "(" "not" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"<>"::: ) (Set "val" ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) "or" (Bool (Set ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "y"))) "or" (Bool (Set ($#k2_zf_lang :::"x."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Var "y"))) "or" (Bool (Set ($#k2_zf_lang :::"x."::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) ")" )) "holds" (Bool "(" (Bool "E" "," (Set (Var "g")) ($#r1_zf_model :::"|="::: ) "H") "iff" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ))) ")" )); end; :: deftheorem defines :::"def_func'"::: ZFMODEL1:def 1 : (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 "val")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "st" (Bool (Bool (Bool "not" (Set ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))))) & (Bool (Set (Var "E")) "," (Set (Var "val")) ($#r1_zf_model :::"|="::: ) (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"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" ))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_zfmodel1 :::"def_func'"::: ) "(" (Set (Var "H")) "," (Set (Var "val")) ")" )) "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":::) "holds" (Bool "(" "not" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "val")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) "or" (Bool (Set ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "y"))) "or" (Bool (Set ($#k2_zf_lang :::"x."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Var "y"))) "or" (Bool (Set ($#k2_zf_lang :::"x."::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Var "E")) "," (Set (Var "g")) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ))) ")" )) ")" ))))); theorem :: ZFMODEL1:13 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) "st" (Bool (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))) "holds" (Bool "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))))) ")" ) & (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "E")) "," (Set (Var "g")) ($#r1_zf_model :::"|="::: ) (Set (Var "H")))))) ; definitionlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); let "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; assume that (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set (Const "H"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k2_tarski :::"}"::: ) )) and (Bool (Set (Const "E")) ($#r2_zf_model :::"|="::: ) (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 (Const "H")) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" )) ; func :::"def_func"::: "(" "H" "," "E" ")" -> ($#m1_subset_1 :::"Function":::) "of" "E" "," "E" means :: ZFMODEL1:def 2 (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," "E" "holds" (Bool "(" (Bool "E" "," (Set (Var "g")) ($#r1_zf_model :::"|="::: ) "H") "iff" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ))) ")" )); end; :: deftheorem defines :::"def_func"::: ZFMODEL1:def 2 : (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 ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (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"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" ))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmodel1 :::"def_func"::: ) "(" (Set (Var "H")) "," (Set (Var "E")) ")" )) "iff" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "E")) "," (Set (Var "g")) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ))) ")" )) ")" )))); definitionlet "F" be ($#m1_hidden :::"Function":::); let "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; pred "F" :::"is_definable_in"::: "E" means :: ZFMODEL1:def 3 (Bool "ex" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "(" (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool "E" ($#r2_zf_model :::"|="::: ) (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"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" )) & (Bool "F" ($#r1_hidden :::"="::: ) (Set ($#k2_zfmodel1 :::"def_func"::: ) "(" (Set (Var "H")) "," "E" ")" )) ")" )); pred "F" :::"is_parametrically_definable_in"::: "E" means :: ZFMODEL1:def 4 (Bool "ex" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::)(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," "E" "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")))) & (Bool "E" "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (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"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" )) & (Bool "F" ($#r1_hidden :::"="::: ) (Set ($#k1_zfmodel1 :::"def_func'"::: ) "(" (Set (Var "H")) "," (Set (Var "f")) ")" )) ")" ))); end; :: deftheorem defines :::"is_definable_in"::: ZFMODEL1:def 3 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_zfmodel1 :::"is_definable_in"::: ) (Set (Var "E"))) "iff" (Bool "ex" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "(" (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "E")) ($#r2_zf_model :::"|="::: ) (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"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" )) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmodel1 :::"def_func"::: ) "(" (Set (Var "H")) "," (Set (Var "E")) ")" )) ")" )) ")" ))); :: deftheorem defines :::"is_parametrically_definable_in"::: ZFMODEL1:def 4 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_zfmodel1 :::"is_parametrically_definable_in"::: ) (Set (Var "E"))) "iff" (Bool "ex" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::)(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E")) "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")))) & (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (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"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" )) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k1_zfmodel1 :::"def_func'"::: ) "(" (Set (Var "H")) "," (Set (Var "f")) ")" )) ")" ))) ")" ))); theorem :: ZFMODEL1: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_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) ($#r1_zfmodel1 :::"is_definable_in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Var "F")) ($#r2_zfmodel1 :::"is_parametrically_definable_in"::: ) (Set (Var "E"))))) ; theorem :: ZFMODEL1:15 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "E")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool "(" (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")))) ")" ) "iff" (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")) "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")))) & (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (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"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" ))) "holds" (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" ($#k1_zfmodel1 :::"def_func'"::: ) "(" (Set (Var "H")) "," (Set (Var "f")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "u"))) ($#r2_hidden :::"in"::: ) (Set (Var "E")))))) ")" )) ; theorem :: ZFMODEL1:16 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "E")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool "(" (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")))) ")" ) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) ($#r2_zfmodel1 :::"is_parametrically_definable_in"::: ) (Set (Var "E")))) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "F")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "E"))))) ")" )) ; theorem :: ZFMODEL1:17 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "E")) "is" ($#v1_zf_model :::"being_a_model_of_ZF"::: ) )) "holds" (Bool "(" (Bool (Set (Var "E")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) ) & (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "u"))) "iff" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "v"))) ")" ) ")" )) "holds" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" ) & (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) ")" ) & (Bool "(" "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "u"))) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) ")" ) & (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "u")))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool "(" (Bool (Set (Var "v")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "w"))) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "u"))) ")" )) ")" ) ")" )) & (Bool "(" "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "E")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "u")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) ")" ) & (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")) "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")))) & (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (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"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" ))) "holds" (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" ($#k1_zfmodel1 :::"def_func'"::: ) "(" (Set (Var "H")) "," (Set (Var "f")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "u"))) ($#r2_hidden :::"in"::: ) (Set (Var "E"))))) ")" ) ")" )) ; theorem :: ZFMODEL1:18 (Bool "for" (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "E")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) ) & (Bool "(" "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) ")" ) & (Bool "(" "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "u"))) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) ")" ) & (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "u")))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "st" (Bool "(" (Bool (Set (Var "v")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "w"))) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "u"))) ")" )) ")" ) ")" )) & (Bool "(" "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool (Set (Set (Var "E")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "u")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) ")" ) & (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")) "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")))) & (Bool (Set (Var "E")) "," (Set (Var "f")) ($#r1_zf_model :::"|="::: ) (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"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" ))) "holds" (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" ($#k1_zfmodel1 :::"def_func'"::: ) "(" (Set (Var "H")) "," (Set (Var "f")) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "u"))) ($#r2_hidden :::"in"::: ) (Set (Var "E"))))) ")" )) "holds" (Bool (Set (Var "E")) "is" ($#v1_zf_model :::"being_a_model_of_ZF"::: ) )) ;