:: CLASSES1 semantic presentation begin definitionlet "B" be ($#m1_hidden :::"set"::: ) ; attr "B" is :::"subset-closed"::: means :: CLASSES1:def 1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) "B") & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) "B")); end; :: deftheorem defines :::"subset-closed"::: CLASSES1:def 1 : (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v1_classes1 :::"subset-closed"::: ) ) "iff" (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) ")" )); definitionlet "B" be ($#m1_hidden :::"set"::: ) ; attr "B" is :::"Tarski"::: means :: CLASSES1:def 2 (Bool "(" (Bool "B" "is" ($#v1_classes1 :::"subset-closed"::: ) ) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) "B")) "holds" (Bool (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) "B") ")" ) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) "B") "or" (Bool (Set (Var "X")) "," "B" ($#r2_tarski :::"are_equipotent"::: ) ) "or" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) "B") ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Tarski"::: CLASSES1:def 2 : (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v2_classes1 :::"Tarski"::: ) ) "iff" (Bool "(" (Bool (Set (Var "B")) "is" ($#v1_classes1 :::"subset-closed"::: ) ) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) "or" (Bool (Set (Var "X")) "," (Set (Var "B")) ($#r2_tarski :::"are_equipotent"::: ) ) "or" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) ")" ) ")" ) ")" )); definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; pred "B" :::"is_Tarski-Class_of"::: "A" means :: CLASSES1:def 3 (Bool "(" (Bool "A" ($#r2_hidden :::"in"::: ) "B") & (Bool "B" "is" ($#v2_classes1 :::"Tarski"::: ) ) ")" ); end; :: deftheorem defines :::"is_Tarski-Class_of"::: CLASSES1:def 3 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r1_classes1 :::"is_Tarski-Class_of"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) "is" ($#v2_classes1 :::"Tarski"::: ) ) ")" ) ")" )); definitionlet "A" be ($#m1_hidden :::"set"::: ) ; func :::"Tarski-Class"::: "A" -> ($#m1_hidden :::"set"::: ) means :: CLASSES1:def 4 (Bool "(" (Bool it ($#r1_classes1 :::"is_Tarski-Class_of"::: ) "A") & (Bool "(" "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "D")) ($#r1_classes1 :::"is_Tarski-Class_of"::: ) "A")) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ); end; :: deftheorem defines :::"Tarski-Class"::: CLASSES1:def 4 : (Bool "for" (Set (Var "A")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set (Var "b2")) ($#r1_classes1 :::"is_Tarski-Class_of"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "D")) ($#r1_classes1 :::"is_Tarski-Class_of"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "b2")) ($#r1_tarski :::"c="::: ) (Set (Var "D"))) ")" ) ")" ) ")" )); registrationlet "A" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_classes1 :::"Tarski-Class"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: CLASSES1:1 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v2_classes1 :::"Tarski"::: ) ) "iff" (Bool "(" (Bool (Set (Var "W")) "is" ($#v1_classes1 :::"subset-closed"::: ) ) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "W")))) "holds" (Bool (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) ")" ) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "W"))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "W"))) ")" ) ")" ) ")" )) ; theorem :: CLASSES1:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))))) ; theorem :: CLASSES1:3 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))))) ; theorem :: CLASSES1:4 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))))) "holds" (Bool (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "Y"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))))) ; theorem :: CLASSES1:5 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")))) "or" (Bool (Set (Var "Y")) "," (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))) ($#r2_tarski :::"are_equipotent"::: ) ) "or" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")))) ")" )) ; theorem :: CLASSES1:6 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "Y"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"Ordinal":::); func :::"Tarski-Class"::: "(" "X" "," "A" ")" -> ($#m1_hidden :::"set"::: ) means :: CLASSES1:def 5 (Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "L")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "A")) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) "X" ($#k1_tarski :::"}"::: ) )) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "A"))) "holds" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "{" (Set (Var "u")) where u "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_classes1 :::"Tarski-Class"::: ) "X") : (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_classes1 :::"Tarski-Class"::: ) "X") "st" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")))) & (Bool (Set (Var "u")) ($#r1_tarski :::"c="::: ) (Set (Var "v"))) ")" )) "}" ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "v")) ")" ) where v "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_classes1 :::"Tarski-Class"::: ) "X") : (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")))) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k1_classes1 :::"Tarski-Class"::: ) "X" ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "A")) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "L")) ($#k5_relat_1 :::"|"::: ) (Set (Var "C")) ")" ) ")" ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_classes1 :::"Tarski-Class"::: ) "X" ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"Tarski-Class"::: CLASSES1:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" )) "iff" (Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "L")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) )) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "{" (Set (Var "u")) where u "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))) : (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))) "st" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")))) & (Bool (Set (Var "u")) ($#r1_tarski :::"c="::: ) (Set (Var "v"))) ")" )) "}" ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "v")) ")" ) where v "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))) : (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")))) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")) ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "L")) ($#k5_relat_1 :::"|"::: ) (Set (Var "C")) ")" ) ")" ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")) ")" ))) ")" ) ")" )) ")" )))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"Ordinal":::); :: original: :::"Tarski-Class"::: redefine func :::"Tarski-Class"::: "(" "X" "," "A" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k1_classes1 :::"Tarski-Class"::: ) "X" ")" ); end; theorem :: CLASSES1:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: CLASSES1:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "{" (Set (Var "u")) where u "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))) : (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))) "st" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" )) & (Bool (Set (Var "u")) ($#r1_tarski :::"c="::: ) (Set (Var "v"))) ")" )) "}" ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "v")) ")" ) where v "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))) : (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" )) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "(" ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ")" ) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")) ")" ) ")" ))))) ; theorem :: CLASSES1:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "u")) where u "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))) : (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "B")) ")" )) ")" )) "}" ))) ; theorem :: CLASSES1:10 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" ) ")" )) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" )) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")))) ")" ) "or" (Bool "ex" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" )) & (Bool "(" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) "or" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "Z")))) ")" ) ")" )) ")" ) ")" ))) ; theorem :: CLASSES1:11 (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ))) "holds" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" ) ")" )))) ; theorem :: CLASSES1:12 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ))) "holds" (Bool (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "Y"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" ) ")" )))) ; theorem :: CLASSES1:13 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" )) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "B")) ")" )) ")" )) ")" ))) ; theorem :: CLASSES1:14 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) ) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" )) & (Bool "(" (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) "or" (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "Y")))) ")" )) "holds" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" )))) ; theorem :: CLASSES1:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" ) ")" )))) ; theorem :: CLASSES1:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "B")) ")" )))) ; theorem :: CLASSES1:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" ) ")" )))) ; theorem :: CLASSES1:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" ) ")" ))) "holds" (Bool (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")))))) ; theorem :: CLASSES1:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")))))) ; theorem :: CLASSES1:20 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")))) ")" ) ")" ))) ; theorem :: CLASSES1:21 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set (Var "X"))) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))))) "holds" (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Bool "not" (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ))) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" ) ")" )) ")" ))) ; theorem :: CLASSES1:22 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k3_classes1 :::"Tarski-Class"::: ) "(" (Set (Var "X")) "," (Set (Var "A")) ")" ) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) ))) ; theorem :: CLASSES1:23 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) ; theorem :: CLASSES1:24 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))))) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "Y"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")) ")" )))) ; theorem :: CLASSES1:25 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))))) "holds" (Bool "not" (Bool (Set (Var "Y")) "," (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))) ($#r2_tarski :::"are_equipotent"::: ) ))) ; theorem :: CLASSES1:26 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))))) "holds" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")))) & (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")))) ")" )) ; theorem :: CLASSES1:27 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))))) ; theorem :: CLASSES1:28 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")))) & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))))) "holds" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))))) ; definitionlet "A" be ($#m1_hidden :::"Ordinal":::); func :::"Rank"::: "A" -> ($#m1_hidden :::"set"::: ) means :: CLASSES1:def 6 (Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "L")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "A")) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "A"))) "holds" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) "A")) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "L")) ($#k5_relat_1 :::"|"::: ) (Set (Var "C")) ")" ) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"Rank"::: CLASSES1:def 6 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "L")) "being" ($#m1_hidden :::"T-Sequence":::) "st" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal2 :::"last"::: ) (Set (Var "L")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "(" (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "C")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "C")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "L")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "L")) ($#k5_relat_1 :::"|"::: ) (Set (Var "C")) ")" ) ")" ))) ")" ) ")" )) ")" ))); theorem :: CLASSES1:29 (Bool (Set ($#k4_classes1 :::"Rank"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; theorem :: CLASSES1:30 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k4_classes1 :::"Rank"::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set "(" ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")) ")" )))) ; theorem :: CLASSES1:31 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "B")))) ")" )) ")" ))) ; theorem :: CLASSES1:32 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))) "iff" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" ))) ")" ))) ; registrationlet "A" be ($#m1_hidden :::"Ordinal":::); cluster (Set ($#k4_classes1 :::"Rank"::: ) "A") -> ($#v1_ordinal1 :::"epsilon-transitive"::: ) ; end; theorem :: CLASSES1:33 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" )))) ; theorem :: CLASSES1:34 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A"))))) ; theorem :: CLASSES1:35 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))))) ; theorem :: CLASSES1:36 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) "iff" (Bool (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "B")))) ")" )) ; theorem :: CLASSES1:37 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "B"))) "iff" (Bool (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "B")))) ")" )) ; theorem :: CLASSES1:38 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A"))))) ; theorem :: CLASSES1:39 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "X")) "," (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A"))) ($#r2_tarski :::"are_equipotent"::: ) )) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")) ")" ))) ")" ))) ; theorem :: CLASSES1:40 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))) "iff" (Bool (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" ))) ")" ))) ; theorem :: CLASSES1:41 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))))) ; theorem :: CLASSES1:42 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))) "iff" (Bool (Set ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" ))) ")" ))) ; theorem :: CLASSES1:43 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))) "iff" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" ))) ")" ))) ; theorem :: CLASSES1:44 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))) ")" ) "iff" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" ))) ")" ))) ; theorem :: CLASSES1:45 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))) ")" ) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" ) ")" ))) ")" ))) ; theorem :: CLASSES1:46 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) ) & (Bool (Set (Set "(" ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_classes1 :::"Rank"::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A")) ")" ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))))) ; theorem :: CLASSES1:47 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))))) ; theorem :: CLASSES1:48 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) ; theorem :: CLASSES1:49 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y"))) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) ; theorem :: CLASSES1:50 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y"))) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"the_transitive-closure_of"::: "X" -> ($#m1_hidden :::"set"::: ) means :: CLASSES1:def 7 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::)(Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_ordinal1 :::"omega"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ($#r1_hidden :::"="::: ) "X") & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ))) ")" ) ")" ))) ")" )); end; :: deftheorem defines :::"the_transitive-closure_of"::: CLASSES1:def 7 : (Bool "for" (Set (Var "X")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::)(Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_ordinal1 :::"omega"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ))) ")" ) ")" ))) ")" )) ")" )); theorem :: CLASSES1:51 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set (Var "X"))) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) ; theorem :: CLASSES1:52 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set (Var "X"))))) ; theorem :: CLASSES1:53 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool (Set ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) ; theorem :: CLASSES1:54 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Var "Z")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) ")" ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "Y")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool (Set ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) ; theorem :: CLASSES1:55 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_ordinal1 :::"epsilon-transitive"::: ) )) "holds" (Bool (Set ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) ; theorem :: CLASSES1:56 (Bool (Set ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; theorem :: CLASSES1:57 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) ; theorem :: CLASSES1:58 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set (Var "Y"))))) ; theorem :: CLASSES1:59 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set "(" ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set (Var "X"))))) ; theorem :: CLASSES1:60 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set (Var "X")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set (Var "Y")) ")" )))) ; theorem :: CLASSES1:61 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set (Var "X")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k5_classes1 :::"the_transitive-closure_of"::: ) (Set (Var "Y")) ")" )))) ; theorem :: CLASSES1:62 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"the_rank_of"::: "X" -> ($#m1_hidden :::"Ordinal":::) means :: CLASSES1:def 8 (Bool "(" (Bool "X" ($#r1_tarski :::"c="::: ) (Set ($#k4_classes1 :::"Rank"::: ) it)) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool "X" ($#r1_tarski :::"c="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "B"))))) "holds" (Bool it ($#r1_ordinal1 :::"c="::: ) (Set (Var "B"))) ")" ) ")" ); end; :: deftheorem defines :::"the_rank_of"::: CLASSES1:def 8 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "b2")))) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "b2")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "B"))) ")" ) ")" ) ")" ))); theorem :: CLASSES1:63 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "X")) ")" )))) ; theorem :: CLASSES1:64 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set "(" ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A")))) ; theorem :: CLASSES1:65 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))) "iff" (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "X"))) ($#r1_ordinal1 :::"c="::: ) (Set (Var "A"))) ")" ))) ; theorem :: CLASSES1:66 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set ($#k4_classes1 :::"Rank"::: ) (Set (Var "A")))) "iff" (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))) ; theorem :: CLASSES1:67 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "X"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "Y"))))) ; theorem :: CLASSES1:68 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "Y"))))) ; theorem :: CLASSES1:69 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "X"))) ($#r1_ordinal1 :::"c="::: ) (Set (Var "A"))) "iff" (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "Y"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) ")" ))) ; theorem :: CLASSES1:70 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_ordinal1 :::"c="::: ) (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "B")) ($#r1_ordinal1 :::"c="::: ) (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "Y")))) ")" ))) ")" ))) ; theorem :: CLASSES1:71 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: CLASSES1:72 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" )))) ; theorem :: CLASSES1:73 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) ; theorem :: CLASSES1:74 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set "(" ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set "(" ($#k1_classes1 :::"Tarski-Class"::: ) (Set (Var "X")) ")" )) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) ) ")" )) ; begin scheme :: CLASSES1:sch 1 NonUniqFuncEx{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool P1[(Set (Var "e")) "," (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))]) ")" ) ")" )) provided (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "ex" (Set (Var "u")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool P1[(Set (Var "e")) "," (Set (Var "u"))]))) proof end; definitionlet "F", "G" be ($#m1_hidden :::"Relation":::); pred "F" "," "G" :::"are_fiberwise_equipotent"::: means :: CLASSES1:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k10_relat_1 :::"Coim"::: ) "(" "F" "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k10_relat_1 :::"Coim"::: ) "(" "G" "," (Set (Var "x")) ")" ")" )))); reflexivity (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k10_relat_1 :::"Coim"::: ) "(" (Set (Var "F")) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k10_relat_1 :::"Coim"::: ) "(" (Set (Var "F")) "," (Set (Var "x")) ")" ")" ))))) ; symmetry (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k10_relat_1 :::"Coim"::: ) "(" (Set (Var "F")) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k10_relat_1 :::"Coim"::: ) "(" (Set (Var "G")) "," (Set (Var "x")) ")" ")" ))) ")" )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k10_relat_1 :::"Coim"::: ) "(" (Set (Var "G")) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k10_relat_1 :::"Coim"::: ) "(" (Set (Var "F")) "," (Set (Var "x")) ")" ")" ))))) ; end; :: deftheorem defines :::"are_fiberwise_equipotent"::: CLASSES1:def 9 : (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k10_relat_1 :::"Coim"::: ) "(" (Set (Var "F")) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k10_relat_1 :::"Coim"::: ) "(" (Set (Var "G")) "," (Set (Var "x")) ")" ")" )))) ")" )); theorem :: CLASSES1:75 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "G"))))) ; theorem :: CLASSES1:76 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) & (Bool (Set (Var "F")) "," (Set (Var "H")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool (Set (Var "G")) "," (Set (Var "H")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) ; theorem :: CLASSES1:77 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) "iff" (Bool "ex" (Set (Var "H")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "G")))) & (Bool (Set (Var "H")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_relat_1 :::"*"::: ) (Set (Var "H")))) ")" )) ")" )) ; theorem :: CLASSES1:78 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "F")) ($#k8_relat_1 :::"""::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "G")) ($#k8_relat_1 :::"""::: ) (Set (Var "X")) ")" )))) ")" )) ; theorem :: CLASSES1:79 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_tarski :::"c="::: ) (Set (Var "D"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "G"))) ($#r1_tarski :::"c="::: ) (Set (Var "D"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k10_relat_1 :::"Coim"::: ) "(" (Set (Var "F")) "," (Set (Var "d")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k10_relat_1 :::"Coim"::: ) "(" (Set (Var "G")) "," (Set (Var "d")) ")" ")" ))) ")" )) "holds" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ))) ; theorem :: CLASSES1:80 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "G"))))) "holds" (Bool "(" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) "iff" (Bool "ex" (Set (Var "P")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")) ")" ) "st" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_relat_1 :::"*"::: ) (Set (Var "P"))))) ")" )) ; theorem :: CLASSES1:81 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "G")) ")" )))) ; theorem :: CLASSES1:82 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_classes1 :::"the_rank_of"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )))))) ; theorem :: CLASSES1:83 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h")))) & (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool (Set (Set (Var "h")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) "," (Set (Set (Var "h")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g"))) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) ;