:: CARD_FIL semantic presentation begin theorem :: CARD_FIL:1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X")))))) ; scheme :: CARD_FIL:sch 1 ElemProp{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool P1[(Set F2 "(" ")" )]) provided (Bool (Set F2 "(" ")" ) ($#r2_hidden :::"in"::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "y"))]) "}" ) proof end; theorem :: CARD_FIL:2 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))) & (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ))) & (Bool "(" "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "Y2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ))) "implies" (Bool (Set (Set (Var "Y1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Y2"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) )) ")" & "(" (Bool (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "Y1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y2")))) "implies" (Bool (Set (Var "Y2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) )) ")" ")" ) ")" ) ")" )) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode :::"Filter"::: "of" "X" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" "X" means :: CARD_FIL:def 1 (Bool "(" (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) it)) & (Bool "(" "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "holds" (Bool "(" "(" (Bool (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Var "Y2")) ($#r2_hidden :::"in"::: ) it)) "implies" (Bool (Set (Set (Var "Y1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Y2"))) ($#r2_hidden :::"in"::: ) it) ")" & "(" (Bool (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Var "Y1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y2")))) "implies" (Bool (Set (Var "Y2")) ($#r2_hidden :::"in"::: ) it) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Filter"::: CARD_FIL:def 1 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X"))) "iff" (Bool "(" (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) & (Bool "(" "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool (Set (Var "Y2")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "implies" (Bool (Set (Set (Var "Y1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Y2"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" & "(" (Bool (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool (Set (Var "Y1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y2")))) "implies" (Bool (Set (Var "Y2")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" ")" ) ")" ) ")" ) ")" ))); theorem :: CARD_FIL:3 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))) & (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "Y2")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "implies" (Bool (Set (Set (Var "Y1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Y2"))) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" & "(" (Bool (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "Y1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y2")))) "implies" (Bool (Set (Var "Y2")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ")" ) ")" ) ")" ) ")" ))) ; theorem :: CARD_FIL:4 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")))) ; theorem :: CARD_FIL:5 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))))) ; theorem :: CARD_FIL:6 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool "not" (Bool (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y"))) ($#r2_hidden :::"in"::: ) (Set (Var "F"))))))) ; theorem :: CARD_FIL:7 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) "iff" (Bool (Set (Set (Var "Y")) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" ) ")" )) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) & (Bool "(" "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "Y2")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "implies" (Bool (Set (Set (Var "Y1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y2"))) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) ")" & "(" (Bool (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "Y2")) ($#r1_tarski :::"c="::: ) (Set (Var "Y1")))) "implies" (Bool (Set (Var "Y2")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) ")" ")" ) ")" ) ")" )))) ; notationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); synonym :::"dual"::: "S" for :::"COMPLEMENT"::: "S"; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); cluster (Set ($#k7_setfam_1 :::"dual"::: ) "S") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: CARD_FIL:8 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k7_setfam_1 :::"dual"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "Y")) where Y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set (Set (Var "Y")) ($#k3_subset_1 :::"`"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) "}" ))) ; theorem :: CARD_FIL:9 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k7_setfam_1 :::"dual"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "Y")) ($#k3_subset_1 :::"`"::: ) ")" ) where Y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) "}" ))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode :::"Ideal"::: "of" "X" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" "X" means :: CARD_FIL:def 2 (Bool "(" (Bool (Bool "not" "X" ($#r2_hidden :::"in"::: ) it)) & (Bool "(" "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "holds" (Bool "(" "(" (Bool (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Var "Y2")) ($#r2_hidden :::"in"::: ) it)) "implies" (Bool (Set (Set (Var "Y1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y2"))) ($#r2_hidden :::"in"::: ) it) ")" & "(" (Bool (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Var "Y2")) ($#r1_tarski :::"c="::: ) (Set (Var "Y1")))) "implies" (Bool (Set (Var "Y2")) ($#r2_hidden :::"in"::: ) it) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Ideal"::: CARD_FIL:def 2 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_card_fil :::"Ideal"::: ) "of" (Set (Var "X"))) "iff" (Bool "(" (Bool (Bool "not" (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) & (Bool "(" "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool (Set (Var "Y2")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "implies" (Bool (Set (Set (Var "Y1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "Y2"))) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" & "(" (Bool (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) & (Bool (Set (Var "Y2")) ($#r1_tarski :::"c="::: ) (Set (Var "Y1")))) "implies" (Bool (Set (Var "Y2")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" ")" ) ")" ) ")" ) ")" ))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_card_fil :::"Filter"::: ) "of" (Set (Const "X")); :: original: :::"dual"::: redefine func :::"dual"::: "F" -> ($#m2_card_fil :::"Ideal"::: ) "of" "X"; end; theorem :: CARD_FIL:10 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "I")) "being" ($#m2_card_fil :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" "not" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "or" "not" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_fil :::"dual"::: ) (Set (Var "F")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" "not" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) "or" "not" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k7_setfam_1 :::"dual"::: ) (Set (Var "I")))) ")" ) ")" ) ")" )))) ; theorem :: CARD_FIL:11 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I")) "being" ($#m2_card_fil :::"Ideal"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "I"))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "N" be ($#m1_hidden :::"Cardinal":::); let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); pred "S" :::"is_multiplicative_with"::: "N" means :: CARD_FIL:def 3 (Bool "for" (Set (Var "S1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S1")) ($#r1_tarski :::"c="::: ) "S") & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "S1"))) ($#r2_hidden :::"in"::: ) "N")) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "S1"))) ($#r2_hidden :::"in"::: ) "S")); end; :: deftheorem defines :::"is_multiplicative_with"::: CARD_FIL:def 3 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m1_hidden :::"Cardinal":::) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "S")) ($#r1_card_fil :::"is_multiplicative_with"::: ) (Set (Var "N"))) "iff" (Bool "for" (Set (Var "S1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S1")) ($#r1_tarski :::"c="::: ) (Set (Var "S"))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "S1"))) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "S1"))) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" )))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "N" be ($#m1_hidden :::"Cardinal":::); let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); pred "S" :::"is_additive_with"::: "N" means :: CARD_FIL:def 4 (Bool "for" (Set (Var "S1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S1")) ($#r1_tarski :::"c="::: ) "S") & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "S1"))) ($#r2_hidden :::"in"::: ) "N")) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "S1"))) ($#r2_hidden :::"in"::: ) "S")); end; :: deftheorem defines :::"is_additive_with"::: CARD_FIL:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m1_hidden :::"Cardinal":::) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "S")) ($#r2_card_fil :::"is_additive_with"::: ) (Set (Var "N"))) "iff" (Bool "for" (Set (Var "S1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "S1")) ($#r1_tarski :::"c="::: ) (Set (Var "S"))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "S1"))) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "S1"))) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" )))); notationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "N" be ($#m1_hidden :::"Cardinal":::); let "F" be ($#m1_card_fil :::"Filter"::: ) "of" (Set (Const "X")); synonym "F" :::"is_complete_with"::: "N" for "F" :::"is_multiplicative_with"::: "N"; end; notationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "N" be ($#m1_hidden :::"Cardinal":::); let "I" be ($#m2_card_fil :::"Ideal"::: ) "of" (Set (Const "X")); synonym "I" :::"is_complete_with"::: "N" for "I" :::"is_additive_with"::: "N"; end; theorem :: CARD_FIL:12 (Bool "for" (Set (Var "N")) "being" ($#m1_hidden :::"Cardinal":::) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "S")) ($#r1_card_fil :::"is_multiplicative_with"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k7_setfam_1 :::"dual"::: ) (Set (Var "S"))) ($#r2_card_fil :::"is_additive_with"::: ) (Set (Var "N")))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_card_fil :::"Filter"::: ) "of" (Set (Const "X")); attr "F" is :::"uniform"::: means :: CARD_FIL:def 5 (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) "X"))); attr "F" is :::"principal"::: means :: CARD_FIL:def 6 (Bool "ex" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) "F") & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) "F")) "holds" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) ")" ) ")" )); attr "F" is :::"being_ultrafilter"::: means :: CARD_FIL:def 7 (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) "F") "or" (Bool (Set "X" ($#k6_subset_1 :::"\"::: ) (Set (Var "Y"))) ($#r2_hidden :::"in"::: ) "F") ")" )); end; :: deftheorem defines :::"uniform"::: CARD_FIL:def 5 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_card_fil :::"uniform"::: ) ) "iff" (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))))) ")" ))); :: deftheorem defines :::"principal"::: CARD_FIL:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_card_fil :::"principal"::: ) ) "iff" (Bool "ex" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) ")" ) ")" )) ")" ))); :: deftheorem defines :::"being_ultrafilter"::: CARD_FIL:def 7 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_card_fil :::"being_ultrafilter"::: ) ) "iff" (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "or" (Bool (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y"))) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) ")" )) ")" ))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_card_fil :::"Filter"::: ) "of" (Set (Const "X")); let "Z" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); func :::"Extend_Filter"::: "(" "F" "," "Z" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" "X" equals :: CARD_FIL:def 8 "{" (Set (Var "Y")) where Y "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool "ex" (Set (Var "Y2")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" "st" (Bool "(" (Bool (Set (Var "Y2")) ($#r2_hidden :::"in"::: ) "{" (Set "(" (Set (Var "Y1")) ($#k9_subset_1 :::"/\"::: ) "Z" ")" ) where Y1 "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) "F") "}" ) & (Bool (Set (Var "Y2")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" )) "}" ; end; :: deftheorem defines :::"Extend_Filter"::: CARD_FIL:def 8 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_card_fil :::"Extend_Filter"::: ) "(" (Set (Var "F")) "," (Set (Var "Z")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "Y")) where Y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool "ex" (Set (Var "Y2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "Y2")) ($#r2_hidden :::"in"::: ) "{" (Set "(" (Set (Var "Y1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Z")) ")" ) where Y1 "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "}" ) & (Bool (Set (Var "Y2")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" )) "}" )))); theorem :: CARD_FIL:13 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "Z1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "Z1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_card_fil :::"Extend_Filter"::: ) "(" (Set (Var "F")) "," (Set (Var "Z")) ")" )) "iff" (Bool "ex" (Set (Var "Z2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "Z2")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Set (Var "Z2")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "Z"))) ($#r1_tarski :::"c="::: ) (Set (Var "Z1"))) ")" )) ")" ))))) ; theorem :: CARD_FIL:14 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "Y1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Y1")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "Y1")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Z"))) ")" )) "holds" (Bool "(" (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_card_fil :::"Extend_Filter"::: ) "(" (Set (Var "F")) "," (Set (Var "Z")) ")" )) & (Bool (Set ($#k2_card_fil :::"Extend_Filter"::: ) "(" (Set (Var "F")) "," (Set (Var "Z")) ")" ) "is" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X"))) & (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set ($#k2_card_fil :::"Extend_Filter"::: ) "(" (Set (Var "F")) "," (Set (Var "Z")) ")" )) ")" )))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"Filters"::: "X" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) "X" ")" ) equals :: CARD_FIL:def 9 "{" (Set (Var "S")) where S "is" ($#m1_subset_1 :::"Subset-Family":::) "of" "X" : (Bool (Set (Var "S")) "is" ($#m1_card_fil :::"Filter"::: ) "of" "X") "}" ; end; :: deftheorem defines :::"Filters"::: CARD_FIL:def 9 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_card_fil :::"Filters"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "S")) where S "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) : (Bool (Set (Var "S")) "is" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X"))) "}" )); theorem :: CARD_FIL:15 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) ($#r2_hidden :::"in"::: ) (Set ($#k3_card_fil :::"Filters"::: ) (Set (Var "X")))) "iff" (Bool (Set (Var "S")) "is" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X"))) ")" ))) ; theorem :: CARD_FIL:16 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "FS")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_card_fil :::"Filters"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set (Var "FS")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "FS"))) "is" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X"))))) ; theorem :: CARD_FIL:17 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")) (Bool "ex" (Set (Var "Uf")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "Uf"))) & (Bool (Set (Var "Uf")) "is" ($#v3_card_fil :::"being_ultrafilter"::: ) ) ")" )))) ; definitionlet "X" be ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) ; func :::"Frechet_Filter"::: "X" -> ($#m1_card_fil :::"Filter"::: ) "of" "X" equals :: CARD_FIL:def 10 "{" (Set (Var "Y")) where Y "is" ($#m1_subset_1 :::"Subset":::) "of" "X" : (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" "X" ($#k6_subset_1 :::"\"::: ) (Set (Var "Y")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) "X")) "}" ; end; :: deftheorem defines :::"Frechet_Filter"::: CARD_FIL:def 10 : (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_card_fil :::"Frechet_Filter"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "Y")) where Y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X")))) "}" )); definitionlet "X" be ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) ; func :::"Frechet_Ideal"::: "X" -> ($#m2_card_fil :::"Ideal"::: ) "of" "X" equals :: CARD_FIL:def 11 (Set ($#k1_card_fil :::"dual"::: ) (Set "(" ($#k4_card_fil :::"Frechet_Filter"::: ) "X" ")" )); end; :: deftheorem defines :::"Frechet_Ideal"::: CARD_FIL:def 11 : (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_card_fil :::"Frechet_Ideal"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_fil :::"dual"::: ) (Set "(" ($#k4_card_fil :::"Frechet_Filter"::: ) (Set (Var "X")) ")" )))); theorem :: CARD_FIL:18 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_fil :::"Frechet_Filter"::: ) (Set (Var "X")))) "iff" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y")) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X")))) ")" ))) ; theorem :: CARD_FIL:19 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k5_card_fil :::"Frechet_Ideal"::: ) (Set (Var "X")))) "iff" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "Y"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X")))) ")" ))) ; theorem :: CARD_FIL:20 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k4_card_fil :::"Frechet_Filter"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "F")) "is" ($#v1_card_fil :::"uniform"::: ) ))) ; theorem :: CARD_FIL:21 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Uf")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "Uf")) "is" ($#v1_card_fil :::"uniform"::: ) ) & (Bool (Set (Var "Uf")) "is" ($#v3_card_fil :::"being_ultrafilter"::: ) )) "holds" (Bool (Set ($#k4_card_fil :::"Frechet_Filter"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "Uf"))))) ; registrationlet "X" be ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#~v2_card_fil "non" ($#v2_card_fil :::"principal"::: ) ) ($#v3_card_fil :::"being_ultrafilter"::: ) for ($#m1_card_fil :::"Filter"::: ) "of" "X"; end; registrationlet "X" be ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_card_fil :::"uniform"::: ) ($#v3_card_fil :::"being_ultrafilter"::: ) -> ($#~v2_card_fil "non" ($#v2_card_fil :::"principal"::: ) ) for ($#m1_card_fil :::"Filter"::: ) "of" "X"; end; theorem :: CARD_FIL:22 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_card_fil :::"being_ultrafilter"::: ) ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) "iff" (Bool (Bool "not" (Set (Var "Y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_card_fil :::"dual"::: ) (Set (Var "F"))))) ")" )))) ; theorem :: CARD_FIL:23 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Bool "not" (Set (Var "F")) "is" ($#v2_card_fil :::"principal"::: ) )) & (Bool (Set (Var "F")) "is" ($#v3_card_fil :::"being_ultrafilter"::: ) ) & (Bool (Set (Var "F")) ($#r1_card_fil :::"is_complete_with"::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "F")) "is" ($#v1_card_fil :::"uniform"::: ) ))) ; begin theorem :: CARD_FIL:24 (Bool "for" (Set (Var "N")) "being" ($#m1_hidden :::"Cardinal":::) "holds" (Bool (Set ($#k2_card_1 :::"nextcard"::: ) (Set (Var "N"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k3_card_2 :::"exp"::: ) "(" (Num 2) "," (Set (Var "N")) ")" ))) ; definitionpred :::"GCH"::: means :: CARD_FIL:def 12 (Bool "for" (Set (Var "N")) "being" ($#m1_hidden :::"Aleph":::) "holds" (Bool (Set ($#k2_card_1 :::"nextcard"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k3_card_2 :::"exp"::: ) "(" (Num 2) "," (Set (Var "N")) ")" ))); end; :: deftheorem defines :::"GCH"::: CARD_FIL:def 12 : (Bool "(" (Bool ($#r3_card_fil :::"GCH"::: ) ) "iff" (Bool "for" (Set (Var "N")) "being" ($#m1_hidden :::"Aleph":::) "holds" (Bool (Set ($#k2_card_1 :::"nextcard"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set ($#k3_card_2 :::"exp"::: ) "(" (Num 2) "," (Set (Var "N")) ")" ))) ")" ); definitionlet "IT" be ($#m1_hidden :::"Aleph":::); attr "IT" is :::"inaccessible"::: means :: CARD_FIL:def 13 (Bool "(" (Bool "IT" "is" ($#v1_card_5 :::"regular"::: ) ) & (Bool "IT" "is" ($#v2_card_1 :::"limit_cardinal"::: ) ) ")" ); end; :: deftheorem defines :::"inaccessible"::: CARD_FIL:def 13 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"Aleph":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_card_fil :::"inaccessible"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_card_5 :::"regular"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v2_card_1 :::"limit_cardinal"::: ) ) ")" ) ")" )); registration cluster ($#~v1_finset_1 "non" ($#v1_finset_1 :::"finite"::: ) ) ($#v1_card_1 :::"cardinal"::: ) ($#v4_card_fil :::"inaccessible"::: ) -> ($#v2_card_1 :::"limit_cardinal"::: ) ($#v1_card_5 :::"regular"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: CARD_FIL:25 (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) "is" ($#v4_card_fil :::"inaccessible"::: ) ) ; definitionlet "IT" be ($#m1_hidden :::"Aleph":::); attr "IT" is :::"strong_limit"::: means :: CARD_FIL:def 14 (Bool "for" (Set (Var "N")) "being" ($#m1_hidden :::"Cardinal":::) "st" (Bool (Bool (Set (Var "N")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set ($#k3_card_2 :::"exp"::: ) "(" (Num 2) "," (Set (Var "N")) ")" ) ($#r2_hidden :::"in"::: ) "IT")); end; :: deftheorem defines :::"strong_limit"::: CARD_FIL:def 14 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"Aleph":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_card_fil :::"strong_limit"::: ) ) "iff" (Bool "for" (Set (Var "N")) "being" ($#m1_hidden :::"Cardinal":::) "st" (Bool (Bool (Set (Var "N")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set ($#k3_card_2 :::"exp"::: ) "(" (Num 2) "," (Set (Var "N")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) ")" )); theorem :: CARD_FIL:26 (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) "is" ($#v5_card_fil :::"strong_limit"::: ) ) ; theorem :: CARD_FIL:27 (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"Aleph":::) "st" (Bool (Bool (Set (Var "M")) "is" ($#v5_card_fil :::"strong_limit"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#v2_card_1 :::"limit_cardinal"::: ) )) ; registration cluster ($#~v1_finset_1 "non" ($#v1_finset_1 :::"finite"::: ) ) ($#v1_card_1 :::"cardinal"::: ) ($#v5_card_fil :::"strong_limit"::: ) -> ($#v2_card_1 :::"limit_cardinal"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: CARD_FIL:28 (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"Aleph":::) "st" (Bool (Bool ($#r3_card_fil :::"GCH"::: ) ) & (Bool (Set (Var "M")) "is" ($#v2_card_1 :::"limit_cardinal"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#v5_card_fil :::"strong_limit"::: ) )) ; definitionlet "IT" be ($#m1_hidden :::"Aleph":::); attr "IT" is :::"strongly_inaccessible"::: means :: CARD_FIL:def 15 (Bool "(" (Bool "IT" "is" ($#v1_card_5 :::"regular"::: ) ) & (Bool "IT" "is" ($#v5_card_fil :::"strong_limit"::: ) ) ")" ); end; :: deftheorem defines :::"strongly_inaccessible"::: CARD_FIL:def 15 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"Aleph":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_card_fil :::"strongly_inaccessible"::: ) ) "iff" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_card_5 :::"regular"::: ) ) & (Bool (Set (Var "IT")) "is" ($#v5_card_fil :::"strong_limit"::: ) ) ")" ) ")" )); registration cluster ($#~v1_finset_1 "non" ($#v1_finset_1 :::"finite"::: ) ) ($#v1_card_1 :::"cardinal"::: ) ($#v6_card_fil :::"strongly_inaccessible"::: ) -> ($#v1_card_5 :::"regular"::: ) ($#v5_card_fil :::"strong_limit"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: CARD_FIL:29 (Bool (Set ($#k4_ordinal1 :::"omega"::: ) ) "is" ($#v6_card_fil :::"strongly_inaccessible"::: ) ) ; theorem :: CARD_FIL:30 (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"Aleph":::) "st" (Bool (Bool (Set (Var "M")) "is" ($#v6_card_fil :::"strongly_inaccessible"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#v4_card_fil :::"inaccessible"::: ) )) ; registration cluster ($#~v1_finset_1 "non" ($#v1_finset_1 :::"finite"::: ) ) ($#v1_card_1 :::"cardinal"::: ) ($#v6_card_fil :::"strongly_inaccessible"::: ) -> ($#v4_card_fil :::"inaccessible"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: CARD_FIL:31 (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"Aleph":::) "st" (Bool (Bool ($#r3_card_fil :::"GCH"::: ) ) & (Bool (Set (Var "M")) "is" ($#v4_card_fil :::"inaccessible"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#v6_card_fil :::"strongly_inaccessible"::: ) )) ; definitionlet "M" be ($#m1_hidden :::"Aleph":::); attr "M" is :::"measurable"::: means :: CARD_FIL:def 16 (Bool "ex" (Set (Var "Uf")) "being" ($#m1_card_fil :::"Filter"::: ) "of" "M" "st" (Bool "(" (Bool (Set (Var "Uf")) ($#r1_card_fil :::"is_complete_with"::: ) "M") & (Bool (Bool "not" (Set (Var "Uf")) "is" ($#v2_card_fil :::"principal"::: ) )) & (Bool (Set (Var "Uf")) "is" ($#v3_card_fil :::"being_ultrafilter"::: ) ) ")" )); end; :: deftheorem defines :::"measurable"::: CARD_FIL:def 16 : (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"Aleph":::) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v7_card_fil :::"measurable"::: ) ) "iff" (Bool "ex" (Set (Var "Uf")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "Uf")) ($#r1_card_fil :::"is_complete_with"::: ) (Set (Var "M"))) & (Bool (Bool "not" (Set (Var "Uf")) "is" ($#v2_card_fil :::"principal"::: ) )) & (Bool (Set (Var "Uf")) "is" ($#v3_card_fil :::"being_ultrafilter"::: ) ) ")" )) ")" )); theorem :: CARD_FIL:32 (Bool "for" (Set (Var "A")) "being" ($#v4_ordinal1 :::"limit_ordinal"::: ) ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set ($#k3_ordinal2 :::"sup"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: CARD_FIL:33 (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"Aleph":::) "st" (Bool (Bool (Set (Var "M")) "is" ($#v7_card_fil :::"measurable"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#v1_card_5 :::"regular"::: ) )) ; registrationlet "M" be ($#m1_hidden :::"Aleph":::); cluster (Set ($#k2_card_1 :::"nextcard"::: ) "M") -> ($#~v2_card_1 "non" ($#v2_card_1 :::"limit_cardinal"::: ) ) ; end; registration cluster ($#v1_ordinal1 :::"epsilon-transitive"::: ) ($#v2_ordinal1 :::"epsilon-connected"::: ) ($#v3_ordinal1 :::"ordinal"::: ) ($#v1_finset_1 :::"infinite"::: ) ($#v1_card_1 :::"cardinal"::: ) ($#~v2_card_1 "non" ($#v2_card_1 :::"limit_cardinal"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_finset_1 "non" ($#v1_finset_1 :::"finite"::: ) ) ($#v1_card_1 :::"cardinal"::: ) ($#~v2_card_1 "non" ($#v2_card_1 :::"limit_cardinal"::: ) ) -> ($#v1_card_5 :::"regular"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "M" be ($#~v2_card_1 "non" ($#v2_card_1 :::"limit_cardinal"::: ) ) ($#m1_hidden :::"Cardinal":::); func :::"predecessor"::: "M" -> ($#m1_hidden :::"Cardinal":::) means :: CARD_FIL:def 17 (Bool "M" ($#r1_hidden :::"="::: ) (Set ($#k2_card_1 :::"nextcard"::: ) it)); end; :: deftheorem defines :::"predecessor"::: CARD_FIL:def 17 : (Bool "for" (Set (Var "M")) "being" ($#~v2_card_1 "non" ($#v2_card_1 :::"limit_cardinal"::: ) ) ($#m1_hidden :::"Cardinal":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Cardinal":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_card_fil :::"predecessor"::: ) (Set (Var "M")))) "iff" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set ($#k2_card_1 :::"nextcard"::: ) (Set (Var "b2")))) ")" ))); registrationlet "M" be ($#~v2_card_1 "non" ($#v2_card_1 :::"limit_cardinal"::: ) ) ($#m1_hidden :::"Aleph":::); cluster (Set ($#k6_card_fil :::"predecessor"::: ) "M") -> ($#v1_finset_1 :::"infinite"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "N", "N1" be ($#m1_hidden :::"Cardinal":::); mode Inf_Matrix of "N" "," "N1" "," "X" is ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "N" "," "N1" ($#k2_zfmisc_1 :::":]"::: ) ) "," "X"; end; definitionlet "M" be ($#~v2_card_1 "non" ($#v2_card_1 :::"limit_cardinal"::: ) ) ($#m1_hidden :::"Aleph":::); let "T" be ($#m1_subset_1 :::"Inf_Matrix":::) "of" (Set "(" ($#k6_card_fil :::"predecessor"::: ) (Set (Const "M")) ")" ) "," (Set (Const "M")) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Const "M")) ")" ); pred "T" :::"is_Ulam_Matrix_of"::: "M" means :: CARD_FIL:def 18 (Bool "(" (Bool "(" "for" (Set (Var "N1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_card_fil :::"predecessor"::: ) "M") (Bool "for" (Set (Var "K1")) "," (Set (Var "K2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "M" "st" (Bool (Bool (Set (Var "K1")) ($#r1_hidden :::"<>"::: ) (Set (Var "K2")))) "holds" (Bool (Set (Set "(" "T" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "N1")) "," (Set (Var "K1")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" "T" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "N1")) "," (Set (Var "K2")) ")" ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "K1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "M" (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_card_fil :::"predecessor"::: ) "M") "st" (Bool (Bool (Set (Var "N1")) ($#r1_hidden :::"<>"::: ) (Set (Var "N2")))) "holds" (Bool (Set (Set "(" "T" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "N1")) "," (Set (Var "K1")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" "T" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "N2")) "," (Set (Var "K1")) ")" ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "N1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_card_fil :::"predecessor"::: ) "M") "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" "M" ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "(" "T" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "N1")) "," (Set (Var "K1")) ")" ")" ) where K1 "is" ($#m1_subset_1 :::"Element"::: ) "of" "M" : (Bool (Set (Var "K1")) ($#r2_hidden :::"in"::: ) "M") "}" ")" ) ")" )) ($#r1_ordinal1 :::"c="::: ) (Set ($#k6_card_fil :::"predecessor"::: ) "M")) ")" ) & (Bool "(" "for" (Set (Var "K1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "M" "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" "M" ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "(" "T" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "N1")) "," (Set (Var "K1")) ")" ")" ) where N1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_card_fil :::"predecessor"::: ) "M") : (Bool (Set (Var "N1")) ($#r2_hidden :::"in"::: ) (Set ($#k6_card_fil :::"predecessor"::: ) "M")) "}" ")" ) ")" )) ($#r1_ordinal1 :::"c="::: ) (Set ($#k6_card_fil :::"predecessor"::: ) "M")) ")" ) ")" ); end; :: deftheorem defines :::"is_Ulam_Matrix_of"::: CARD_FIL:def 18 : (Bool "for" (Set (Var "M")) "being" ($#~v2_card_1 "non" ($#v2_card_1 :::"limit_cardinal"::: ) ) ($#m1_hidden :::"Aleph":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Inf_Matrix":::) "of" (Set "(" ($#k6_card_fil :::"predecessor"::: ) (Set (Var "M")) ")" ) "," (Set (Var "M")) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "M")) ")" ) "holds" (Bool "(" (Bool (Set (Var "T")) ($#r4_card_fil :::"is_Ulam_Matrix_of"::: ) (Set (Var "M"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "N1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_card_fil :::"predecessor"::: ) (Set (Var "M"))) (Bool "for" (Set (Var "K1")) "," (Set (Var "K2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "K1")) ($#r1_hidden :::"<>"::: ) (Set (Var "K2")))) "holds" (Bool (Set (Set "(" (Set (Var "T")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "N1")) "," (Set (Var "K1")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "T")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "N1")) "," (Set (Var "K2")) ")" ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "K1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_card_fil :::"predecessor"::: ) (Set (Var "M"))) "st" (Bool (Bool (Set (Var "N1")) ($#r1_hidden :::"<>"::: ) (Set (Var "N2")))) "holds" (Bool (Set (Set "(" (Set (Var "T")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "N1")) "," (Set (Var "K1")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "T")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "N2")) "," (Set (Var "K1")) ")" ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "N1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_card_fil :::"predecessor"::: ) (Set (Var "M"))) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "M")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "T")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "N1")) "," (Set (Var "K1")) ")" ")" ) where K1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "M")) : (Bool (Set (Var "K1")) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) "}" ")" ) ")" )) ($#r1_ordinal1 :::"c="::: ) (Set ($#k6_card_fil :::"predecessor"::: ) (Set (Var "M")))) ")" ) & (Bool "(" "for" (Set (Var "K1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "M")) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "M")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "T")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "N1")) "," (Set (Var "K1")) ")" ")" ) where N1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_card_fil :::"predecessor"::: ) (Set (Var "M"))) : (Bool (Set (Var "N1")) ($#r2_hidden :::"in"::: ) (Set ($#k6_card_fil :::"predecessor"::: ) (Set (Var "M")))) "}" ")" ) ")" )) ($#r1_ordinal1 :::"c="::: ) (Set ($#k6_card_fil :::"predecessor"::: ) (Set (Var "M")))) ")" ) ")" ) ")" ))); theorem :: CARD_FIL:34 (Bool "for" (Set (Var "M")) "being" ($#~v2_card_1 "non" ($#v2_card_1 :::"limit_cardinal"::: ) ) ($#m1_hidden :::"Aleph":::) (Bool "ex" (Set (Var "T")) "being" ($#m1_subset_1 :::"Inf_Matrix":::) "of" (Set "(" ($#k6_card_fil :::"predecessor"::: ) (Set (Var "M")) ")" ) "," (Set (Var "M")) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "M")) ")" ) "st" (Bool (Set (Var "T")) ($#r4_card_fil :::"is_Ulam_Matrix_of"::: ) (Set (Var "M"))))) ; theorem :: CARD_FIL:35 (Bool "for" (Set (Var "M")) "being" ($#~v2_card_1 "non" ($#v2_card_1 :::"limit_cardinal"::: ) ) ($#m1_hidden :::"Aleph":::) (Bool "for" (Set (Var "I")) "being" ($#m2_card_fil :::"Ideal"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "I")) ($#r2_card_fil :::"is_complete_with"::: ) (Set (Var "M"))) & (Bool (Set ($#k5_card_fil :::"Frechet_Ideal"::: ) (Set (Var "M"))) ($#r1_tarski :::"c="::: ) (Set (Var "I")))) "holds" (Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "M"))) & (Bool "(" "for" (Set (Var "X1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X1")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool "not" (Bool (Set (Var "X1")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) ")" ) & (Bool "(" "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X1")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "X2")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "X1")) ($#r1_hidden :::"<>"::: ) (Set (Var "X2")))) "holds" (Bool (Set (Var "X1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "X2"))) ")" ) ")" )))) ; theorem :: CARD_FIL:36 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "N")) "being" ($#m1_hidden :::"Cardinal":::) "st" (Bool (Bool (Set (Var "N")) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))))) "holds" (Bool "ex" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Var "N"))) ")" )))) ; theorem :: CARD_FIL:37 (Bool "for" (Set (Var "M")) "being" ($#~v2_card_1 "non" ($#v2_card_1 :::"limit_cardinal"::: ) ) ($#m1_hidden :::"Aleph":::) (Bool "for" (Set (Var "F")) "being" ($#m1_card_fil :::"Filter"::: ) "of" (Set (Var "M")) "holds" (Bool "(" "not" (Bool (Set (Var "F")) "is" ($#v1_card_fil :::"uniform"::: ) ) "or" "not" (Bool (Set (Var "F")) "is" ($#v3_card_fil :::"being_ultrafilter"::: ) ) "or" "not" (Bool (Set (Var "F")) ($#r1_card_fil :::"is_complete_with"::: ) (Set (Var "M"))) ")" ))) ; theorem :: CARD_FIL:38 (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"Aleph":::) "st" (Bool (Bool (Set (Var "M")) "is" ($#v7_card_fil :::"measurable"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#v2_card_1 :::"limit_cardinal"::: ) )) ; theorem :: CARD_FIL:39 (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"Aleph":::) "st" (Bool (Bool (Set (Var "M")) "is" ($#v7_card_fil :::"measurable"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#v4_card_fil :::"inaccessible"::: ) )) ; theorem :: CARD_FIL:40 (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"Aleph":::) "st" (Bool (Bool (Set (Var "M")) "is" ($#v7_card_fil :::"measurable"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#v5_card_fil :::"strong_limit"::: ) )) ; theorem :: CARD_FIL:41 (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"Aleph":::) "st" (Bool (Bool (Set (Var "M")) "is" ($#v7_card_fil :::"measurable"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#v6_card_fil :::"strongly_inaccessible"::: ) )) ;