:: CARD_4  semantic presentation begin  






























theorem :: CARD_4:1 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v4_card_3 :::"countable"::: )  )) ; 
 
theorem :: CARD_4:2 (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  ) "is"   ($#v4_card_3 :::"countable"::: )  ) ; 
 



theorem :: CARD_4:3 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "iff" (Bool (Set (Set (Var "r"))  ($#k2_newton :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 
theorem :: CARD_4:4 (Bool  "for" (Set (Var "n1")) "," (Set (Var "m1")) "," (Set (Var "n2")) "," (Set (Var "m2")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set  "(" (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "n1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "m1")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "n2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "m2")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))) "holds"  (Bool  "("  (Bool (Set (Var "n1"))  ($#r1_hidden :::"="::: )  (Set (Var "n2"))) & (Bool (Set (Var "m1"))  ($#r1_hidden :::"="::: )  (Set (Var "m2")))  ")" )) ; 
 
theorem :: CARD_4:5 (Bool  "("  (Bool (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set   ($#k5_numbers :::"NAT"::: )  )  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k5_numbers :::"NAT"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) )))  ")" ) ; 
 
theorem :: CARD_4:6 (Bool (Set (Set  ($#k4_ordinal1 :::"omega"::: ) )  ($#k2_card_2 :::"*`"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )) ; 
 
theorem :: CARD_4:7 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v4_card_3 :::"countable"::: )  ) & (Bool (Set (Var "Y")) "is"   ($#v4_card_3 :::"countable"::: )  )) "holds"  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "is"   ($#v4_card_3 :::"countable"::: )  )) ; 
 
theorem :: CARD_4:8 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Num 1)  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set (Var "D"))) "," (Set (Var "D"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Num 1)  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set (Var "D")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "D"))))  ")" )) ; 
 












theorem :: CARD_4:9 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "(" (Set (Var "n"))  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set (Var "D")) ")" ) "," (Set  "(" (Set (Var "m"))  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set (Var "D")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "m")) ")" )  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set (Var "D")))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "(" (Set (Var "n"))  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set (Var "D")) ")" ) "," (Set  "(" (Set (Var "m"))  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set (Var "D")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "m")) ")" )  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set (Var "D")) ")" )))  ")" ))) ; 
 
theorem :: CARD_4:10 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "D")) "is"   ($#v4_card_3 :::"countable"::: )  )) "holds"  (Bool (Set (Set (Var "n"))  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set (Var "D"))) "is"   ($#v4_card_3 :::"countable"::: )  ))) ; 
 
theorem :: CARD_4:11 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))) "is"   ($#v4_card_3 :::"countable"::: )  ) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))) "is"   ($#v4_card_3 :::"countable"::: )  )  ")" )) "holds"  (Bool (Set   ($#k3_card_3 :::"Union"::: )  (Set (Var "f"))) "is"   ($#v4_card_3 :::"countable"::: )  )) ; 
 
theorem :: CARD_4:12 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v4_card_3 :::"countable"::: )  ) & (Bool  "("   "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "Y")) "is"   ($#v4_card_3 :::"countable"::: )  )  ")" )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X"))) "is"   ($#v4_card_3 :::"countable"::: )  )) ; 
 
theorem :: CARD_4:13 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "D")) "is"   ($#v4_card_3 :::"countable"::: )  )) "holds"  (Bool (Set (Set (Var "D"))  ($#k3_finseq_2 :::"*"::: )  ) "is"   ($#v4_card_3 :::"countable"::: )  )) ; 
 
theorem :: CARD_4:14 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "D"))  ($#k3_finseq_2 :::"*"::: )  ")" )))) ; 
 scheme  :: CARD_4:sch 1 FraenCoun1{ F1(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "{"  (Set F1 "(" (Set (Var "n")) ")" ) where n "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool P1[(Set (Var "n"))])  "}"   "is"   ($#v4_card_3 :::"countable"::: )  )
 proof 


end; scheme  :: CARD_4:sch 2 FraenCoun2{ F1(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "{"  (Set F1 "(" (Set (Var "n1")) "," (Set (Var "n2")) ")" ) where n1, n2 "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool P1[(Set (Var "n1")) "," (Set (Var "n2"))])  "}"   "is"   ($#v4_card_3 :::"countable"::: )  )
 proof 


end; scheme  :: CARD_4:sch 3 FraenCoun3{ F1(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "{"  (Set F1 "(" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ) where n1, n2, n3 "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool P1[(Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3"))])  "}"   "is"   ($#v4_card_3 :::"countable"::: )  )
 proof 


end; 









theorem :: CARD_4:15 (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Bool  "not" (Set (Var "M")) "is"   ($#v1_finset_1 :::"finite"::: )  ))) "holds"  (Bool (Set (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "M")))) ; 
 
theorem :: CARD_4:16 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Bool  "not" (Set (Var "M")) "is"   ($#v1_finset_1 :::"finite"::: )  )) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool  "("  (Bool (Set (Var "N"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "M"))) "or" (Bool (Set (Var "N"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N")))  ($#r1_hidden :::"="::: )  (Set (Var "M"))) & (Bool (Set (Set (Var "N"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "M")))  ")" )) ; 
 
theorem :: CARD_4:17 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Bool  "not" (Set (Var "M")) "is"   ($#v1_finset_1 :::"finite"::: )  )) & (Bool  "("  (Bool (Set (Var "N"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "M"))) "or" (Bool (Set (Var "N"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "M"))) & (Bool (Set (Set (Var "N"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "M")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "M")))  ")" )) ; 
 
theorem :: CARD_4:18 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  ))) "holds"  (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))  ")" )) ; 
 
theorem :: CARD_4:19 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  )) & (Bool (Set (Var "Y")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))  ")" )) ; 
 
theorem :: CARD_4:20 (Bool  "for" (Set (Var "K")) "," (Set (Var "L")) "," (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Var "K"))  ($#r2_hidden :::"in"::: )  (Set (Var "L"))) & (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "M")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "L"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N")))) & (Bool (Set (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "K")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "L"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N"))))  ")" )) ; 
 
theorem :: CARD_4:21 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  ))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k4_ordinal1 :::"omega"::: ) )  ($#k2_card_2 :::"*`"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: CARD_4:22 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Bool  "not" (Set (Var "Y")) "is"   ($#v1_finset_1 :::"finite"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "Y")) ")" )  ($#k2_card_2 :::"*`"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y"))))) ; 
 
theorem :: CARD_4:23 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Bool  "not" (Set (Var "D")) "is"   ($#v1_finset_1 :::"finite"::: )  )) & (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "n"))  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set (Var "D"))) "," (Set (Var "D"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "n"))  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set (Var "D")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "D"))))  ")" ))) ; 
 
theorem :: CARD_4:24 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "D")) "is"   ($#v1_finset_1 :::"finite"::: )  ))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "D"))  ($#k3_finseq_2 :::"*"::: )  ")" )))) ;