:: WELLORD2  semantic presentation begin  






















definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"RelIncl"::: "X" ->   ($#m1_hidden :::"Relation":::) means :: WELLORD2:def 1 (Bool  "("  (Bool (Set   ($#k1_relat_1 :::"field"::: )  it)  ($#r1_hidden :::"="::: )  "X") & (Bool  "("   "for" (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "Z"))  ($#r2_hidden :::"in"::: )  "X")) "holds"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))  ")" )  ")" )  ")" ); end; 





:: deftheorem    defines :::"RelIncl"::: WELLORD2:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "Z"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))  ")" )  ")" )  ")" )  ")" ))); 
 
theorem :: WELLORD2:1 canceled; 
 
theorem :: WELLORD2:2 canceled; 
 
theorem :: WELLORD2:3 canceled; 
 
theorem :: WELLORD2:4 canceled; 
 
theorem :: WELLORD2:5 canceled; 
 
theorem :: WELLORD2:6 canceled; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_wellord2 :::"RelIncl"::: )  "X") ->   ($#v1_relat_2 :::"reflexive"::: )   ; 

cluster (Set   ($#k1_wellord2 :::"RelIncl"::: )  "X") ->   ($#v8_relat_2 :::"transitive"::: )   ; 

cluster (Set   ($#k1_wellord2 :::"RelIncl"::: )  "X") ->   ($#v4_relat_2 :::"antisymmetric"::: )   ; 
end; registrationlet "A" be   ($#m1_hidden :::"Ordinal":::); 
cluster (Set   ($#k1_wellord2 :::"RelIncl"::: )  "A") ->   ($#v6_relat_2 :::"connected"::: )   ; 

cluster (Set   ($#k1_wellord2 :::"RelIncl"::: )  "A") ->   ($#v1_wellord1 :::"well_founded"::: )   ; 
end; 
theorem :: WELLORD2:7 (Bool  "for" (Set (Var "Y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X")) ")" )  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "Y"))))) ; 
 
theorem :: WELLORD2:8 (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_wellord2 :::"RelIncl"::: )  (Set (Var "X"))) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ))) ; 
 



theorem :: WELLORD2:9 (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 "A"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "B")) ")" )  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "A"))))) ; 
 
theorem :: WELLORD2:10 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "A"))) "," (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "B")))  ($#r4_wellord1 :::"are_isomorphic"::: )  )) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) ; 
 
theorem :: WELLORD2:11 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "R")) "," (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "A")))  ($#r4_wellord1 :::"are_isomorphic"::: )  ) & (Bool (Set (Var "R")) "," (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "B")))  ($#r4_wellord1 :::"are_isomorphic"::: )  )) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B"))))) ; 
 
theorem :: WELLORD2:12 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))) "holds"  (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set  "(" (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "a")) ")" )) "," (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "A")))  ($#r4_wellord1 :::"are_isomorphic"::: )  ))  ")" )) "holds"  (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "R")) "," (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "A")))  ($#r4_wellord1 :::"are_isomorphic"::: )  ))) ; 
 
theorem :: WELLORD2:13 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )) "holds"  (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "R")) "," (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "A")))  ($#r4_wellord1 :::"are_isomorphic"::: )  ))) ; 
 definitionlet "R" be   ($#m1_hidden :::"Relation":::); assume 
(Bool (Set (Const "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )
 ; func  :::"order_type_of"::: "R" ->   ($#m1_hidden :::"Ordinal":::) means :: WELLORD2:def 2 (Bool "R" "," (Set   ($#k1_wellord2 :::"RelIncl"::: )  it)  ($#r4_wellord1 :::"are_isomorphic"::: )  ); end; 






:: deftheorem    defines :::"order_type_of"::: WELLORD2:def 2 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )) "holds"  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_wellord2 :::"order_type_of"::: )  (Set (Var "R")))) "iff" (Bool (Set (Var "R")) "," (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "b2")))  ($#r4_wellord1 :::"are_isomorphic"::: )  )  ")" ))); 
 definitionlet "A" be   ($#m1_hidden :::"Ordinal":::); let "R" be   ($#m1_hidden :::"Relation":::); pred "A" :::"is_order_type_of"::: "R" means :: WELLORD2:def 3 (Bool "A"  ($#r1_hidden :::"="::: )  (Set   ($#k2_wellord2 :::"order_type_of"::: )  "R")); end; 





:: deftheorem    defines :::"is_order_type_of"::: WELLORD2:def 3 :  (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r1_wellord2 :::"is_order_type_of"::: )  (Set (Var "R"))) "iff" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_wellord2 :::"order_type_of"::: )  (Set (Var "R"))))  ")" ))); 
 
theorem :: WELLORD2:14 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) "holds"  (Bool (Set   ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "A"))))) ; 
 



definitionlet "X", "Y" be    ($#m1_hidden :::"set"::: )  ; :: original: :::"are_equipotent"::: redefine pred "X" "," "Y" :::"are_equipotent":::  means :: WELLORD2:def 4 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  "X") & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  "Y")  ")" )); reflexivity  
(Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "X")))  ")" )))
 ; symmetry  
(Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "Y")))  ")" ))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "Y"))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "X")))  ")" )))
 ; end; 





:: deftheorem    defines :::"are_equipotent"::: WELLORD2:def 4 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "," (Set (Var "Y"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "Y")))  ")" ))  ")" )); 
 
theorem :: WELLORD2:15 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "," (Set (Var "Y"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set (Var "Y")) "," (Set (Var "Z"))  ($#r2_wellord2 :::"are_equipotent"::: )  )) "holds"  (Bool (Set (Var "X")) "," (Set (Var "Z"))  ($#r2_wellord2 :::"are_equipotent"::: )  )) ; 
 
theorem :: WELLORD2:16 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R"))  ($#r2_wellord1 :::"well_orders"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set   ($#k1_relat_1 :::"field"::: )  (Set  "(" (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set (Set (Var "R"))  ($#k2_wellord1 :::"|_2"::: )  (Set (Var "X"))) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )  ")" ))) ; 
 
theorem :: WELLORD2:17 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "st" (Bool (Set (Var "R"))  ($#r2_wellord1 :::"well_orders"::: )  (Set (Var "X"))))) ; 
 



theorem :: WELLORD2:18 (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" ) & (Bool  "("   "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))  ")" )) "holds"  (Bool  "ex" (Set (Var "Choice")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool (Set (Set (Var "Choice"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))))) ; 
 begin  
theorem :: WELLORD2:19 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X")))  ($#r1_relat_2 :::"is_reflexive_in"::: )  (Set (Var "X")))) ; 
 
theorem :: WELLORD2:20 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X")))  ($#r8_relat_2 :::"is_transitive_in"::: )  (Set (Var "X")))) ; 
 
theorem :: WELLORD2:21 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X")))  ($#r4_relat_2 :::"is_antisymmetric_in"::: )  (Set (Var "X")))) ; 
 registration
cluster (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) )) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_wellord2 :::"RelIncl"::: )  "X") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: WELLORD2:22 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: WELLORD2:23 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))) ;