:: 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-2016 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:];