:: FINSET_1 semantic presentation begin definitionlet "IT" be ($#m1_hidden :::"set"::: ) ; attr "IT" is :::"finite"::: means :: FINSET_1:def 1 (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) "IT") & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) ")" )); end; :: deftheorem defines :::"finite"::: FINSET_1:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_finset_1 :::"finite"::: ) ) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "IT"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) ")" )) ")" )); notationlet "IT" be ($#m1_hidden :::"set"::: ) ; antonym :::"infinite"::: "IT" for :::"finite"::: ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; scheme :: FINSET_1:sch 1 OLambdaC{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F3( ($#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 "x")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "x")) ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )) ")" ")" ) ")" ) ")" )) proof end; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_tarski :::"{"::: ) "x" "," "y" ($#k2_tarski :::"}"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "x", "y", "z" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_enumset1 :::"{"::: ) "x" "," "y" "," "z" ($#k1_enumset1 :::"}"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "x1", "x2", "x3", "x4" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_enumset1 :::"{"::: ) "x1" "," "x2" "," "x3" "," "x4" ($#k2_enumset1 :::"}"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "x1", "x2", "x3", "x4", "x5" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_enumset1 :::"{"::: ) "x1" "," "x2" "," "x3" "," "x4" "," "x5" ($#k3_enumset1 :::"}"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "x1", "x2", "x3", "x4", "x5", "x6" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_enumset1 :::"{"::: ) "x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6" ($#k4_enumset1 :::"}"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "x1", "x2", "x3", "x4", "x5", "x6", "x7" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_enumset1 :::"{"::: ) "x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6" "," "x7" ($#k5_enumset1 :::"}"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "x1", "x2", "x3", "x4", "x5", "x6", "x7", "x8" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k6_enumset1 :::"{"::: ) "x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6" "," "x7" "," "x8" ($#k6_enumset1 :::"}"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "B" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "B"); end; registrationlet "X", "Y" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k2_xboole_0 :::"\/"::: ) "Y") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: FINSET_1:1 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) )) ; theorem :: FINSET_1:2 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B"))) "is" ($#v1_finset_1 :::"finite"::: ) )) ; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k3_xboole_0 :::"/\"::: ) "B") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "A" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k3_xboole_0 :::"/\"::: ) "B") -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set "A" ($#k4_xboole_0 :::"\"::: ) "B") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: FINSET_1:3 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B"))) "is" ($#v1_finset_1 :::"finite"::: ) )) ; theorem :: FINSET_1:4 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set (Var "B"))) "is" ($#v1_finset_1 :::"finite"::: ) )) ; registrationlet "f" be ($#m1_hidden :::"Function":::); let "A" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k7_relat_1 :::".:"::: ) "A") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: FINSET_1:5 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "A"))) "is" ($#v1_finset_1 :::"finite"::: ) ))) ; theorem :: FINSET_1:6 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" )))) ; scheme :: FINSET_1:sch 2 Finite{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool P1[(Set F1 "(" ")" )]) provided (Bool (Set F1 "(" ")" ) "is" ($#v1_finset_1 :::"finite"::: ) ) and (Bool P1[(Set ($#k1_xboole_0 :::"{}"::: ) )]) and (Bool "for" (Set (Var "x")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "B"))])) "holds" (Bool P1[(Set (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))])) proof end; registrationlet "A", "B" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "A", "B", "C" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_zfmisc_1 :::"[:"::: ) "A" "," "B" "," "C" ($#k3_zfmisc_1 :::":]"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "A", "B", "C", "D" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_zfmisc_1 :::"[:"::: ) "A" "," "B" "," "C" "," "D" ($#k4_zfmisc_1 :::":]"::: ) ) -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "A" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_zfmisc_1 :::"bool"::: ) "A") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: FINSET_1:7 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "X")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ) ")" ) "iff" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" )) ; theorem :: FINSET_1:8 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) "is" ($#v1_finset_1 :::"finite"::: ) )) ; theorem :: FINSET_1:9 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set (Var "Y"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Var "Y")) "is" ($#v1_finset_1 :::"finite"::: ) ))) ; registrationlet "X", "Y" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k5_xboole_0 :::"\+\"::: ) "Y") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); end; begin theorem :: FINSET_1:10 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "is" ($#v1_finset_1 :::"finite"::: ) ) "iff" (Bool (Set (Var "f")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" )) ; theorem :: FINSET_1:11 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "F")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) )) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "m")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) ")" ) ")" ))) ; theorem :: FINSET_1:12 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "F")) "is" ($#v6_ordinal1 :::"c=-linear"::: ) )) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "m"))) ")" ) ")" ))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"finite-yielding"::: means :: FINSET_1:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))) "holds" (Bool (Set (Var "x")) "is" ($#v1_finset_1 :::"finite"::: ) )); end; :: deftheorem defines :::"finite-yielding"::: FINSET_1:def 2 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_finset_1 :::"finite-yielding"::: ) ) "iff" (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 "R"))))) "holds" (Bool (Set (Var "x")) "is" ($#v1_finset_1 :::"finite"::: ) )) ")" )); theorem :: FINSET_1:13 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "ex" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "B")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "Z"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ))) ; theorem :: FINSET_1:14 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ))) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "R" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k9_xtuple_0 :::"proj1"::: ) "R") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "f" be ($#m1_hidden :::"Function":::); let "g" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); cluster (Set "g" ($#k3_relat_1 :::"*"::: ) "f") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "A" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2("A" "," "B") -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "x" ($#k16_funcop_1 :::".-->"::: ) "y") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "R" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k10_xtuple_0 :::"proj2"::: ) "R") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "f" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k8_relat_1 :::"""::: ) "x") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "f", "g" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k1_funct_4 :::"+*"::: ) "g") -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "F" be ($#m1_hidden :::"set"::: ) ; attr "F" is :::"centered"::: means :: FINSET_1:def 3 (Bool "(" (Bool "F" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "G")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) "F") & (Bool (Set (Var "G")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "G"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"centered"::: FINSET_1:def 3 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v3_finset_1 :::"centered"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "G")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "F"))) & (Bool (Set (Var "G")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "G"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ) ")" )); definitionlet "f" be ($#m1_hidden :::"Function":::); redefine attr "f" is :::"finite-yielding"::: means :: FINSET_1:def 4 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#v1_finset_1 :::"finite"::: ) )); end; :: deftheorem defines :::"finite-yielding"::: FINSET_1:def 4 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_finset_1 :::"finite-yielding"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#v1_finset_1 :::"finite"::: ) )) ")" )); definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "IT" be (Set (Const "I")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); :: original: :::"finite-yielding"::: redefine attr "IT" is :::"finite-yielding"::: means :: FINSET_1:def 5 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#v1_finset_1 :::"finite"::: ) )); end; :: deftheorem defines :::"finite-yielding"::: FINSET_1:def 5 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_finset_1 :::"finite-yielding"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#v1_finset_1 :::"finite"::: ) )) ")" ))); theorem :: FINSET_1:15 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) "is" ($#v1_finset_1 :::"infinite"::: ) )) "holds" (Bool "not" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) )))) ; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "I")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) "f" ($#v5_funct_1 :::"-compatible"::: ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "A" ($#k6_relat_1 :::"|`"::: ) "F") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "F" ($#k5_relat_1 :::"|"::: ) "A") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "A" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_hidden :::"Function":::); cluster (Set "F" ($#k5_relat_1 :::"|"::: ) "A") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "R" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k1_relat_1 :::"field"::: ) "R") -> ($#v1_finset_1 :::"finite"::: ) ; end; registration cluster ($#v1_zfmisc_1 :::"trivial"::: ) -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_finset_1 :::"infinite"::: ) -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); end; registrationlet "x", "y", "a", "b" be ($#m1_hidden :::"set"::: ) ; cluster (Set "(" "x" "," "y" ")" ($#k4_funct_4 :::"-->"::: ) "(" "a" "," "b" ")" ) -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; attr "A" is :::"finite-membered"::: means :: FINSET_1:def 6 (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool (Set (Var "B")) "is" ($#v1_finset_1 :::"finite"::: ) )); end; :: deftheorem defines :::"finite-membered"::: FINSET_1:def 6 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v5_finset_1 :::"finite-membered"::: ) ) "iff" (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "B")) "is" ($#v1_finset_1 :::"finite"::: ) )) ")" )); registration cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v5_finset_1 :::"finite-membered"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "A" be ($#v5_finset_1 :::"finite-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "A"; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v5_finset_1 :::"finite-membered"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_tarski :::"{"::: ) "X" ($#k1_tarski :::"}"::: ) ) -> ($#v5_finset_1 :::"finite-membered"::: ) ; cluster (Set ($#k1_zfmisc_1 :::"bool"::: ) "X") -> ($#v5_finset_1 :::"finite-membered"::: ) ; let "Y" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_tarski :::"{"::: ) "X" "," "Y" ($#k2_tarski :::"}"::: ) ) -> ($#v5_finset_1 :::"finite-membered"::: ) ; end; registrationlet "X" be ($#v5_finset_1 :::"finite-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v5_finset_1 :::"finite-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); let "Y" be ($#v5_finset_1 :::"finite-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k2_xboole_0 :::"\/"::: ) "Y") -> ($#v5_finset_1 :::"finite-membered"::: ) ; end; registrationlet "X" be ($#v1_finset_1 :::"finite"::: ) ($#v5_finset_1 :::"finite-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_tarski :::"union"::: ) "X") -> ($#v1_finset_1 :::"finite"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_finset_1 :::"finite-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_relat_1 :::"Relation-like"::: ) -> ($#v2_finset_1 :::"finite-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "F" be ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "F" be ($#v2_finset_1 :::"finite-yielding"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k10_xtuple_0 :::"proj2"::: ) "F") -> ($#v5_finset_1 :::"finite-membered"::: ) ; end;