:: ZFREFLE1 semantic presentation begin definitionlet "M" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_zf_lang :::"WFF"::: ) ); pred "M" :::"|="::: "F" means :: ZFREFLE1:def 1 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool "M" ($#r2_zf_model :::"|="::: ) (Set (Var "H")))); end; :: deftheorem defines :::"|="::: ZFREFLE1:def 1 : (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_zf_lang :::"WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_zfrefle1 :::"|="::: ) (Set (Var "F"))) "iff" (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set (Var "H")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "M")) ($#r2_zf_model :::"|="::: ) (Set (Var "H")))) ")" ))); definitionlet "M1", "M2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; pred "M1" :::"<==>"::: "M2" means :: ZFREFLE1:def 2 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool "M1" ($#r2_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool "M2" ($#r2_zf_model :::"|="::: ) (Set (Var "H"))) ")" )); reflexivity (Bool "for" (Set (Var "M1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r2_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "M1")) ($#r2_zf_model :::"|="::: ) (Set (Var "H"))) ")" ))) ; symmetry (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r2_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "M2")) ($#r2_zf_model :::"|="::: ) (Set (Var "H"))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "M2")) ($#r2_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "M1")) ($#r2_zf_model :::"|="::: ) (Set (Var "H"))) ")" ))) ; pred "M1" :::"is_elementary_subsystem_of"::: "M2" means :: ZFREFLE1:def 3 (Bool "(" (Bool "M1" ($#r1_tarski :::"c="::: ) "M2") & (Bool "(" "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," "M1" "holds" (Bool "(" (Bool "M1" "," (Set (Var "v")) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool "M2" "," (Set "M2" ($#k1_zf_lang1 :::"!"::: ) (Set (Var "v"))) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) ")" )) ")" ) ")" ); reflexivity (Bool "for" (Set (Var "M1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r1_tarski :::"c="::: ) (Set (Var "M1"))) & (Bool "(" "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M1")) "holds" (Bool "(" (Bool (Set (Var "M1")) "," (Set (Var "v")) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "M1")) "," (Set (Set (Var "M1")) ($#k1_zf_lang1 :::"!"::: ) (Set (Var "v"))) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) ")" )) ")" ) ")" )) ; end; :: deftheorem defines :::"<==>"::: ZFREFLE1:def 2 : (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r2_zfrefle1 :::"<==>"::: ) (Set (Var "M2"))) "iff" (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r2_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "M2")) ($#r2_zf_model :::"|="::: ) (Set (Var "H"))) ")" )) ")" )); :: deftheorem defines :::"is_elementary_subsystem_of"::: ZFREFLE1:def 3 : (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r3_zfrefle1 :::"is_elementary_subsystem_of"::: ) (Set (Var "M2"))) "iff" (Bool "(" (Bool (Set (Var "M1")) ($#r1_tarski :::"c="::: ) (Set (Var "M2"))) & (Bool "(" "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M1")) "holds" (Bool "(" (Bool (Set (Var "M1")) "," (Set (Var "v")) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "M2")) "," (Set (Set (Var "M2")) ($#k1_zf_lang1 :::"!"::: ) (Set (Var "v"))) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) ")" )) ")" ) ")" ) ")" )); definitionfunc :::"ZF-axioms"::: -> ($#m1_hidden :::"set"::: ) means :: ZFREFLE1:def 4 (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k9_zf_lang :::"WFF"::: ) )) & (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k6_zf_model :::"the_axiom_of_extensionality"::: ) )) "or" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k7_zf_model :::"the_axiom_of_pairs"::: ) )) "or" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k8_zf_model :::"the_axiom_of_unions"::: ) )) "or" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k9_zf_model :::"the_axiom_of_infinity"::: ) )) "or" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k10_zf_model :::"the_axiom_of_power_sets"::: ) )) "or" (Bool "ex" (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")))) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k11_zf_model :::"the_axiom_of_substitution_for"::: ) (Set (Var "H")))) ")" )) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"ZF-axioms"::: ZFREFLE1:def 4 : (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_zfrefle1 :::"ZF-axioms"::: ) )) "iff" (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k9_zf_lang :::"WFF"::: ) )) & (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k6_zf_model :::"the_axiom_of_extensionality"::: ) )) "or" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k7_zf_model :::"the_axiom_of_pairs"::: ) )) "or" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k8_zf_model :::"the_axiom_of_unions"::: ) )) "or" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k9_zf_model :::"the_axiom_of_infinity"::: ) )) "or" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k10_zf_model :::"the_axiom_of_power_sets"::: ) )) "or" (Bool "ex" (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")))) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k11_zf_model :::"the_axiom_of_substitution_for"::: ) (Set (Var "H")))) ")" )) ")" ) ")" ) ")" )) ")" )); definition:: original: :::"ZF-axioms"::: redefine func :::"ZF-axioms"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_zf_lang :::"WFF"::: ) ); end; theorem :: ZFREFLE1:1 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "M")) ($#r1_zfrefle1 :::"|="::: ) (Set ($#k1_subset_1 :::"{}"::: ) (Set ($#k9_zf_lang :::"WFF"::: ) )))) ; theorem :: ZFREFLE1:2 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_zf_lang :::"WFF"::: ) ) "st" (Bool (Bool (Set (Var "F1")) ($#r1_tarski :::"c="::: ) (Set (Var "F2"))) & (Bool (Set (Var "M")) ($#r1_zfrefle1 :::"|="::: ) (Set (Var "F2")))) "holds" (Bool (Set (Var "M")) ($#r1_zfrefle1 :::"|="::: ) (Set (Var "F1"))))) ; theorem :: ZFREFLE1:3 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_zf_lang :::"WFF"::: ) ) "st" (Bool (Bool (Set (Var "M")) ($#r1_zfrefle1 :::"|="::: ) (Set (Var "F1"))) & (Bool (Set (Var "M")) ($#r1_zfrefle1 :::"|="::: ) (Set (Var "F2")))) "holds" (Bool (Set (Var "M")) ($#r1_zfrefle1 :::"|="::: ) (Set (Set (Var "F1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "F2")))))) ; theorem :: ZFREFLE1:4 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "M")) "is" ($#v1_zf_model :::"being_a_model_of_ZF"::: ) )) "holds" (Bool (Set (Var "M")) ($#r1_zfrefle1 :::"|="::: ) (Set ($#k2_zfrefle1 :::"ZF-axioms"::: ) ))) ; theorem :: ZFREFLE1:5 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "M")) ($#r1_zfrefle1 :::"|="::: ) (Set ($#k2_zfrefle1 :::"ZF-axioms"::: ) )) & (Bool (Set (Var "M")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#v1_zf_model :::"being_a_model_of_ZF"::: ) )) ; theorem :: ZFREFLE1:6 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "ex" (Set (Var "S")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool "(" (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r2_zf_model :::"|="::: ) (Set (Var "S"))) "iff" (Bool (Set (Var "M")) ($#r2_zf_model :::"|="::: ) (Set (Var "H"))) ")" ) ")" ) ")" ))) ; theorem :: ZFREFLE1:7 (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r2_zfrefle1 :::"<==>"::: ) (Set (Var "M2"))) "iff" (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r2_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "M2")) ($#r2_zf_model :::"|="::: ) (Set (Var "H"))) ")" )) ")" )) ; theorem :: ZFREFLE1:8 (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r2_zfrefle1 :::"<==>"::: ) (Set (Var "M2"))) "iff" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k9_zf_lang :::"WFF"::: ) ) "holds" (Bool "(" (Bool (Set (Var "M1")) ($#r1_zfrefle1 :::"|="::: ) (Set (Var "F"))) "iff" (Bool (Set (Var "M2")) ($#r1_zfrefle1 :::"|="::: ) (Set (Var "F"))) ")" )) ")" )) ; theorem :: ZFREFLE1:9 (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "M1")) ($#r3_zfrefle1 :::"is_elementary_subsystem_of"::: ) (Set (Var "M2")))) "holds" (Bool (Set (Var "M1")) ($#r2_zfrefle1 :::"<==>"::: ) (Set (Var "M2")))) ; theorem :: ZFREFLE1:10 (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v1_zf_model :::"being_a_model_of_ZF"::: ) ) & (Bool (Set (Var "M1")) ($#r2_zfrefle1 :::"<==>"::: ) (Set (Var "M2"))) & (Bool (Set (Var "M2")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool (Set (Var "M2")) "is" ($#v1_zf_model :::"being_a_model_of_ZF"::: ) )) ; theorem :: ZFREFLE1:11 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "W")))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set (Var "W"))))) ; theorem :: ZFREFLE1:12 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "X")) "," (Set (Var "Y")) ($#r2_tarski :::"are_equipotent"::: ) ) "or" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "Y")))) ")" )) "holds" (Bool "(" (Bool (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "X"))) "," (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "Y"))) ($#r2_tarski :::"are_equipotent"::: ) ) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "Y")) ")" ))) ")" )) ; theorem :: ZFREFLE1:13 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Phi")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_ordinal1 :::"On"::: ) (Set (Var "W")) ")" ) "," (Set "(" ($#k2_ordinal1 :::"On"::: ) (Set (Var "W")) ")" ) ")" ")" ) "st" (Bool (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "D"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "W"))))) "holds" (Bool "ex" (Set (Var "phi")) "being" ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "W")) "st" (Bool "(" (Bool (Set (Var "phi")) "is" ($#v2_ordinal2 :::"increasing"::: ) ) & (Bool (Set (Var "phi")) "is" ($#v3_ordinal2 :::"continuous"::: ) ) & (Bool (Set (Set (Var "phi")) ($#k4_ordinal4 :::"."::: ) (Set "(" ($#k2_ordinal4 :::"0-element_of"::: ) (Set (Var "W")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_ordinal4 :::"0-element_of"::: ) (Set (Var "W")))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) "holds" (Bool (Set (Set (Var "phi")) ($#k4_ordinal4 :::"."::: ) (Set "(" ($#k6_ordinal4 :::"succ"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_ordinal2 :::"sup"::: ) (Set "(" (Set ($#k1_classes2 :::"{"::: ) (Set "(" (Set (Var "phi")) ($#k4_ordinal4 :::"."::: ) (Set (Var "a")) ")" ) ($#k1_classes2 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k13_funct_5 :::"uncurry"::: ) (Set (Var "Phi")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set ($#k1_classes2 :::"{"::: ) (Set "(" ($#k6_ordinal4 :::"succ"::: ) (Set (Var "a")) ")" ) ($#k1_classes2 :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_ordinal4 :::"0-element_of"::: ) (Set (Var "W")))) & (Bool (Set (Var "a")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "phi")) ($#k4_ordinal4 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_ordinal2 :::"sup"::: ) (Set "(" (Set (Var "phi")) ($#k5_relat_1 :::"|"::: ) (Set (Var "a")) ")" ))) ")" ) ")" ))))) ; theorem :: ZFREFLE1:14 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "phi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Set (Var "phi")) "is" ($#v2_ordinal2 :::"increasing"::: ) )) "holds" (Bool (Set (Set (Var "C")) ($#k1_ordinal3 :::"+^"::: ) (Set (Var "phi"))) "is" ($#v2_ordinal2 :::"increasing"::: ) ))) ; theorem :: ZFREFLE1:15 (Bool "for" (Set (Var "C")) "," (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "xi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "holds" (Bool (Set (Set "(" (Set (Var "C")) ($#k1_ordinal3 :::"+^"::: ) (Set (Var "xi")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k1_ordinal3 :::"+^"::: ) (Set "(" (Set (Var "xi")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ))))) ; theorem :: ZFREFLE1:16 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "phi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Set (Var "phi")) "is" ($#v2_ordinal2 :::"increasing"::: ) ) & (Bool (Set (Var "phi")) "is" ($#v3_ordinal2 :::"continuous"::: ) )) "holds" (Bool (Set (Set (Var "C")) ($#k1_ordinal3 :::"+^"::: ) (Set (Var "phi"))) "is" ($#v3_ordinal2 :::"continuous"::: ) ))) ; theorem :: ZFREFLE1:17 (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "psi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "psi"))))) "holds" (Bool (Set (Var "e")) "is" ($#m1_hidden :::"Ordinal":::)))) ; theorem :: ZFREFLE1:18 (Bool "for" (Set (Var "psi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "psi"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_ordinal2 :::"sup"::: ) (Set (Var "psi"))))) ; theorem :: ZFREFLE1:19 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "A")) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Set (Var "C")))) ; theorem :: ZFREFLE1:20 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "B")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "A")))) ; theorem :: ZFREFLE1:21 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) ; theorem :: ZFREFLE1:22 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "psi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "psi"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "psi"))) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) ) & (Bool (Set (Var "psi")) "is" ($#v2_ordinal2 :::"increasing"::: ) ) & (Bool (Set (Var "A")) ($#r1_ordinal2 :::"is_limes_of"::: ) (Set (Var "psi")))) "holds" (Bool (Set (Var "A")) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "psi")))))) ; theorem :: ZFREFLE1:23 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A"))) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Num 1))) ; theorem :: ZFREFLE1:24 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "B"))))) "holds" (Bool "ex" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C")))))) ; theorem :: ZFREFLE1:25 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) ) "iff" (Bool (Set (Var "B")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) ) ")" )) ; theorem :: ZFREFLE1:26 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: ZFREFLE1:27 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) "holds" (Bool (Bool "not" (Set ($#k2_ordinal1 :::"On"::: ) (Set (Var "W"))) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Set (Var "a")))))) ; theorem :: ZFREFLE1:28 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "phi")) "being" ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "phi")) "is" ($#v2_ordinal2 :::"increasing"::: ) ) & (Bool (Set (Var "phi")) "is" ($#v3_ordinal2 :::"continuous"::: ) )) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Set (Var "phi")) ($#k4_ordinal4 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ))))) ; theorem :: ZFREFLE1:29 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "phi")) "being" ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "phi")) "is" ($#v2_ordinal2 :::"increasing"::: ) ) & (Bool (Set (Var "phi")) "is" ($#v3_ordinal2 :::"continuous"::: ) )) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "phi")) ($#k4_ordinal4 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) ")" ))))) ; theorem :: ZFREFLE1:30 (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")) ")" ))) ")" )) "holds" (Bool "ex" (Set (Var "phi")) "being" ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "W")) "st" (Bool "(" (Bool (Set (Var "phi")) "is" ($#v2_ordinal2 :::"increasing"::: ) ) & (Bool (Set (Var "phi")) "is" ($#v3_ordinal2 :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Set (Var "phi")) ($#k4_ordinal4 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "L")) ($#k5_zf_refle :::"."::: ) (Set (Var "a"))) ($#r3_zfrefle1 :::"is_elementary_subsystem_of"::: ) (Set ($#k4_zf_refle :::"Union"::: ) (Set (Var "L")))) ")" ) ")" )))) ; theorem :: ZFREFLE1:31 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) "holds" (Bool (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set (Var "W"))))) ; theorem :: ZFREFLE1:32 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) (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 :::"{}"::: ) ))) "holds" (Bool (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "a"))) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "W"))))) ; theorem :: ZFREFLE1:33 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) "st" (Bool (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool "ex" (Set (Var "phi")) "being" ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "W")) "st" (Bool "(" (Bool (Set (Var "phi")) "is" ($#v2_ordinal2 :::"increasing"::: ) ) & (Bool (Set (Var "phi")) "is" ($#v3_ordinal2 :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "phi")) ($#k4_ordinal4 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "M")) ($#r3_zfrefle1 :::"is_elementary_subsystem_of"::: ) (Set (Var "W")))) ")" ) ")" ))) ; theorem :: ZFREFLE1:34 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))(Bool "ex" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "b")))) & (Bool (Set (Var "M")) ($#r3_zfrefle1 :::"is_elementary_subsystem_of"::: ) (Set (Var "W"))) ")" ))))) ; theorem :: ZFREFLE1:35 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) "st" (Bool (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))(Bool "ex" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) & (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "a")))) & (Bool (Set (Var "M")) ($#r3_zfrefle1 :::"is_elementary_subsystem_of"::: ) (Set (Var "W"))) ")" )))) ; theorem :: ZFREFLE1:36 (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")) ")" ))) ")" )) "holds" (Bool "ex" (Set (Var "phi")) "being" ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "W")) "st" (Bool "(" (Bool (Set (Var "phi")) "is" ($#v2_ordinal2 :::"increasing"::: ) ) & (Bool (Set (Var "phi")) "is" ($#v3_ordinal2 :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Set (Var "phi")) ($#k4_ordinal4 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "L")) ($#k5_zf_refle :::"."::: ) (Set (Var "a"))) ($#r2_zfrefle1 :::"<==>"::: ) (Set ($#k4_zf_refle :::"Union"::: ) (Set (Var "L")))) ")" ) ")" )))) ; theorem :: ZFREFLE1:37 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) "st" (Bool (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool "ex" (Set (Var "phi")) "being" ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "W")) "st" (Bool "(" (Bool (Set (Var "phi")) "is" ($#v2_ordinal2 :::"increasing"::: ) ) & (Bool (Set (Var "phi")) "is" ($#v3_ordinal2 :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "phi")) ($#k4_ordinal4 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "M")) ($#r2_zfrefle1 :::"<==>"::: ) (Set (Var "W")))) ")" ) ")" ))) ; theorem :: ZFREFLE1:38 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))(Bool "ex" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "b"))) & (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "b")))) & (Bool (Set (Var "M")) ($#r2_zfrefle1 :::"<==>"::: ) (Set (Var "W"))) ")" ))))) ; theorem :: ZFREFLE1:39 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) "st" (Bool (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))(Bool "ex" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) & (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "a")))) & (Bool (Set (Var "M")) ($#r2_zfrefle1 :::"<==>"::: ) (Set (Var "W"))) ")" )))) ; theorem :: ZFREFLE1:40 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) "st" (Bool (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))(Bool "ex" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) & (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "a")))) & (Bool (Set (Var "M")) "is" ($#v1_zf_model :::"being_a_model_of_ZF"::: ) ) ")" )))) ; theorem :: ZFREFLE1:41 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Universe":::) "st" (Bool (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool "ex" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "M")) "is" ($#v1_zf_model :::"being_a_model_of_ZF"::: ) ) ")" )))) ;