:: Zermelo Theorem and Axiom of Choice. The correspondence of :: well ordering relations and ordinal numbers :: by Grzegorz Bancerek :: :: Received June 26, 1989 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies RELAT_1, ORDINAL1, TARSKI, RELAT_2, WELLORD1, XBOOLE_0, SUBSET_1, ZFMISC_1, FUNCT_1, WELLORD2; notations TARSKI, XBOOLE_0, ZFMISC_1, MCART_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, WELLORD1, ORDINAL1; constructors RELAT_2, ORDINAL1, WELLORD1, MCART_1, XTUPLE_0; registrations RELAT_1, FUNCT_1, ORDINAL1, WELLORD1; requirements SUBSET, BOOLE; begin reserve X,Y,Z for set, a,b,c,d,x,y,z,u for object, R for Relation, A,B,C for Ordinal; definition let X; func RelIncl X -> Relation means :: WELLORD2:def 1 field it = X & for Y,Z st Y in X & Z in X holds [Y,Z] in it iff Y c= Z; end; ::$CT 6 registration let X; cluster RelIncl X -> reflexive; cluster RelIncl X -> transitive; cluster RelIncl X -> antisymmetric; end; registration let A; cluster RelIncl A -> connected; cluster RelIncl A -> well_founded; end; theorem :: WELLORD2:7 Y c= X implies (RelIncl X) |_2 Y = RelIncl Y; theorem :: WELLORD2:8 for A,X st X c= A holds RelIncl X is well-ordering; reserve H for Function; theorem :: WELLORD2:9 A in B implies A = (RelIncl B)-Seg(A); theorem :: WELLORD2:10 RelIncl A,RelIncl B are_isomorphic implies A = B; theorem :: WELLORD2:11 R,RelIncl A are_isomorphic & R,RelIncl B are_isomorphic implies A = B; theorem :: WELLORD2:12 for R st R is well-ordering & for a being object st a in field R ex A st R |_2 (R-Seg(a)),RelIncl A are_isomorphic ex A st R,RelIncl A are_isomorphic; theorem :: WELLORD2:13 for R st R is well-ordering ex A st R,RelIncl A are_isomorphic; definition let R; assume R is well-ordering; func order_type_of R -> Ordinal means :: WELLORD2:def 2 R,RelIncl it are_isomorphic; end; definition let A,R; pred A is_order_type_of R means :: WELLORD2:def 3 A = order_type_of R; end; theorem :: WELLORD2:14 X c= A implies order_type_of RelIncl X c= A; reserve f,g for Function; definition let X,Y; redefine pred X,Y are_equipotent means :: WELLORD2:def 4 ex f st f is one-to-one & dom f = X & rng f = Y; reflexivity; symmetry; end; theorem :: WELLORD2:15 X,Y are_equipotent & Y,Z are_equipotent implies X,Z are_equipotent; theorem :: WELLORD2:16 R well_orders X implies field(R|_2 X) = X & R|_2 X is well-ordering; ::$N Zermelo Theorem theorem :: WELLORD2:17 for X ex R st R well_orders X; reserve M for non empty set; ::$N Axiom of Choice theorem :: WELLORD2:18 (for X st X in M holds X <> {}) & (for X,Y st X in M & Y in M & X <> Y holds X misses Y) implies ex Choice being set st for X st X in M ex x being object st Choice /\ X = { x }; begin :: Addenda theorem :: WELLORD2:19 :: WAYBEL35:1, AK, 21.02.2006 for X being set holds RelIncl X is_reflexive_in X; theorem :: WELLORD2:20 :: WAYBEL35:1, AK, 21.02.2006 for X being set holds RelIncl X is_transitive_in X; theorem :: WELLORD2:21 :: WAYBEL35:1, AK, 21.02.2006 for X being set holds RelIncl X is_antisymmetric_in X; :: from AMISTD_2, 2010.01.10, A.T registration cluster RelIncl {} -> empty; end; registration let X be non empty set; cluster RelIncl X -> non empty; end; theorem :: WELLORD2:22 RelIncl {x} = {[x,x]}; theorem :: WELLORD2:23 RelIncl X c= [:X,X:];