:: Zermelo's Theorem
:: by Bogdan Nowak and S{\l}awomir Bia{\l}ecki
::
:: Received October 27, 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, FUNCT_1, XBOOLE_0, ZFMISC_1, SUBSET_1, WELLORD1,
RELAT_2, TARSKI;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1,
WELLORD1;
constructors TARSKI, SUBSET_1, RELAT_2, WELLORD1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1;
requirements SUBSET, BOOLE;
begin
reserve a,b,x,y,z,z1,z2,z3,y1,y3,y4,A,B,C,D,G,M,N,X,Y,Z,W0,W00 for set,
R,S,T, W,W1,W2 for Relation,
F,H,H1 for Function;
theorem :: WELLSET1:1
for x being object holds
x in field R iff ex y being object st ([x,y] in R or [y,x] in R);
theorem :: WELLSET1:2
X <> {} & Y <> {} & W = [: X,Y :] implies field W = X \/ Y;
scheme :: WELLSET1:sch 1
RSeparation { A()-> set, P[Relation] } :
ex B st for R being Relation holds R in B iff R in A() & P[R];
theorem :: WELLSET1:3
for x,y,W st x in field W & y in field W & W is well-ordering
holds not x in W-Seg(y) implies [y,x] in W;
theorem :: WELLSET1:4
for x,y,W st x in field W & y in field W & W is well-ordering
holds x in W-Seg(y) implies not [y,x] in W;
theorem :: WELLSET1:5
for F,D st (for X st X in D holds not F.X in X & F.X in union D)
ex R st field R c= union D & R is well-ordering & not field R in D & for y st y
in field R holds R-Seg(y) in D & F.(R-Seg(y)) = y;
theorem :: WELLSET1:6
for N ex R st R is well-ordering & field R = N;