:: ZF_FUND2  semantic presentation begin  











































definitionlet "H" be   ($#m2_finseq_1 :::"ZF-formula":::); let "M" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "v" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Const "M")); func  :::"Section":::  "(" "H" "," "v" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" "M" equals :: ZF_FUND2:def 1  "{"  (Set (Var "m")) where m "is"    ($#m1_subset_1 :::"Element"::: )   "of" "M" : (Bool "M" "," (Set "v"  ($#k2_zf_lang1 :::"/"::: )   "(" (Set  "("  ($#k2_zf_lang :::"x."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set (Var "m")) ")" )  ($#r1_zf_model :::"|="::: )  "H")  "}"   if (Bool (Set   ($#k2_zf_lang :::"x."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_zf_model :::"Free"::: )  "H"))  otherwise (Set   ($#k1_xboole_0 :::"{}"::: )  ); end; 







:: deftheorem    defines :::"Section"::: ZF_FUND2:def 1 :  (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("   "("  (Bool (Bool (Set   ($#k2_zf_lang :::"x."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_zf_model :::"Free"::: )  (Set (Var "H"))))) "implies" (Bool (Set   ($#k1_zf_fund2 :::"Section"::: )   "(" (Set (Var "H")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "m")) where m "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "M")) : (Bool (Set (Var "M")) "," (Set (Set (Var "v"))  ($#k2_zf_lang1 :::"/"::: )   "(" (Set  "("  ($#k2_zf_lang :::"x."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set (Var "m")) ")" )  ($#r1_zf_model :::"|="::: )  (Set (Var "H")))  "}"  )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k2_zf_lang :::"x."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_zf_model :::"Free"::: )  (Set (Var "H")))))) "implies" (Bool (Set   ($#k1_zf_fund2 :::"Section"::: )   "(" (Set (Var "H")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")"   ")" )))); 
 definitionlet "M" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; attr "M" is  :::"predicatively_closed":::  means :: ZF_FUND2: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"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "E"))  "st" (Bool (Bool (Set (Var "E"))  ($#r2_hidden :::"in"::: )  "M")) "holds"  (Bool (Set   ($#k1_zf_fund2 :::"Section"::: )   "(" (Set (Var "H")) "," (Set (Var "f")) ")" )  ($#r2_hidden :::"in"::: )  "M")))); end; 




:: deftheorem    defines :::"predicatively_closed"::: ZF_FUND2:def 2 :  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "M")) "is"   ($#v1_zf_fund2 :::"predicatively_closed"::: )  ) "iff" (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 (Var "E"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool (Set   ($#k1_zf_fund2 :::"Section"::: )   "(" (Set (Var "H")) "," (Set (Var "f")) ")" )  ($#r2_hidden :::"in"::: )  (Set (Var "M"))))))  ")" )); 
 
theorem :: ZF_FUND2:1 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "e")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (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 "E")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  )) "holds"  (Bool (Set   ($#k1_zf_fund2 :::"Section"::: )   "(" (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  "(" (Set  "("  ($#k2_zf_lang :::"x."::: )  (Num 2) ")" )  ($#k5_zf_lang :::"'in'"::: )  (Set  "("  ($#k2_zf_lang :::"x."::: )  (Num 1) ")" ) ")" ) ")" ) ")"  ")" ) "," (Set  "(" (Set (Var "f"))  ($#k2_zf_lang1 :::"/"::: )   "(" (Set  "("  ($#k2_zf_lang :::"x."::: )  (Num 1) ")" ) "," (Set (Var "e")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "E"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "e")) ")" )))))) ; 
 


















theorem :: ZF_FUND2:2 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"DOMAIN-Sequence":::) "of" (Set (Var "W"))  "st" (Bool (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "b"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) "holds"   (Bool  "("  (Bool (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "a")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_zf_refle :::"Union"::: )  (Set (Var "L")))) & (Bool (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "a"))) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  )  ")" )  ")" ) & (Bool (Set   ($#k4_zf_refle :::"Union"::: )  (Set (Var "L"))) "is"   ($#v1_zf_fund2 :::"predicatively_closed"::: )  )) "holds"  (Bool (Set   ($#k4_zf_refle :::"Union"::: )  (Set (Var "L")))  ($#r2_zf_model :::"|="::: )  (Set   ($#k10_zf_model :::"the_axiom_of_power_sets"::: )  )))) ; 
 
theorem :: ZF_FUND2:3 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"DOMAIN-Sequence":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "b"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "a")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "a")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) "holds"   (Bool  "("  (Bool (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "a")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_zf_refle :::"Union"::: )  (Set (Var "L")))) & (Bool (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "a"))) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  )  ")" )  ")" ) & (Bool (Set   ($#k4_zf_refle :::"Union"::: )  (Set (Var "L"))) "is"   ($#v1_zf_fund2 :::"predicatively_closed"::: )  )) "holds"  (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   ($#k4_zf_refle :::"Union"::: )  (Set (Var "L")))  ($#r2_zf_model :::"|="::: )  (Set   ($#k11_zf_model :::"the_axiom_of_substitution_for"::: )  (Set (Var "H"))))))) ; 
 
theorem :: ZF_FUND2:4 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"  (Bool (Set   ($#k1_zf_fund2 :::"Section"::: )   "(" (Set (Var "H")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "m")) where m "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "M")) : (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "m")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set  "(" (Set (Var "v"))  ($#k1_partfun1 :::"*"::: )  (Set  ($#k2_zf_fund1 :::"decode"::: ) ) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set  "("  ($#k4_zf_fund1 :::"code"::: )  (Set  "("  ($#k2_zf_model :::"Free"::: )  (Set (Var "H")) ")" ) ")" )  ($#k7_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_zf_fund1 :::"Diagram"::: )   "(" (Set (Var "H")) "," (Set (Var "M")) ")" ))  "}"  )))) ; 
 
theorem :: ZF_FUND2:5 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subclass":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "Y")) "is"   ($#v8_zf_fund1 :::"closed_wrt_A1-A7"::: )  ) & (Bool (Set (Var "Y")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  )) "holds"  (Bool (Set (Var "Y")) "is"   ($#v1_zf_fund2 :::"predicatively_closed"::: )  ))) ; 
 
theorem :: ZF_FUND2:6 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"DOMAIN-Sequence":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "b"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "a")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "a")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) "holds"   (Bool  "("  (Bool (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "a")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_zf_refle :::"Union"::: )  (Set (Var "L")))) & (Bool (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "a"))) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  )  ")" )  ")" ) & (Bool (Set   ($#k4_zf_refle :::"Union"::: )  (Set (Var "L"))) "is"   ($#v8_zf_fund1 :::"closed_wrt_A1-A7"::: )  )) "holds"  (Bool (Set   ($#k4_zf_refle :::"Union"::: )  (Set (Var "L"))) "is"   ($#v1_zf_model :::"being_a_model_of_ZF"::: )  ))) ;