:: ORDINAL3 semantic presentation begin theorem :: ORDINAL3:1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "X"))))) ; theorem :: ORDINAL3:2 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) ; theorem :: ORDINAL3:3 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) "iff" (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "B")))) ")" )) ; theorem :: ORDINAL3:4 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "X"))) "is" ($#m1_hidden :::"Ordinal":::)))) ; theorem :: ORDINAL3:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_ordinal1 :::"On"::: ) (Set (Var "X")) ")" )) "is" ($#m1_hidden :::"Ordinal":::))) ; theorem :: ORDINAL3:6 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k2_ordinal1 :::"On"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: ORDINAL3:7 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k2_ordinal1 :::"On"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: ORDINAL3:8 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) ; theorem :: ORDINAL3:9 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k2_ordinal2 :::"inf"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: ORDINAL3:10 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k2_ordinal2 :::"inf"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "A")))) ; theorem :: ORDINAL3:11 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set (Var "X"))) "is" ($#m1_hidden :::"Ordinal":::)))) ; registrationlet "A", "B" be ($#m1_hidden :::"Ordinal":::); cluster (Set "A" ($#k2_xboole_0 :::"\/"::: ) "B") -> ($#v3_ordinal1 :::"ordinal"::: ) ; cluster (Set "A" ($#k3_xboole_0 :::"/\"::: ) "B") -> ($#v3_ordinal1 :::"ordinal"::: ) ; end; theorem :: ORDINAL3:12 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) "or" (Bool (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" )) ; theorem :: ORDINAL3:13 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) "or" (Bool (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) ")" )) ; theorem :: ORDINAL3:14 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Num 1))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: ORDINAL3:15 (Bool (Num 1) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ; theorem :: ORDINAL3:16 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" "not" (Bool (Set (Var "A")) ($#r1_ordinal1 :::"c="::: ) (Num 1)) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) ; theorem :: ORDINAL3:17 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool "(" (Bool (Set (Var "A")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "B"))) "or" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" ) & (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "A")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "D"))))) ; theorem :: ORDINAL3:18 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "C")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "A")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "C"))) ($#r1_ordinal1 :::"c="::: ) (Set (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "D"))))) ; theorem :: ORDINAL3:19 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool "(" (Bool "(" (Bool (Set (Var "C")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "D"))) & (Bool (Set (Var "D")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "or" (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "D"))))) ; theorem :: ORDINAL3:20 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "C")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "A")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C"))) ($#r1_ordinal1 :::"c="::: ) (Set (Set (Var "B")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "D"))))) ; theorem :: ORDINAL3:21 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Var "D")))) ; theorem :: ORDINAL3:22 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) ; theorem :: ORDINAL3:23 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "C"))) ($#r1_ordinal1 :::"c="::: ) (Set (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Var "C")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "D")))) ; theorem :: ORDINAL3:24 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_ordinal1 :::"c="::: ) (Set (Set (Var "A")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "B")))) & (Bool (Set (Var "B")) ($#r1_ordinal1 :::"c="::: ) (Set (Set (Var "A")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "B")))) ")" )) ; theorem :: ORDINAL3:25 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "C")))) & (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "B")))) ")" )) ; theorem :: ORDINAL3:26 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Set (Var "A")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: ORDINAL3:27 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "C")))))) ; theorem :: ORDINAL3:28 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "ex" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "C")))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: ORDINAL3:29 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "A"))) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) ; theorem :: ORDINAL3:30 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "B")) ")" ) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k10_ordinal2 :::"+^"::: ) (Set "(" (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "C")) ")" )))) ; theorem :: ORDINAL3:31 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" "not" (Bool (Set (Set (Var "A")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: ORDINAL3:32 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C")))) & (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "B")))) ")" )) ; theorem :: ORDINAL3:33 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Set (Var "B")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "A")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "C")))) ; theorem :: ORDINAL3:34 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Set (Var "B")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) ; theorem :: ORDINAL3:35 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Set (Var "B")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "A"))) ($#r1_ordinal1 :::"c="::: ) (Set (Set (Var "C")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "A")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "B")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "C")))) ; theorem :: ORDINAL3:36 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_ordinal1 :::"c="::: ) (Set (Set (Var "A")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "B")))) & (Bool (Set (Var "A")) ($#r1_ordinal1 :::"c="::: ) (Set (Set (Var "B")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "A")))) ")" )) ; theorem :: ORDINAL3:37 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Set (Var "A")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) ; theorem :: ORDINAL3:38 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" "not" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "C")))) "or" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) "or" (Bool "ex" (Set (Var "D")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "D")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "D")))) ")" )) ")" )) ; definitionlet "C" be ($#m1_hidden :::"Ordinal":::); let "fi" be ($#m1_hidden :::"Ordinal-Sequence":::); func "C" :::"+^"::: "fi" -> ($#m1_hidden :::"Ordinal-Sequence":::) means :: ORDINAL3:def 1 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "fi")) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "fi"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set "C" ($#k10_ordinal2 :::"+^"::: ) (Set "(" "fi" ($#k1_funct_1 :::"."::: ) (Set (Var "A")) ")" ))) ")" ) ")" ); func "fi" :::"+^"::: "C" -> ($#m1_hidden :::"Ordinal-Sequence":::) means :: ORDINAL3:def 2 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "fi")) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "fi"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "fi" ($#k1_funct_1 :::"."::: ) (Set (Var "A")) ")" ) ($#k10_ordinal2 :::"+^"::: ) "C")) ")" ) ")" ); func "C" :::"*^"::: "fi" -> ($#m1_hidden :::"Ordinal-Sequence":::) means :: ORDINAL3:def 3 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "fi")) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "fi"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set "C" ($#k11_ordinal2 :::"*^"::: ) (Set "(" "fi" ($#k1_funct_1 :::"."::: ) (Set (Var "A")) ")" ))) ")" ) ")" ); func "fi" :::"*^"::: "C" -> ($#m1_hidden :::"Ordinal-Sequence":::) means :: ORDINAL3:def 4 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "fi")) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "fi"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "fi" ($#k1_funct_1 :::"."::: ) (Set (Var "A")) ")" ) ($#k11_ordinal2 :::"*^"::: ) "C")) ")" ) ")" ); end; :: deftheorem defines :::"+^"::: ORDINAL3:def 1 : (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "fi")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k1_ordinal3 :::"+^"::: ) (Set (Var "fi")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "fi")))) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "fi"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k10_ordinal2 :::"+^"::: ) (Set "(" (Set (Var "fi")) ($#k1_funct_1 :::"."::: ) (Set (Var "A")) ")" ))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"+^"::: ORDINAL3:def 2 : (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "fi")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "fi")) ($#k2_ordinal3 :::"+^"::: ) (Set (Var "C")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "fi")))) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "fi"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "fi")) ($#k1_funct_1 :::"."::: ) (Set (Var "A")) ")" ) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "C")))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"*^"::: ORDINAL3:def 3 : (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "fi")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k3_ordinal3 :::"*^"::: ) (Set (Var "fi")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "fi")))) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "fi"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k11_ordinal2 :::"*^"::: ) (Set "(" (Set (Var "fi")) ($#k1_funct_1 :::"."::: ) (Set (Var "A")) ")" ))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"*^"::: ORDINAL3:def 4 : (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "fi")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "fi")) ($#k4_ordinal3 :::"*^"::: ) (Set (Var "C")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "fi")))) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "fi"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "fi")) ($#k1_funct_1 :::"."::: ) (Set (Var "A")) ")" ) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C")))) ")" ) ")" ) ")" ))); theorem :: ORDINAL3:39 (Bool "for" (Set (Var "fi")) "," (Set (Var "psi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "fi")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "fi"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "psi")))) & (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "fi")))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "fi")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "psi")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "B")))) ")" )) "holds" (Bool (Set ($#k4_ordinal2 :::"sup"::: ) (Set (Var "psi"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k10_ordinal2 :::"+^"::: ) (Set "(" ($#k4_ordinal2 :::"sup"::: ) (Set (Var "fi")) ")" ))))) ; theorem :: ORDINAL3:40 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "B"))) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) ; theorem :: ORDINAL3:41 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C")))) & (Bool (Set (Var "B")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool "ex" (Set (Var "D")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "D")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "D")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C")))) ")" ))) ; theorem :: ORDINAL3:42 (Bool "for" (Set (Var "fi")) "," (Set (Var "psi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "fi"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "psi")))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_ordinal2 :::"sup"::: ) (Set (Var "fi"))) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) ) & (Bool "(" "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "fi")))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "fi")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "psi")) ($#k1_funct_1 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C")))) ")" )) "holds" (Bool (Set ($#k4_ordinal2 :::"sup"::: ) (Set (Var "psi"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_ordinal2 :::"sup"::: ) (Set (Var "fi")) ")" ) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C")))))) ; theorem :: ORDINAL3:43 (Bool "for" (Set (Var "fi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "fi"))))) "holds" (Bool (Set ($#k4_ordinal2 :::"sup"::: ) (Set "(" (Set (Var "C")) ($#k1_ordinal3 :::"+^"::: ) (Set (Var "fi")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k10_ordinal2 :::"+^"::: ) (Set "(" ($#k4_ordinal2 :::"sup"::: ) (Set (Var "fi")) ")" ))))) ; theorem :: ORDINAL3:44 (Bool "for" (Set (Var "fi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "fi")))) & (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_ordinal2 :::"sup"::: ) (Set (Var "fi"))) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool (Set ($#k4_ordinal2 :::"sup"::: ) (Set "(" (Set (Var "fi")) ($#k4_ordinal3 :::"*^"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_ordinal2 :::"sup"::: ) (Set (Var "fi")) ")" ) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C")))))) ; theorem :: ORDINAL3:45 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "A")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k10_ordinal2 :::"+^"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set (Var "B")) ")" )))) ; theorem :: ORDINAL3:46 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "B")) ")" ) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C")) ")" ) ($#k10_ordinal2 :::"+^"::: ) (Set "(" (Set (Var "B")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C")) ")" )))) ; theorem :: ORDINAL3:47 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "C")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "A")) ")" ) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "D")))) & (Bool (Set (Var "D")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))) ; theorem :: ORDINAL3:48 (Bool "for" (Set (Var "A")) "," (Set (Var "C1")) "," (Set (Var "D1")) "," (Set (Var "C2")) "," (Set (Var "D2")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "C1")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "A")) ")" ) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "D1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "C2")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "A")) ")" ) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "D2")))) & (Bool (Set (Var "D1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "D2")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Var "C2"))) & (Bool (Set (Var "D1")) ($#r1_hidden :::"="::: ) (Set (Var "D2"))) ")" )) ; theorem :: ORDINAL3:49 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) "is" ($#v4_ordinal1 :::"limit_ordinal"::: ) )) "holds" (Bool "for" (Set (Var "fi")) "being" ($#m1_hidden :::"Ordinal-Sequence":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "fi"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "fi")) ($#k1_funct_1 :::"."::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "B")))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_ordinal2 :::"sup"::: ) (Set (Var "fi")))))) ; theorem :: ORDINAL3:50 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "B")) ")" ) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k11_ordinal2 :::"*^"::: ) (Set "(" (Set (Var "B")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C")) ")" )))) ; definitionlet "A", "B" be ($#m1_hidden :::"Ordinal":::); func "A" :::"-^"::: "B" -> ($#m1_hidden :::"Ordinal":::) means :: ORDINAL3:def 5 (Bool "A" ($#r1_hidden :::"="::: ) (Set "B" ($#k10_ordinal2 :::"+^"::: ) it)) if (Bool "B" ($#r1_ordinal1 :::"c="::: ) "A") otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); func "A" :::"div^"::: "B" -> ($#m1_hidden :::"Ordinal":::) means :: ORDINAL3:def 6 (Bool "ex" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool "A" ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k11_ordinal2 :::"*^"::: ) "B" ")" ) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "C")))) & (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) "B") ")" )) if (Bool "B" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"-^"::: ORDINAL3:def 5 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "B")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "A")))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "B")))) "iff" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "b3")))) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "B")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "A"))))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "B")))) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ")" )); :: deftheorem defines :::"div^"::: ORDINAL3:def 6 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_ordinal3 :::"div^"::: ) (Set (Var "B")))) "iff" (Bool "ex" (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "B")) ")" ) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "C")))) & (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_ordinal3 :::"div^"::: ) (Set (Var "B")))) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ")" )); definitionlet "A", "B" be ($#m1_hidden :::"Ordinal":::); func "A" :::"mod^"::: "B" -> ($#m1_hidden :::"Ordinal":::) equals :: ORDINAL3:def 7 (Set "A" ($#k5_ordinal3 :::"-^"::: ) (Set "(" (Set "(" "A" ($#k6_ordinal3 :::"div^"::: ) "B" ")" ) ($#k11_ordinal2 :::"*^"::: ) "B" ")" )); end; :: deftheorem defines :::"mod^"::: ORDINAL3:def 7 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Set (Var "A")) ($#k7_ordinal3 :::"mod^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_ordinal3 :::"-^"::: ) (Set "(" (Set "(" (Set (Var "A")) ($#k6_ordinal3 :::"div^"::: ) (Set (Var "B")) ")" ) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "B")) ")" )))); theorem :: ORDINAL3:51 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k10_ordinal2 :::"+^"::: ) (Set "(" (Set (Var "B")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "A")) ")" )))) ; theorem :: ORDINAL3:52 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "B")) ")" ) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "B")))) ; theorem :: ORDINAL3:53 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool "(" (Bool (Set (Var "C")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "A"))) "or" (Bool (Set (Var "C")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "C"))))) ; theorem :: ORDINAL3:54 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Set (Var "A")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: ORDINAL3:55 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Set (Var "B")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "A")))) ")" )) ; theorem :: ORDINAL3:56 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k5_ordinal3 :::"-^"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: ORDINAL3:57 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Set (Var "A")) ($#k5_ordinal3 :::"-^"::: ) (Set "(" (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "B")) ")" ) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "C"))))) ; theorem :: ORDINAL3:58 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "C")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "B"))) ($#r1_ordinal1 :::"c="::: ) (Set (Set (Var "C")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "A"))))) ; theorem :: ORDINAL3:59 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_ordinal1 :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "A")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "C"))) ($#r1_ordinal1 :::"c="::: ) (Set (Set (Var "B")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "C"))))) ; theorem :: ORDINAL3:60 (Bool "for" (Set (Var "C")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "C")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Set (Var "A")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) ; theorem :: ORDINAL3:61 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Set (Var "A")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "B"))) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "A"))))) ; theorem :: ORDINAL3:62 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Var "A")) ($#r1_ordinal1 :::"c="::: ) (Set (Set (Var "B")) ($#k10_ordinal2 :::"+^"::: ) (Set "(" (Set (Var "A")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "B")) ")" )))) ; theorem :: ORDINAL3:63 (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C")) ")" ) ($#k5_ordinal3 :::"-^"::: ) (Set "(" (Set (Var "B")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "B")) ")" ) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C"))))) ; theorem :: ORDINAL3:64 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k6_ordinal3 :::"div^"::: ) (Set (Var "B")) ")" ) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "B"))) ($#r1_ordinal1 :::"c="::: ) (Set (Var "A")))) ; theorem :: ORDINAL3:65 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "A")) ($#k6_ordinal3 :::"div^"::: ) (Set (Var "B")) ")" ) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "B")) ")" ) ($#k10_ordinal2 :::"+^"::: ) (Set "(" (Set (Var "A")) ($#k7_ordinal3 :::"mod^"::: ) (Set (Var "B")) ")" )))) ; theorem :: ORDINAL3:66 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C")) ")" ) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "D")))) & (Bool (Set (Var "D")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_ordinal3 :::"div^"::: ) (Set (Var "C")))) & (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_ordinal3 :::"mod^"::: ) (Set (Var "C")))) ")" )) ; theorem :: ORDINAL3:67 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "C"))))) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k6_ordinal3 :::"div^"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "A")) ($#k7_ordinal3 :::"mod^"::: ) (Set (Var "C"))) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) ")" )) ; theorem :: ORDINAL3:68 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "B")) ")" ) ($#k6_ordinal3 :::"div^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) ; theorem :: ORDINAL3:69 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "B")) ")" ) ($#k7_ordinal3 :::"mod^"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: ORDINAL3:70 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k6_ordinal3 :::"div^"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k7_ordinal3 :::"mod^"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "A")) ($#k7_ordinal3 :::"mod^"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" )) ; theorem :: ORDINAL3:71 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k6_ordinal3 :::"div^"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "A")) ($#k7_ordinal3 :::"mod^"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; begin theorem :: ORDINAL3:72 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_ordinal2 :::"sup"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_ordinal1 :::"On"::: ) (Set (Var "X")) ")" ) ")" )))) ; theorem :: ORDINAL3:73 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "A"))) ($#r2_ordinal2 :::"is_cofinal_with"::: ) (Num 1))) ; theorem :: ORDINAL3:74 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Set (Var "a")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "b"))) "is" ($#v7_ordinal1 :::"natural"::: ) )) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) ")" )) ; registrationlet "a", "b" be ($#v7_ordinal1 :::"natural"::: ) ($#m1_hidden :::"Ordinal":::); cluster (Set "a" ($#k5_ordinal3 :::"-^"::: ) "b") -> ($#v7_ordinal1 :::"natural"::: ) ; cluster (Set "a" ($#k11_ordinal2 :::"*^"::: ) "b") -> ($#v7_ordinal1 :::"natural"::: ) ; end; theorem :: ORDINAL3:75 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Set (Var "a")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "b"))) "is" ($#v7_ordinal1 :::"natural"::: ) ) & (Bool (Bool "not" (Set (Set (Var "a")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "b"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k4_ordinal1 :::"omega"::: ) )) ")" )) ; definitionlet "a", "b" be ($#v7_ordinal1 :::"natural"::: ) ($#m1_hidden :::"Ordinal":::); :: original: :::"+^"::: redefine func "a" :::"+^"::: "b" -> ($#m1_hidden :::"set"::: ) ; commutativity (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v7_ordinal1 :::"natural"::: ) ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Set (Var "a")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "a"))))) ; end; definitionlet "a", "b" be ($#v7_ordinal1 :::"natural"::: ) ($#m1_hidden :::"Ordinal":::); :: original: :::"*^"::: redefine func "a" :::"*^"::: "b" -> ($#m1_hidden :::"set"::: ) ; commutativity (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v7_ordinal1 :::"natural"::: ) ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set (Set (Var "a")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k11_ordinal2 :::"*^"::: ) (Set (Var "a"))))) ; end;