:: Partially Ordered Sets
:: by Wojciech A. Trybulec
::
:: Received August 30, 1989
:: Copyright (c) 1990-2026 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 FUNCT_1, XBOOLE_0, TARSKI, SUBSET_1, ZFMISC_1, RELAT_1, PARTFUN1,
RELAT_2, ORDINAL1, WELLORD1, WELLORD2, SETFAM_1, FINSET_1, ORDERS_1,
CARD_3, PBOOLE;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, XTUPLE_0, MCART_1, ORDINAL1, WELLORD1,
SETFAM_1, WELLORD2, FINSET_1, PBOOLE;
constructors SETFAM_1, RELAT_2, WELLORD1, PARTFUN1, WELLORD2, FUNCT_2,
FINSET_1, RELSET_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, PARTFUN1, FINSET_1,
RELSET_1, WELLORD2, FUNCT_1, RELAT_2, PBOOLE;
requirements BOOLE, SUBSET;
definitions RELAT_2, TARSKI, WELLORD1, RELAT_1, ORDINAL1, XBOOLE_0;
equalities TARSKI, WELLORD1, RELAT_1;
expansions RELAT_2, TARSKI, WELLORD1, ORDINAL1, XBOOLE_0;
theorems FUNCT_1, FUNCT_2, RELAT_1, RELAT_2, RELSET_1, TARSKI, WELLORD1,
WELLORD2, ZFMISC_1, XBOOLE_0, XBOOLE_1, PARTFUN1, ORDINAL1, SETFAM_1,
XTUPLE_0;
schemes FUNCT_1, XBOOLE_0, ORDINAL1, TARSKI, RELSET_1, RELAT_1;
begin
reserve X,Y for set,
x,x1,x2,y,y1,y2,z for set,
f,g,h for Function;
Lm1: (ex X st X <> {} & X in Y) iff union Y <> {}
proof
thus (ex X st X <> {} & X in Y) implies union Y <> {}
proof
given X such that
A1: X <> {} and
A2: X in Y;
set x = the Element of X;
x in X by A1;
hence thesis by A2,TARSKI:def 4;
end;
set x = the Element of union Y;
assume union Y <> {};
then consider X such that
A3: x in X and
A4: X in Y by TARSKI:def 4;
take X;
thus thesis by A3,A4;
end;
::
:: Choice function.
::
definition let f be Function;
mode Choice of f -> Function means
:Def1: dom it = dom f &
for x being object st x in dom f holds it.x = the Element of f.x;
existence
proof
deffunc F(object) = the Element of f.$1;
consider g being Function such that
A1: dom g = dom f and
A2: for x being object st x in dom f holds g.x = F(x) from FUNCT_1:sch 3;
take g;
thus dom g = dom f by A1;
let x be object such that
A3: x in dom f;
reconsider x as set by TARSKI:1;
g.x = F(x) by A3,A2;
hence thesis;
end;
end;
definition let I be set; let M be ManySortedSet of I;
redefine mode Choice of M -> ManySortedSet of I means :: redefines Choice (ORDERS_1, definition)
:Def2:
for x being object st x in I holds it.x = the Element of M.x;
coherence
proof let Ch be Choice of M;
dom Ch = dom M by Def1
.= I by PARTFUN1:def 2;
then Ch is total I-defined Function by RELAT_1:def 18,PARTFUN1:def 2;
hence thesis;
end;
compatibility
proof let Ch be ManySortedSet of I;
dom M = I by PARTFUN1:def 2;
hence Ch is Choice of M implies
for x being object st x in I holds Ch.x = the Element of M.x by Def1;
assume
A1: for x being object st x in I holds Ch.x = the Element of M.x;
thus dom Ch = I by PARTFUN1:def 2 .= dom M by PARTFUN1:def 2;
thus for x being object st x in dom M holds Ch.x = the Element of M.x
by A1;
end;
end;
definition let A be set;
mode Choice_Function of A is Choice of id A;
end;
reserve M for non empty set;
Lm2:
not {} in M implies
for Ch being Choice_Function of M
for X st X in M holds Ch.X in X
proof assume
A1: not {} in M;
let Ch be Choice_Function of M;
let X;
assume
A2: X in M;
then
A3: X <> {} by A1;
A4: (id M).X = X by A2,FUNCT_1:18;
X in dom Ch by A2,PARTFUN1:def 2;
then Ch.X = the Element of (id M).X by Def2
.= the Element of X by A4;
hence Ch.X in X by A3;
end;
Lm3:
not {} in M implies
for Ch being Choice_Function of M
holds Ch is Function of M, union M
proof assume
A1: not {} in M;
let Ch be Choice_Function of M;
A2: dom Ch = M by PARTFUN1:def 2;
rng Ch c= union M
proof let x be object;
assume x in rng Ch;
then consider y being object such that
A3: y in dom Ch and
A4: x = Ch.y by FUNCT_1:def 3;
reconsider y as set by TARSKI:1;
A5: x in y by A3,A1,A4,Lm2;
y in M by A3;
hence x in union M by A5,TARSKI:def 4;
end;
hence Ch is Function of M, union M by A2,FUNCT_2:2;
end;
reserve D for non empty set;
definition
let D be set;
func BOOL D -> set equals
bool D \ {{}};
coherence;
end;
registration
let D;
cluster BOOL D -> non empty;
coherence
proof
A1: not D in {{}} by TARSKI:def 1;
D in bool D by ZFMISC_1:def 1;
hence thesis by A1,XBOOLE_0:def 5;
end;
end;
theorem
not {} in BOOL D
proof
assume not thesis;
then not {} in {{}} by XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
theorem
D c= X iff D in BOOL X
proof
thus D c= X implies D in BOOL X
proof
A1: not D in {{}} by TARSKI:def 1;
assume D c= X;
hence thesis by A1,XBOOLE_0:def 5;
end;
assume D in BOOL X;
hence thesis;
end;
reserve P for Relation;
::
:: Orders.
::
definition
let X;
mode Order of X is total reflexive antisymmetric transitive Relation of X;
end;
reserve O for Order of X;
Lm4: for R being total Relation of X holds field R = X
proof
let R be total Relation of X;
thus field R = X \/ rng R by PARTFUN1:def 2
.= X by XBOOLE_1:12;
end;
theorem Th3:
x in X implies [x,x] in O
proof
field O = X by Lm4;
then O is_reflexive_in X by RELAT_2:def 9;
hence thesis;
end;
theorem
x in X & y in X & [x,y] in O & [y,x] in O implies x = y
proof
field O = X by Lm4;
then O is_antisymmetric_in X by RELAT_2:def 12;
hence thesis;
end;
theorem
x in X & y in X & z in X & [x,y] in O & [y,z] in O implies [x,z] in O
proof
field O = X by Lm4;
then O is_transitive_in X by RELAT_2:def 16;
hence thesis;
end;
theorem
(ex X st X <> {} & X in Y) iff union Y <> {} by Lm1;
theorem
P is_strongly_connected_in X iff P is_reflexive_in X & P is_connected_in X
proof
thus P is_strongly_connected_in X implies P is_reflexive_in X & P
is_connected_in X;
assume that
A1: P is_reflexive_in X and
A2: P is_connected_in X;
let x,y be object;
assume that
A3: x in X and
A4: y in X;
x = y implies thesis by A1,A3;
hence thesis by A2,A3,A4;
end;
theorem
P is_reflexive_in X & Y c= X implies P is_reflexive_in Y;
theorem
P is_antisymmetric_in X & Y c= X implies P is_antisymmetric_in Y;
theorem
P is_transitive_in X & Y c= X implies P is_transitive_in Y;
theorem
P is_strongly_connected_in X & Y c= X implies P is_strongly_connected_in Y;
theorem
for R being total Relation of X holds field R = X by Lm4;
theorem Th13:
for A being set, R being Relation of A st R is_reflexive_in A
holds dom R = A & field R = A
proof
let A be set, R be Relation of A such that
A1: R is_reflexive_in A;
A2: A c= dom R
proof
let x be object;
assume x in A;
then [x,x] in R by A1;
hence thesis by XTUPLE_0:def 12;
end;
hence dom R = A;
thus field R = A \/ rng R by A2,XBOOLE_0:def 10
.= A by XBOOLE_1:12;
end;
begin :: Originally ORDERS_2
reserve R,P for Relation,
X,X1,X2,Y,Z,x,y,z,u for set,
g,h for Function,
O for Order of X,
D for non empty set,
d,d1,d2 for Element of D,
A1,A2,B for Ordinal,
L,L1,L2 for Sequence;
::
:: Orders.
::
theorem Th14:
dom O = X & rng O = X
proof
thus dom O = X
proof
thus dom O c= X;
let x be object;
assume x in X;
then [x,x] in O by Th3;
hence thesis by XTUPLE_0:def 12;
end;
thus rng O c= X;
let x be object;
assume x in X;
then [x,x] in O by Th3;
hence thesis by XTUPLE_0:def 13;
end;
theorem
field O = X
proof
thus X = X \/ X .= dom O \/ X by Th14
.= field O by Th14;
end;
definition
let R;
attr R is being_quasi-order means
R is reflexive transitive;
attr R is being_partial-order means
R is reflexive transitive antisymmetric;
attr R is being_linear-order means
R is reflexive transitive antisymmetric connected;
end;
theorem
R is being_quasi-order implies R~ is being_quasi-order;
theorem
R is being_partial-order implies R~ is being_partial-order;
Lm5: R is connected implies R~ is connected
proof
assume
A1: for x,y being object holds
x in field R & y in field R & x <> y implies [x,y] in R or [y,x] in R;
let x,y be object;
assume that
A2: x in field(R~) and
A3: y in field(R~) and
A4: x <> y;
field R = field(R~) by RELAT_1:21;
then [x,y] in R or [y,x] in R by A1,A2,A3,A4;
hence thesis by RELAT_1:def 7;
end;
theorem Th18:
R is being_linear-order implies R~ is being_linear-order
by Lm5;
theorem
R is well-ordering implies R is being_quasi-order & R is
being_partial-order & R is being_linear-order;
theorem
R is being_linear-order implies R is being_quasi-order & R is
being_partial-order;
theorem
R is being_partial-order implies R is being_quasi-order;
theorem
O is being_partial-order;
theorem
O is being_quasi-order;
theorem
O is connected implies O is being_linear-order;
Lm6: R c= [:field R,field R:]
proof
let y,z be object;
assume
A1: [y,z] in R;
then
A2: z in field R by RELAT_1:15;
y in field R by A1,RELAT_1:15;
hence thesis by A2,ZFMISC_1:87;
end;
Lm7: R is reflexive & X c= field R implies field(R|_2 X) = X
proof
assume that
A1: for x being object holds x in field R implies [x,x] in R and
A2: X c= field R;
thus field(R|_2 X) c= X
by WELLORD1:12;
let y be object;
assume
A3: y in X;
then
A4: [y,y] in [:X,X:] by ZFMISC_1:87;
[y,y] in R by A1,A2,A3;
then [y,y] in R|_2 X by A4,XBOOLE_0:def 4;
hence thesis by RELAT_1:15;
end;
theorem
R is being_quasi-order implies R|_2 X is being_quasi-order
by WELLORD1:15,WELLORD1:17;
theorem
R is being_partial-order implies R|_2 X is being_partial-order
by WELLORD1:15,WELLORD1:17;
theorem
R is being_linear-order implies R|_2 X is being_linear-order
by WELLORD1:15,WELLORD1:16,WELLORD1:17;
registration let R be empty Relation;
cluster field R -> empty;
coherence;
end;
registration
cluster empty -> being_quasi-order being_partial-order
being_linear-order well-ordering for Relation;
coherence
proof
let R be Relation such that
A1: R is empty;
thus
A2: R is reflexive by A1;
thus
A3: R is transitive by A1;
hence R is reflexive & R is transitive by A2;
thus
A4: R is antisymmetric by A1;
hence R is reflexive & R is transitive & R is antisymmetric by A2,A3;
thus R is connected by A1;
hence R is reflexive & R is transitive & R is antisymmetric & R is
connected by A2,A3,A4;
let Y;
assume that
A5: Y c= field R and
A6: Y <> {};
thus thesis by A5,A6,A1;
end;
end;
registration let X;
cluster id X -> being_quasi-order being_partial-order;
coherence;
end;
definition
let R,X;
pred R quasi_orders X means
R is_reflexive_in X & R is_transitive_in X;
pred R partially_orders X means
R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X;
pred R linearly_orders X means
R is_reflexive_in X & R is_transitive_in X &
R is_antisymmetric_in X & R is_connected_in X;
end;
theorem Th28:
R well_orders X implies R quasi_orders X & R partially_orders X
& R linearly_orders X;
theorem Th29:
R linearly_orders X implies R quasi_orders X & R partially_orders X;
theorem
R partially_orders X implies R quasi_orders X;
theorem Th31:
R is being_quasi-order implies R quasi_orders field R
proof
assume that
A1: R is_reflexive_in field R and
A2: R is_transitive_in field R;
thus R is_reflexive_in field R & R is_transitive_in field R by A1,A2;
end;
theorem
R quasi_orders Y & X c= Y implies R quasi_orders X
proof
assume that
A1: R is_reflexive_in Y and
A2: R is_transitive_in Y and
A3: X c= Y;
thus R is_reflexive_in X & R is_transitive_in X by A1,A2,A3;
end;
Lm8: R is_reflexive_in X implies R|_2 X is reflexive
proof
assume
A1: for x being object holds x in X implies [x,x] in R;
let x be object;
assume
A2: x in field(R|_2 X);
then x in X by WELLORD1:12;
then
A3: [x,x] in [:X,X:] by ZFMISC_1:87;
[x,x] in R by A1,A2,WELLORD1:12;
hence thesis by A3,XBOOLE_0:def 4;
end;
Lm9: R is_transitive_in X implies R|_2 X is transitive
proof
assume
A1: for x,y,z being object holds
x in X & y in X & z in X & [x,y] in R & [y,z] in R implies [x,z] in R;
let x,y,z be object;
assume that
A2: x in field(R|_2 X) and
A3: y in field(R|_2 X) and
A4: z in field(R|_2 X);
A5: z in X by A4,WELLORD1:12;
A6: x in X by A2,WELLORD1:12;
then
A7: [x,z] in [:X,X:] by A5,ZFMISC_1:87;
assume that
A8: [x,y] in R|_2 X and
A9: [y,z] in R|_2 X;
A10: [x,y] in R by A8,XBOOLE_0:def 4;
A11: [y,z] in R by A9,XBOOLE_0:def 4;
y in X by A3,WELLORD1:12;
then [x,z] in R by A1,A6,A5,A10,A11;
hence thesis by A7,XBOOLE_0:def 4;
end;
Lm10: R is_antisymmetric_in X implies R|_2 X is antisymmetric
proof
assume
A1: for x,y being object holds
x in X & y in X & [x,y] in R & [y,x] in R implies x = y;
let x,y be object;
assume that
A2: x in field(R|_2 X) and
A3: y in field(R|_2 X);
A4: y in X by A3,WELLORD1:12;
assume that
A5: [x,y] in R|_2 X and
A6: [y,x] in R|_2 X;
A7: [x,y] in R by A5,XBOOLE_0:def 4;
A8: [y,x] in R by A6,XBOOLE_0:def 4;
x in X by A2,WELLORD1:12;
hence thesis by A1,A4,A7,A8;
end;
Lm11: R is_connected_in X implies R|_2 X is connected
proof
assume
A1: for x,y being object holds
x in X & y in X & x <> y implies [x,y] in R or [y,x] in R;
let x,y be object;
assume that
A2: x in field(R|_2 X) and
A3: y in field(R|_2 X) and
A4: x <> y;
A5: y in X by A3,WELLORD1:12;
A6: x in X by A2,WELLORD1:12;
then
A7: [x,y] in [:X,X:] by A5,ZFMISC_1:87;
A8: [y,x] in [:X,X:] by A6,A5,ZFMISC_1:87;
[x,y] in R or [y,x] in R by A1,A4,A6,A5;
hence thesis by A7,A8,XBOOLE_0:def 4;
end;
theorem
R quasi_orders X implies R|_2 X is being_quasi-order
by Lm8,Lm9;
theorem Th34:
R is being_partial-order implies R partially_orders field R
proof
assume that
A1: R is_reflexive_in field R and
A2: R is_transitive_in field R and
A3: R is_antisymmetric_in field R;
thus R is_reflexive_in field R & R is_transitive_in field R & R
is_antisymmetric_in field R by A1,A2,A3;
end;
theorem
R partially_orders Y & X c= Y implies R partially_orders X
proof
assume that
A1: R is_reflexive_in Y and
A2: R is_transitive_in Y and
A3: R is_antisymmetric_in Y and
A4: X c= Y;
thus R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X by
A1,A2,A3,A4;
end;
theorem
R partially_orders X implies R|_2 X is being_partial-order
by Lm8,Lm9,Lm10;
theorem
R is being_linear-order implies R linearly_orders field R
proof
assume that
A1: R is_reflexive_in field R and
A2: R is_transitive_in field R and
A3: R is_antisymmetric_in field R and
A4: R is_connected_in field R;
thus R is_reflexive_in field R & R is_transitive_in field R & R
is_antisymmetric_in field R & R is_connected_in field R by A1,A2,A3,A4;
end;
theorem
R linearly_orders Y & X c= Y implies R linearly_orders X
proof
assume that
A1: R is_reflexive_in Y and
A2: R is_transitive_in Y and
A3: R is_antisymmetric_in Y and
A4: R is_connected_in Y and
A5: X c= Y;
thus R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X &
R is_connected_in X by A1,A2,A3,A4,A5;
end;
theorem
R linearly_orders X implies R|_2 X is being_linear-order
by Lm8,Lm9,Lm10,Lm11;
Lm12: R is_reflexive_in X implies R~ is_reflexive_in X
proof
assume
A1: for x being object holds x in X implies [x,x] in R;
let x be object;
assume x in X;
then [x,x] in R by A1;
hence thesis by RELAT_1:def 7;
end;
Lm13: R is_transitive_in X implies R~ is_transitive_in X
proof
assume
A1: for x,y,z being object holds
x in X & y in X & z in X & [x,y] in R & [y,z] in R implies [x,z] in R;
let x,y,z be object;
assume that
A2: x in X and
A3: y in X and
A4: z in X and
A5: [x,y] in R~ and
A6: [y,z] in R~;
A7: [z,y] in R by A6,RELAT_1:def 7;
[y,x] in R by A5,RELAT_1:def 7;
then [z,x] in R by A1,A2,A3,A4,A7;
hence thesis by RELAT_1:def 7;
end;
Lm14: R is_antisymmetric_in X implies R~ is_antisymmetric_in X
proof
assume
A1: for x,y being object holds
x in X & y in X & [x,y] in R & [y,x] in R implies x = y;
let x,y be object;
assume that
A2: x in X and
A3: y in X and
A4: [x,y] in R~ and
A5: [y,x] in R~;
A6: [y,x] in R by A4,RELAT_1:def 7;
[x,y] in R by A5,RELAT_1:def 7;
hence thesis by A1,A2,A3,A6;
end;
Lm15: R is_connected_in X implies R~ is_connected_in X
proof
assume
A1: for x,y being object holds
x in X & y in X & x <> y implies [x,y] in R or [y,x] in R;
let x,y be object;
assume that
A2: x in X and
A3: y in X and
A4: x <> y;
[x,y] in R or [y,x] in R by A1,A2,A3,A4;
hence thesis by RELAT_1:def 7;
end;
theorem
R quasi_orders X implies R~ quasi_orders X
by Lm12,Lm13;
theorem Th41:
R partially_orders X implies R~ partially_orders X
by Lm12,Lm13,Lm14;
theorem
R linearly_orders X implies R~ linearly_orders X
by Lm12,Lm13,Lm14,Lm15;
theorem
O quasi_orders X
proof
A1: field O = X by Lm4;
then
A2: O is_transitive_in X by RELAT_2:def 16;
O is_reflexive_in X by A1,RELAT_2:def 9;
hence thesis by A2;
end;
theorem
O partially_orders X
proof
A1: field O = X by Lm4;
then
A2: O is_antisymmetric_in X by RELAT_2:def 12;
A3: O is_transitive_in X by A1,RELAT_2:def 16;
O is_reflexive_in X by A1,RELAT_2:def 9;
hence thesis by A2,A3;
end;
theorem Th45:
R partially_orders X implies R |_2 X is Order of X
proof
set S = R |_2 X;
A1: field S c= X by WELLORD1:13;
rng S c= field S by XBOOLE_1:7;
then
A2: rng S c= X by A1;
dom S c= field S by XBOOLE_1:7;
then dom S c= X by A1;
then reconsider S as Relation of X by A2,RELSET_1:4;
assume
A3: R partially_orders X;
A4: R |_2 X is_antisymmetric_in X
proof
A5: R is_antisymmetric_in X by A3;
let x,y be object;
assume that
A6: x in X and
A7: y in X and
A8: [x,y] in R |_2 X and
A9: [y,x] in R |_2 X;
A10: [y,x] in R by A9,XBOOLE_0:def 4;
[x,y] in R by A8,XBOOLE_0:def 4;
hence thesis by A6,A7,A10,A5;
end;
A11: R |_2 X is_transitive_in X
proof
A12: R is_transitive_in X by A3;
let x,y,z be object;
assume that
A13: x in X and
A14: y in X and
A15: z in X and
A16: [x,y] in R |_2 X and
A17: [y,z] in R |_2 X;
A18: [x,z] in [:X,X:] by A13,A15,ZFMISC_1:87;
A19: [y,z] in R by A17,XBOOLE_0:def 4;
[x,y] in R by A16,XBOOLE_0:def 4;
then [x,z] in R by A13,A14,A15,A19,A12;
hence thesis by A18,XBOOLE_0:def 4;
end;
A20: R is_reflexive_in X by A3;
A21: R |_2 X is_reflexive_in X
proof
let x be object;
assume
A22: x in X;
then
A23: [x,x] in [:X,X:] by ZFMISC_1:87;
[x,x] in R by A20,A22;
hence thesis by A23,XBOOLE_0:def 4;
end;
then
A24: field S = X by Th13;
dom S = X by A21,Th13;
hence thesis by A21,A24,A4,A11,PARTFUN1:def 2,RELAT_2:def 9,def 12,def 16;
end;
theorem
R linearly_orders X implies R |_2 X is Order of X by Th29,Th45;
theorem
R well_orders X implies R |_2 X is Order of X by Th28,Th45;
theorem
id X quasi_orders X & id X partially_orders X
proof
field id X = X \/ rng id X
.= X \/ X
.= X;
hence thesis by Th31,Th34;
end;
definition
let R,X;
pred X has_upper_Zorn_property_wrt R means
for Y st Y c= X & R|_2 Y
is being_linear-order ex x st x in X & for y st y in Y holds [y,x] in R;
pred X has_lower_Zorn_property_wrt R means
for Y st Y c= X & R|_2 Y is
being_linear-order ex x st x in X & for y st y in Y holds [x,y] in R;
end;
Lm16: (R|_2 X)~ = R~|_2 X
proof
now
let x,y be object;
thus [x,y] in R~|_2 X implies [y,x] in R|_2 X
proof
assume
A1: [x,y] in R~|_2 X;
then [x,y] in [:X,X:] by XBOOLE_0:def 4;
then
A2: [y,x] in [:X,X:] by ZFMISC_1:88;
[x,y] in R~ by A1,XBOOLE_0:def 4;
then [y,x] in R by RELAT_1:def 7;
hence thesis by A2,XBOOLE_0:def 4;
end;
assume
A3: [y,x] in R|_2 X;
then [y,x] in [:X,X:] by XBOOLE_0:def 4;
then
A4: [x,y] in [:X,X:] by ZFMISC_1:88;
[y,x] in R by A3,XBOOLE_0:def 4;
then [x,y] in R~ by RELAT_1:def 7;
hence [x,y] in R~|_2 X by A4,XBOOLE_0:def 4;
end;
hence thesis by RELAT_1:def 7;
end;
Lm17: now
let R;
thus R|_2 {} = {}|`R|{} by WELLORD1:10
.= {};
end;
theorem Th49:
X has_upper_Zorn_property_wrt R implies X <> {}
proof
assume
A1: for Y st Y c= X & R|_2 Y is being_linear-order ex x st x in X & for
y st y in Y holds [y,x] in R;
R|_2 {} is being_linear-order by Lm17;
then ex x st x in X & for y st y in {} holds [y,x] in R by A1,XBOOLE_1:2;
hence thesis;
end;
theorem
X has_lower_Zorn_property_wrt R implies X <> {}
proof
assume
A1: for Y st Y c= X & R|_2 Y is being_linear-order ex x st x in X & for
y st y in Y holds [x,y] in R;
R|_2 {} is being_linear-order by Lm17;
then ex x st x in X & for y st y in {} holds [x,y] in R by A1,XBOOLE_1:2;
hence thesis;
end;
theorem Th51:
X has_upper_Zorn_property_wrt R iff X has_lower_Zorn_property_wrt R~
proof
thus X has_upper_Zorn_property_wrt R implies X has_lower_Zorn_property_wrt R
~
proof
assume
A1: for Y st Y c= X & R|_2 Y is being_linear-order ex x st x in X &
for y st y in Y holds [y,x] in R;
let Y;
A2: (R|_2 Y)~~ = R|_2 Y;
assume that
A3: Y c= X and
A4: R~|_2 Y is being_linear-order;
R~|_2 Y = (R|_2 Y)~ by Lm16;
then consider x such that
A5: x in X and
A6: for y st y in Y holds [y,x] in R by A1,A2,A3,A4,Th18;
take x;
thus x in X by A5;
let y;
assume y in Y;
then [y,x] in R by A6;
hence thesis by RELAT_1:def 7;
end;
assume
A7: for Y st Y c= X & R~|_2 Y is being_linear-order ex x st x in X &
for y st y in Y holds [x,y] in R~;
let Y;
assume that
A8: Y c= X and
A9: R|_2 Y is being_linear-order;
R~|_2 Y = (R|_2 Y)~ by Lm16;
then consider x such that
A10: x in X and
A11: for y st y in Y holds [x,y] in R~ by A7,A8,A9,Th18;
take x;
thus x in X by A10;
let y;
assume y in Y;
then [x,y] in R~ by A11;
hence thesis by RELAT_1:def 7;
end;
theorem
X has_upper_Zorn_property_wrt R~ iff X has_lower_Zorn_property_wrt R
proof
R~~ = R;
hence thesis by Th51;
end;
definition
let R,x;
pred x is_maximal_in R means
x in field R & not ex y st y in field R & y <> x & [x,y] in R;
pred x is_minimal_in R means
x in field R & not ex y st y in field R & y <> x & [y,x] in R;
pred x is_superior_of R means
x in field R & for y st y in field R & y <> x holds [y,x] in R;
pred x is_inferior_of R means
x in field R & for y st y in field R & y <> x holds [x,y] in R;
end;
theorem
x is_inferior_of R & R is antisymmetric implies x is_minimal_in R
proof
assume that
A1: x is_inferior_of R and
A2: R is antisymmetric;
A3: R is_antisymmetric_in field R by A2;
thus
A4: x in field R by A1;
let y;
assume that
A5: y in field R and
A6: y <> x and
A7: [y,x] in R;
[x,y] in R by A1,A5,A6;
hence thesis by A4,A5,A6,A7,A3;
end;
theorem
x is_superior_of R & R is antisymmetric implies x is_maximal_in R
proof
assume that
A1: x is_superior_of R and
A2: R is antisymmetric;
A3: R is_antisymmetric_in field R by A2;
thus
A4: x in field R by A1;
let y;
assume that
A5: y in field R and
A6: y <> x and
A7: [x,y] in R;
[y,x] in R by A1,A5,A6;
hence thesis by A4,A5,A6,A7,A3;
end;
theorem
x is_minimal_in R & R is connected implies x is_inferior_of R
proof
assume that
A1: x is_minimal_in R and
A2: R is connected;
thus
A3: x in field R by A1;
let y;
assume that
A4: y in field R and
A5: y <> x;
R is_connected_in field R by A2;
then [x,y] in R or [y,x] in R by A3,A4,A5;
hence thesis by A1,A4;
end;
theorem
x is_maximal_in R & R is connected implies x is_superior_of R
proof
assume that
A1: x is_maximal_in R and
A2: R is connected;
thus
A3: x in field R by A1;
let y;
assume that
A4: y in field R and
A5: y <> x;
R is_connected_in field R by A2;
then [x,y] in R or [y,x] in R by A3,A4,A5;
hence thesis by A1,A4;
end;
theorem
x in X & x is_superior_of R & X c= field R & R is reflexive implies X
has_upper_Zorn_property_wrt R
proof
assume that
A1: x in X and
A2: x is_superior_of R and
A3: X c= field R and
A4: R is_reflexive_in field R;
let Y such that
A5: Y c= X and
R|_2 Y is being_linear-order;
take x;
thus x in X by A1;
let y;
assume y in Y;
then
A6: y in X by A5;
y = x or y <> x;
hence thesis by A2,A3,A4,A6;
end;
theorem
x in X & x is_inferior_of R & X c= field R & R is reflexive implies X
has_lower_Zorn_property_wrt R
proof
assume that
A1: x in X and
A2: x is_inferior_of R and
A3: X c= field R and
A4: R is_reflexive_in field R;
let Y such that
A5: Y c= X and
R|_2 Y is being_linear-order;
take x;
thus x in X by A1;
let y;
assume y in Y;
then
A6: y in X by A5;
y = x or y <> x;
hence thesis by A2,A3,A4,A6;
end;
theorem Th59:
x is_minimal_in R iff x is_maximal_in R~
proof
A1: field R = field(R~) by RELAT_1:21;
thus x is_minimal_in R implies x is_maximal_in R~
proof
assume that
A2: x in field R and
A3: not ex y st y in field R & y <> x & [y,x] in R;
thus x in field(R~) by A2,RELAT_1:21;
let y;
assume that
A4: y in field(R~) and
A5: y <> x;
not [y,x] in R by A1,A3,A4,A5;
hence thesis by RELAT_1:def 7;
end;
assume that
A6: x in field(R~) and
A7: not ex y st y in field(R~) & y <> x & [x,y] in R~;
thus x in field R by A6,RELAT_1:21;
let y;
assume that
A8: y in field R and
A9: y <> x;
not [x,y] in R~ by A1,A7,A8,A9;
hence thesis by RELAT_1:def 7;
end;
theorem
x is_minimal_in R~ iff x is_maximal_in R
proof
A1: field R = field(R~) by RELAT_1:21;
thus x is_minimal_in R~ implies x is_maximal_in R
proof
assume that
A2: x in field(R~) and
A3: not ex y st y in field(R~) & y <> x & [y,x] in R~;
thus x in field R by A2,RELAT_1:21;
let y;
assume that
A4: y in field R and
A5: y <> x;
not [y,x] in R~ by A1,A3,A4,A5;
hence thesis by RELAT_1:def 7;
end;
assume that
A6: x in field R and
A7: not ex y st y in field R & y <> x & [x,y] in R;
thus x in field(R~) by A6,RELAT_1:21;
let y;
assume that
A8: y in field(R~) and
A9: y <> x;
not [x,y] in R by A1,A7,A8,A9;
hence thesis by RELAT_1:def 7;
end;
theorem
x is_inferior_of R iff x is_superior_of R~
proof
A1: field R = field(R~) by RELAT_1:21;
thus x is_inferior_of R implies x is_superior_of R~
proof
assume that
A2: x in field R and
A3: for y st y in field R & y <> x holds [x,y] in R;
thus x in field(R~) by A2,RELAT_1:21;
let y;
assume that
A4: y in field(R~) and
A5: y <> x;
[x,y] in R by A1,A3,A4,A5;
hence thesis by RELAT_1:def 7;
end;
assume that
A6: x in field(R~) and
A7: for y st y in field(R~) & y <> x holds [y,x] in R~;
thus x in field R by A6,RELAT_1:21;
let y;
assume that
A8: y in field R and
A9: y <> x;
[y,x] in R~ by A1,A7,A8,A9;
hence thesis by RELAT_1:def 7;
end;
theorem
x is_inferior_of R~ iff x is_superior_of R
proof
A1: field R = field(R~) by RELAT_1:21;
thus x is_inferior_of R~ implies x is_superior_of R
proof
assume that
A2: x in field(R~) and
A3: for y st y in field(R~) & y <> x holds [x,y] in R~;
thus x in field R by A2,RELAT_1:21;
let y;
assume that
A4: y in field R and
A5: y <> x;
[x,y] in R~ by A1,A3,A4,A5;
hence thesis by RELAT_1:def 7;
end;
assume that
A6: x in field R and
A7: for y st y in field R & y <> x holds [y,x] in R;
thus x in field(R~) by A6,RELAT_1:21;
let y;
assume that
A8: y in field(R~) and
A9: y <> x;
[y,x] in R by A1,A7,A8,A9;
hence thesis by RELAT_1:def 7;
end;
Lm18: R well_orders X & Y c= X implies R well_orders Y
proof
assume that
A1: R well_orders X and
A2: Y c= X;
A3: R is_transitive_in X by A1;
A4: R is_connected_in X by A1;
A5: R is_antisymmetric_in X by A1;
A6: R is_well_founded_in X by A1;
R is_reflexive_in X by A1;
hence R is_reflexive_in Y & R is_transitive_in Y & R is_antisymmetric_in Y &
R is_connected_in Y by A2,A3,A5,A4;
let Z;
assume that
A7: Z c= Y and
A8: Z <> {};
Z c= X by A2,A7;
hence thesis by A8,A6;
end;
::
:: Kuratowski - Zorn Lemma.
::
reserve A,C for Ordinal;
theorem Th63:
for R,X st R partially_orders X & field R = X & X
has_upper_Zorn_property_wrt R ex x st x is_maximal_in R
proof
let R;
let FIELD be set;
assume that
A1: R is_reflexive_in FIELD and
A2: R is_transitive_in FIELD and
A3: R is_antisymmetric_in FIELD and
A4: field R = FIELD and
A5: FIELD has_upper_Zorn_property_wrt R;
reconsider XD = FIELD as non empty set by A5,Th49;
consider D such that
A6: D = XD;
A7: D in bool D by ZFMISC_1:def 1;
not D in {{}} by TARSKI:def 1;
then reconsider M = (bool D) \ {{}} as non empty set by A7,XBOOLE_0:def 5;
set f = the Choice_Function of M;
defpred P[object,object] means $1 <> {} & $2 = f.$1 or $1 = {} & $2 = D;
A8: for x being object st x in bool D ex y being object st P[x,y]
proof
let x being object such that
x in bool D;
x = {} implies thesis;
hence thesis;
end;
A9: for x,y,z being object st x in bool D & P[x,y] & P[x,z] holds y = z;
consider g such that
A10: dom g = bool D &
for x being object st x in bool D holds P[x,g.x] from FUNCT_1:
sch 2 (A9,A8);
defpred ON[Ordinal,object] means
ex L st $2 = g.{ d : for x st x in rng L holds
x <> d & [x,d] in R } & dom L = $1 & for A,L1 st A in $1 & L1 = L|A holds L.A =
g.{ d1 : for x st x in rng L1 holds x <> d1 & [x,d1] in R };
A11: ON[A,x] & ON[A,y] implies x = y
proof
given L1 such that
A12: x = g.{ d1 : for x st x in rng L1 holds x <> d1 & [x,d1] in R } and
A13: dom L1 = A & for C,L st C in A & L = L1|C holds L1.C = g.{ d2 :
for x st x in rng L holds x <> d2 & [x,d2] in R };
A14: L1 = L1|A by A13;
given L2 such that
A15: y = g.{ d1 : for x st x in rng L2 holds x <> d1 & [x,d1] in R } and
A16: dom L2 = A & for C,L st C in A & L = L2|C holds L2.C = g.{ d2 :
for x st x in rng L holds x <> d2 & [x,d2] in R };
defpred P[Ordinal] means $1 c= A implies L1|$1 = L2|$1;
A17: for A1 st for A2 st A2 in A1 holds P[A2] holds P[A1]
proof
let A1 such that
A18: for A2 st A2 in A1 holds A2 c= A implies L1|A2 = L2|A2 and
A19: A1 c= A;
A20: dom(L2|A1) = A1 by A16,A19,RELAT_1:62;
A21: now
let x be object;
assume
A22: x in A1;
then reconsider A3 = x as Ordinal;
A23: L1.x = L1|A1.x by A22,FUNCT_1:49;
A3 c= A by A19,A22,ORDINAL1:def 2;
then
A24: L1|A3 = L2|A3 by A18,A22;
A25: L2.A3 = g.{ d2 : for x st x in rng(L2|A3) holds x <> d2 & [x,d2]
in R } by A16,A19,A22;
L1.A3 = g.{ d1 : for x st x in rng(L1|A3) holds x <> d1 & [x,d1]
in R } by A13,A19,A22;
hence L1|A1.x = L2|A1.x by A22,A24,A23,A25,FUNCT_1:49;
end;
dom(L1|A1) = A1 by A13,A19,RELAT_1:62;
hence thesis by A20,A21,FUNCT_1:2;
end;
for A1 holds P[A1] from ORDINAL1:sch 2(A17);
then
A26: L1|A = L2|A;
L2 = L2|A by A16;
hence thesis by A12,A15,A26,A14;
end;
{} in {{}} by TARSKI:def 1;
then
A27: not {} in M by XBOOLE_0:def 5;
A28: X in bool D & X <> {} implies g.X in X
proof
assume that
A29: X in bool D and
A30: X <> {};
not X in {{}} by A30,TARSKI:def 1;
then
A31: X in M by A29,XBOOLE_0:def 5;
f.X = g.X by A10,A29,A30;
hence thesis by A27,A31,Lm2;
end;
defpred OM[Ordinal] means ON[$1,D];
{} c= D;
then
A32: g.{} = D by A10;
A33: now
let A,B,L1,L2;
assume that
A34: dom L1 = A & for C,L st C in A & L = L1|C holds L1.C = g.{ d2 :
for x st x in rng L holds x <> d2 & [x,d2] in R } and
A35: dom L2 = B & for C,L st C in B & L = L2|C holds L2.C = g.{ d2 :
for x st x in rng L holds x <> d2 & [x,d2] in R };
let C such that
A36: C c= A and
A37: C c= B;
defpred P[Ordinal] means $1 c= C implies L1|$1 = L2|$1;
A38: for A1 st for A2 st A2 in A1 holds P[A2] holds P[A1]
proof
let A1 such that
A39: for A2 st A2 in A1 holds A2 c= C implies L1|A2 = L2|A2 and
A40: A1 c= C;
A41: dom(L2|A1) = A1 by A35,A37,A40,RELAT_1:62,XBOOLE_1:1;
A42: now
let x be object;
assume
A43: x in A1;
then reconsider A3 = x as Ordinal;
A44: L1.x = L1|A1.x by A43,FUNCT_1:49;
A3 c= C by A40,A43,ORDINAL1:def 2;
then
A45: L1|A3 = L2|A3 by A39,A43;
A46: A3 in C by A40,A43;
then
A47: L2.A3 = g.{ d2 : for x st x in rng(L2|A3) holds x <> d2 & [x,d2]
in R } by A35,A37;
L1.A3 = g.{ d1 : for x st x in rng(L1|A3) holds x <> d1 & [x,d1]
in R } by A34,A36,A46;
hence L1|A1.x = L2|A1.x by A43,A45,A44,A47,FUNCT_1:49;
end;
dom(L1|A1) = A1 by A34,A36,A40,RELAT_1:62,XBOOLE_1:1;
hence thesis by A41,A42,FUNCT_1:2;
end;
for A1 holds P[A1] from ORDINAL1:sch 2(A38);
hence L1|C = L2|C;
end;
A48: for d,A,B st ON[A,d] & ON[B,d] holds A = B
proof
let d,A,B;
given L1 such that
A49: d = g.{ d1 : for x st x in rng L1 holds x <> d1 & [x,d1] in R } and
A50: dom L1 = A & for C,L st C in A & L = L1|C holds L1.C = g.{ d2 :
for x st x in rng L holds x <> d2 & [x,d2] in R };
given L2 such that
A51: d = g.{ d1 : for x st x in rng L2 holds x <> d1 & [x,d1] in R } and
A52: dom L2 = B & for C,L st C in B & L = L2|C holds L2.C = g.{ d2 :
for x st x in rng L holds x <> d2 & [x,d2] in R };
A53: now
set Y = { d1 : for x st x in rng L1 holds x <> d1 & [x,d1] in R };
set X = { d1 : for x st x in rng(L1|B) holds x <> d1 & [x,d1] in R };
A54: Y c= D
proof
let x be object;
assume x in Y;
then ex d1 st x = d1 & for x st x in rng L1 holds x <> d1 & [x,d1] in
R;
hence thesis;
end;
assume
A55: B in A;
then B c= A by ORDINAL1:def 2;
then
A56: L1|B = L2|B by A33,A50,A52
.= L2 by A52;
L1.B = g.X by A50,A55;
then
A57: d in rng L1 by A50,A51,A55,A56,FUNCT_1:def 3;
A58: now
assume
A59: Y <> {};
then not Y in {{}} by TARSKI:def 1;
then
A60: Y in M by A54,XBOOLE_0:def 5;
g.Y = f.Y by A10,A54,A59;
then d in Y by A27,A49,A60,Lm2;
then ex d1 st d = d1 & for x st x in rng L1 holds x <> d1 & [x,d1] in
R;
hence contradiction by A57;
end;
A61: not d in d;
P[Y,g.Y] by A10,A54;
hence contradiction by A49,A61,A58;
end;
now
set Y = { d1 : for x st x in rng L2 holds x <> d1 & [x,d1] in R };
set X = { d1 : for x st x in rng(L2|A) holds x <> d1 & [x,d1] in R };
A62: Y c= D
proof
let x be object;
assume x in Y;
then ex d1 st x = d1 & for x st x in rng L2 holds x <> d1 & [x,d1] in
R;
hence thesis;
end;
assume
A63: A in B;
then A c= B by ORDINAL1:def 2;
then
A64: L2|A = L1|A by A33,A50,A52
.= L1 by A50;
L2.A = g.X by A52,A63;
then
A65: d in rng L2 by A49,A52,A63,A64,FUNCT_1:def 3;
A66: now
assume
A67: Y <> {};
then not Y in {{}} by TARSKI:def 1;
then
A68: Y in M by A62,XBOOLE_0:def 5;
g.Y = f.Y by A10,A62,A67;
then d in Y by A27,A51,A68,Lm2;
then ex d1 st d = d1 & for x st x in rng L2 holds x <> d1 & [x,d1] in
R;
hence contradiction by A65;
end;
A69: not d in d;
P[Y,g.Y] by A10,A62;
hence contradiction by A51,A69,A66;
end;
hence thesis by A53,ORDINAL1:14;
end;
A70: ex A1 st OM[A1]
proof
defpred P[object,object] means ex A st $2 = A & ON[A,$1];
defpred OO[Ordinal] means ex d st ON[$1,d];
assume
A71: for A1 holds not ON[A1,D];
A72: for A st for B st B in A holds OO[B] holds OO[A]
proof
defpred P[object,object] means ex C st $1 = C & ON[C,$2];
let A such that
A73: for B st B in A ex d st ON[B,d];
A74: for x being object st x in A ex y being object st P[x,y]
proof
let x be object;
assume
A75: x in A;
then reconsider C = x as Ordinal;
consider d such that
A76: ON[C,d] by A73,A75;
reconsider y = d as set;
take y,C;
thus thesis by A76;
end;
A77: for x,y,z being object st x in A & P[x,y] & P[x,z] holds y = z by A11;
consider h such that
A78: dom h = A & for x being object st x in A holds P[x,h.x]
from FUNCT_1:sch 2(
A77,A74 );
reconsider h as Sequence by A78,ORDINAL1:def 7;
set X = { d1 : for x st x in rng h holds x <> d1 & [x,d1] in R };
A79: X c= D
proof
let x be object;
assume x in X;
then ex d1 st x = d1 & for x st x in rng h holds x <> d1 & [x,d1] in R;
hence thesis;
end;
A80: ON[A,g.X]
proof
take h;
thus g.X = g.{ d1 : for x st x in rng h holds x <> d1 & [x,d1] in R }
& dom h = A by A78;
let B,L;
assume that
A81: B in A and
A82: L = h|B;
ex C st B = C & ON[C,h.B] by A78,A81;
then consider L1 such that
A83: h.B = g.{d1: for x st x in rng L1 holds x <> d1 & [x,d1] in R } and
A84: dom L1 = B & for C,L st C in B & L = L1|C holds L1.C = g.{
d1: for x st x in rng L holds x <> d1 & [x,d1] in R };
A85: for x being object st x in B holds L1.x = h|B.x
proof
let x be object;
assume
A86: x in B;
then reconsider A1 = x as Ordinal;
A87: h|B.x = h.x by A86,FUNCT_1:49;
A88: ON[A1,L1.x]
proof
reconsider K = L1|A1 as Sequence;
take K;
thus L1.x = g.{d1: for x st x in rng K holds x <> d1 & [x,d1] in R
} by A84,A86;
A1 c= B by A86,ORDINAL1:def 2;
hence dom K = A1 by A84,RELAT_1:62;
let A2,L2;
assume that
A89: A2 in A1 and
A90: L2 = K|A2;
A2 c= A1 by A89,ORDINAL1:def 2;
then
A91: L2 = L1|A2 by A90,FUNCT_1:51;
K.A2 = L1.A2 by A89,FUNCT_1:49;
hence thesis by A84,A86,A89,A91,ORDINAL1:10;
end;
ex A2 st x = A2 & ON[A2,h.x] by A78,A81,A86,ORDINAL1:10;
hence thesis by A11,A88,A87;
end;
B c= A by A81,ORDINAL1:def 2;
then dom(h|B) = B by A78,RELAT_1:62;
then h|B = L1 by A84,A85,FUNCT_1:2;
hence thesis by A82,A83;
end;
then X <> {} by A32,A71;
then g.X in X by A28,A79;
then reconsider dd = g.X as Element of D by A79;
take dd;
thus thesis by A80;
end;
A92: for A holds OO[A] from ORDINAL1:sch 2(A72);
A93: for x,y,z being object st P[x,y] & P[x,z] holds y = z
proof
let x,y,z be object;
given A1 such that
A94: y = A1 and
A95: ON[A1,x];
consider d1 such that
A96: ON[A1,d1] by A92;
given A2 such that
A97: z = A2 and
A98: ON[A2,x];
d1 = x by A11,A95,A96;
hence thesis by A48,A94,A95,A97,A98;
end;
consider X such that
A99: for x being object holds x in X iff
ex y being object st y in D & P[y,x] from TARSKI:sch 1(A93);
for A holds A in X
proof
let A;
ex d st ON[A,d] by A92;
hence thesis by A99;
end;
hence contradiction by ORDINAL1:26;
end;
consider A such that
A100: OM[A] & for B st OM[B] holds A c= B from ORDINAL1:sch 1(A70);
A101: for L
holds { d : for x st x in rng L holds x <> d & [x,d] in R } c= D
proof
let L; let x be object;
assume x in { d : for x st x in rng L holds x <> d & [x,d] in R };
then ex d1 st x = d1 & for x st x in rng L holds x <> d1 & [x,d1] in R;
hence thesis;
end;
D in bool D by ZFMISC_1:def 1;
then reconsider d = g.D as Element of D by A28;
A102: d in D & ON[{},d]
proof
deffunc H(set) = {};
thus d in D;
consider L such that
A103: dom L = {} & for B,L1 st B in {} & L1 = L|B holds L.B = H(L1)
from ORDINAL1:sch 4;
take L;
A104: D c= { d1 : for x st x in rng L holds x <> d1 & [x,d1] in R }
proof
let x be object;
assume x in D;
then reconsider d = x as Element of D;
for x st x in rng L holds x <> d & [x,d] in R by A103,RELAT_1:42;
hence thesis;
end;
{ d1 : for x st x in rng L holds x <> d1 & [x,d1] in R } c= D by A101;
hence d = g.{ d1 : for x st x in rng L holds x <> d1 & [x,d1] in R } by
A104,XBOOLE_0:def 10;
thus dom L = {} by A103;
thus thesis;
end;
A105: {} c= A;
defpred P[object] means ex B st B in A & ON[B,$1];
consider X such that
A106: for x being object holds x in X iff x in D & P[x] from XBOOLE_0:sch 1;
not Y in Y;
then d <> D;
then {} <> A by A11,A100,A102;
then {} c< A by A105;
then {} in A by ORDINAL1:11;
then reconsider X as non empty set by A106,A102;
consider L such that
A107: D = g.{ d1 : for x st x in rng L holds x <> d1 & [x,d1] in R } and
A108: dom L = A & for B,L1 st B in A & L1 = L|B holds L.B = g.{ d2 : for
x st x in rng L1 holds x <> d2 & [x,d2] in R } by A100;
R is transitive by A2,A4;
then
A109: R|_2 X is transitive by WELLORD1:17;
A110: rng L c= X
proof
let z be object;
assume z in rng L;
then consider y being object such that
A111: y in dom L and
A112: z = L.y by FUNCT_1:def 3;
reconsider y as Ordinal by A111;
set Z = { d2 : for x st x in rng(L|y) holds x <> d2 & [x,d2] in R };
A113: Z c= D by A101;
A114: ON[y,z]
proof
reconsider K = L|y as Sequence;
take K;
thus z = g.{ d2 : for x st x in rng K holds x <> d2 & [x,d2] in R } by
A108,A111,A112;
y c= dom L by A111,ORDINAL1:def 2;
hence
A115: dom K = y by RELAT_1:62;
let B,L1;
assume that
A116: B in y and
A117: L1 = K|B;
B c= y by A116,ORDINAL1:def 2;
then
A118: L1 = L|B by A117,FUNCT_1:51;
K.B = L.B by A115,A116,FUNCT_1:47;
hence thesis by A108,A111,A116,A118,ORDINAL1:10;
end;
now
assume Z = {};
then z = D by A32,A108,A111,A112;
then dom L c= y by A100,A108,A114;
hence contradiction by A111,ORDINAL1:5;
end;
then g.Z in Z by A28,A113;
then z in Z by A108,A111,A112;
hence thesis by A106,A108,A111,A114,A113;
end;
A119: R|_2 X is connected
proof
let x,y be object;
assume that
A120: x in field(R|_2 X) and
A121: y in field(R|_2 X);
A122: x in X by A120,WELLORD1:12;
then consider A1 such that
A1 in A and
A123: ON[A1,x] by A106;
A124: y in X by A121,WELLORD1:12;
then consider A2 such that
A2 in A and
A125: ON[A2,y] by A106;
reconsider x9 = x, y9 = y as Element of D by A106,A122,A124;
consider L1 such that
A126: x9 = g.{ d1 : for x st x in rng L1 holds x <> d1 & [x,d1] in R } and
A127: dom L1 = A1 & for C,L st C in A1 & L = L1|C holds L1.C = g.{ d2
: for x st x in rng L holds x <> d2 & [x,d2] in R } by A123;
consider L2 such that
A128: y9 = g.{ d1 : for x st x in rng L2 holds x <> d1 & [x,d1] in R } and
A129: dom L2 = A2 & for C,L st C in A2 & L = L2|C holds L2.C = g.{ d2
: for x st x in rng L holds x <> d2 & [x,d2] in R } by A125;
A130: [x,y] in [:X,X:] by A122,A124,ZFMISC_1:87;
A131: now
set Y = { d1 : for x st x in rng L2 holds x <> d1 & [x,d1] in R };
set Z = { d1 : for x st x in rng(L2|A1) holds x <> d1 & [x,d1] in R };
not y9 in y9;
then
A132: Y <> {} by A32,A128;
Y c= D by A101;
then y9 in Y by A28,A128,A132;
then
A133: ex d1 st y9 = d1 & for x st x in rng L2 holds x <> d1 & [x,d1] in R;
assume
A134: A1 in A2;
then A1 c= A2 by ORDINAL1:def 2;
then
A135: L2|A1 = L1|A1 by A33,A127,A129
.= L1 by A127;
L2.A1 = g.Z by A129,A134;
then x9 in rng L2 by A126,A129,A134,A135,FUNCT_1:def 3;
then [x,y] in R by A133;
hence thesis by A130,XBOOLE_0:def 4;
end;
A136: [y,x] in [:X,X:] by A122,A124,ZFMISC_1:87;
A137: now
set Y = { d1 : for x st x in rng L1 holds x <> d1 & [x,d1] in R };
set Z = { d1 : for x st x in rng(L1|A2) holds x <> d1 & [x,d1] in R };
not d1 in d1;
then
A138: Y <> {} by A32,A126;
Y c= D by A101;
then x9 in Y by A28,A126,A138;
then
A139: ex d1 st x9 = d1 & for x st x in rng L1 holds x <> d1 & [x,d1] in R;
assume
A140: A2 in A1;
then A2 c= A1 by ORDINAL1:def 2;
then
A141: L1|A2 = L2|A2 by A33,A127,A129
.= L2 by A129;
L1.A2 = g.Z by A127,A140;
then y9 in rng L1 by A127,A128,A140,A141,FUNCT_1:def 3;
then [y,x] in R by A139;
hence thesis by A136,XBOOLE_0:def 4;
end;
A1 = A2 implies thesis by A11,A123,A125;
hence thesis by A131,A137,ORDINAL1:14;
end;
R is antisymmetric by A3,A4;
then
A142: R|_2 X is antisymmetric;
set Z = { d1 : for x st x in rng L holds x <> d1 & [x,d1] in R };
A143: X c= D
by A106;
R is reflexive by A1,A4;
then R|_2 X is reflexive by WELLORD1:15;
then R|_2 X is being_linear-order by A109,A142,A119;
then consider x such that
A144: x in D and
A145: for y st y in X holds [y,x] in R by A5,A6,A143;
take x;
thus x in field R by A4,A6,A144;
let y such that
A146: y in field R and
A147: y <> x and
A148: [x,y] in R;
reconsider y9 = y as Element of D by A4,A6,A146;
A149: now
assume y in X;
then [y,x] in R by A145;
hence contradiction by A3,A4,A6,A144,A146,A147,A148;
end;
now
let z;
assume
A150: z in rng L;
then reconsider z9 = z as Element of X by A110;
thus z <> y9 by A110,A149,A150;
A151: [z9,x] in R by A145;
z in D by A106,A110,A150;
hence [z,y] in R by A2,A4,A6,A144,A146,A148,A151;
end;
then
A152: y in Z;
Z c= D by A101;
hence contradiction by A28,A107,A152,ORDINAL1:5;
end;
theorem Th64:
for R,X st R partially_orders X & field R = X & X
has_lower_Zorn_property_wrt R ex x st x is_minimal_in R
proof
let R,X such that
A1: R partially_orders X and
A2: field R = X and
A3: X has_lower_Zorn_property_wrt R;
R = R~~;
then
A4: X has_upper_Zorn_property_wrt R~ by A3,Th51;
field(R~) = X by A2,RELAT_1:21;
then consider x such that
A5: x is_maximal_in R~ by A1,A4,Th41,Th63;
take x;
thus thesis by A5,Th59;
end;
::$N Kuratowski-Zorn Lemma
::$N Zorn Lemma
::$L https://en.wikipedia.org/wiki/Zorn's_lemma Kuratowski-Zorn Lemma
theorem Th65:
for X st X <> {} & for Z st Z c= X & Z is c=-linear
ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y
ex Y st Y in X & for Z st Z in X & Z <> Y holds not Y c= Z
proof
let X;
assume that
A1: X <> {} and
A2: for Z st Z c= X & Z is c=-linear ex Y st Y in X & for X1 st X1 in Z
holds X1 c= Y;
reconsider D = X as non empty set by A1;
set R = RelIncl D;
A3: D has_upper_Zorn_property_wrt R
proof
let Z;
assume that
A4: Z c= D and
A5: R|_2 Z is being_linear-order;
set Q = R|_2 Z;
A6: Z c= field(R|_2 Z)
proof
let x be object;
assume
A7: x in Z;
then
A8: [x,x] in [:Z,Z:] by ZFMISC_1:87;
[x,x] in R by A4,A7,WELLORD2:def 1;
then [x,x] in R|_2 Z by A8,XBOOLE_0:def 4;
hence thesis by RELAT_1:15;
end;
R|_2 Z is connected by A5;
then
A9: R|_2 Z is_connected_in field(R|_2 Z);
Z is c=-linear
proof
let X1,X2;
assume that
A10: X1 in Z and
A11: X2 in Z;
X1 <> X2 implies [X1,X2] in Q or [X2,X1] in Q by A9,A6,A10,A11;
then X1 <> X2 implies [X1,X2] in R or [X2,X1] in R by XBOOLE_0:def 4;
hence X1 c= X2 or X2 c= X1 by A4,A10,A11,WELLORD2:def 1;
end;
then consider Y such that
A12: Y in X and
A13: for X1 st X1 in Z holds X1 c= Y by A2,A4;
take x = Y;
thus x in D by A12;
let y;
assume
A14: y in Z;
then y c= Y by A13;
hence thesis by A4,A12,A14,WELLORD2:def 1;
end;
A15: field R = D by WELLORD2:def 1;
A16: R is_antisymmetric_in D by A15,RELAT_2:def 12;
A17: R is_transitive_in D by A15,RELAT_2:def 16;
R is_reflexive_in D by A15,RELAT_2:def 9;
then R partially_orders D by A17,A16;
then consider x such that
A18: x is_maximal_in R by A15,A3,Th63;
take Y = x;
A19: Y in field R by A18;
thus Y in X by A15,A18;
let Z;
assume that
A20: Z in X and
A21: Z <> Y;
not [Y,Z] in R by A15,A18,A20,A21;
hence thesis by A15,A19,A20,WELLORD2:def 1;
end;
theorem Th66:
for X st X <> {} & for Z st Z c= X & Z is c=-linear ex Y st Y
in X & for X1 st X1 in Z holds Y c= X1 ex Y st Y in X & for Z st Z in X & Z <>
Y holds not Z c= Y
proof
let X;
assume that
A1: X <> {} and
A2: for Z st Z c= X & Z is c=-linear ex Y st Y in X & for X1 st X1 in Z
holds Y c= X1;
reconsider D = X as non empty set by A1;
set R = (RelIncl D)~;
A3: x in D implies [x,x] in R
proof
x in D implies [x,x] in RelIncl D by WELLORD2:def 1;
hence thesis by RELAT_1:def 7;
end;
A4: D has_upper_Zorn_property_wrt R
proof
let Z;
assume that
A5: Z c= D and
A6: R|_2 Z is being_linear-order;
set Q = R|_2 Z;
A7: Z c= field(R|_2 Z)
proof
let x be object;
assume
A8: x in Z;
then
A9: [x,x] in [:Z,Z:] by ZFMISC_1:87;
[x,x] in R by A3,A5,A8;
then [x,x] in R|_2 Z by A9,XBOOLE_0:def 4;
hence thesis by RELAT_1:15;
end;
R|_2 Z is connected by A6;
then
A10: R|_2 Z is_connected_in field(R|_2 Z);
Z is c=-linear
proof
let X1,X2;
assume that
A11: X1 in Z and
A12: X2 in Z;
X1 <> X2 implies [X1,X2] in Q or [X2,X1] in Q by A10,A7,A11,A12;
then X1 <> X2 implies [X1,X2] in R or [X2,X1] in R by XBOOLE_0:def 4;
then X1 <> X2 implies [X1,X2] in RelIncl D or [X2,X1] in RelIncl D by
RELAT_1:def 7;
hence X1 c= X2 or X2 c= X1 by A5,A11,A12,WELLORD2:def 1;
end;
then consider Y such that
A13: Y in X and
A14: for X1 st X1 in Z holds Y c= X1 by A2,A5;
take x = Y;
thus x in D by A13;
let y;
assume
A15: y in Z;
then Y c= y by A14;
then [Y,y] in RelIncl D by A5,A13,A15,WELLORD2:def 1;
hence thesis by RELAT_1:def 7;
end;
A16: field R = field RelIncl D by RELAT_1:21
.= D by WELLORD2:def 1;
A17: field RelIncl D = D by WELLORD2:def 1;
RelIncl D is_antisymmetric_in D by A17,RELAT_2:def 12;
then
A18: R is_antisymmetric_in D by Lm14;
RelIncl D is_transitive_in D by A17,RELAT_2:def 16;
then
A19: R is_transitive_in D by Lm13;
RelIncl D is_reflexive_in D by A17,RELAT_2:def 9;
then R is_reflexive_in D by Lm12;
then R partially_orders D by A19,A18;
then consider x such that
A20: x is_maximal_in R by A16,A4,Th63;
take Y = x;
A21: Y in field R by A20;
thus Y in X by A16,A20;
let Z;
assume that
A22: Z in X and
A23: Z <> Y;
not [Y,Z] in R by A16,A20,A22,A23;
then not [Z,Y] in RelIncl D by RELAT_1:def 7;
hence thesis by A16,A21,A22,WELLORD2:def 1;
end;
theorem Th67:
for X st X <> {} & for Z st Z <> {} & Z c= X & Z is c=-linear
holds union Z in X ex Y st Y in X & for Z st Z in X & Z <> Y holds not Y c= Z
proof
let X such that
A1: X <> {} and
A2: for Z st Z <> {} & Z c= X & Z is c=-linear holds union Z in X;
for Z st Z c= X & Z is c=-linear ex Y st Y in X & for X1 st X1 in Z
holds X1 c= Y
proof
set x = the Element of X;
let Z such that
A3: Z c= X and
A4: Z is c=-linear;
Z <> {} or Z = {};
then consider Y such that
A5: Y = union Z & Z <> {} or Y = x & Z = {};
take Y;
thus thesis by A1,A2,A3,A4,A5,ZFMISC_1:74;
end;
hence thesis by A1,Th65;
end;
theorem
for X st X <> {} & for Z st Z <> {} & Z c= X & Z is c=-linear holds
meet Z in X ex Y st Y in X & for Z st Z in X & Z <> Y holds not Z c= Y
proof
let X such that
A1: X <> {} and
A2: for Z st Z <> {} & Z c= X & Z is c=-linear holds meet Z in X;
for Z st Z c= X & Z is c=-linear ex Y st Y in X & for X1 st X1 in Z
holds Y c= X1
proof
set x = the Element of X;
let Z such that
A3: Z c= X and
A4: Z is c=-linear;
Z <> {} or Z = {};
then consider Y such that
A5: Y = meet Z & Z <> {} or Y = x & Z = {};
take Y;
thus thesis by A1,A2,A3,A4,A5,SETFAM_1:3;
end;
hence thesis by A1,Th66;
end;
scheme
ZornMax{A() -> non empty set, P[set,set]}: ex x being Element of A() st for
y being Element of A() st x <> y holds not P[x,y]
provided
A1: for x being Element of A() holds P[x,x] and
A2: for x,y being Element of A() st P[x,y] & P[y,x] holds x = y and
A3: for x,y,z being Element of A() st P[x,y] & P[y,z] holds P[x,z] and
A4: for X st X c= A() & (for x,y being Element of A() st x in X & y in X
holds P[x,y] or P[y,x]) holds ex y being Element of A() st for x being Element
of A() st x in X holds P[x,y]
proof
consider R being Relation of A() such that
A5: for x,y being Element of A() holds [x,y] in R iff P[x,y] from
RELSET_1:sch 2;
A6: R is_transitive_in A()
proof
let x,y,z be object;
assume that
A7: x in A() and
A8: y in A() and
A9: z in A();
reconsider x9 = x, y9 = y, z9 = z as Element of A() by A7,A8,A9;
assume that
A10: [x,y] in R and
A11: [y,z] in R;
A12: P[y9,z9] by A5,A11;
P[x9,y9] by A5,A10;
then P[x9,z9] by A3,A12;
hence thesis by A5;
end;
A() c= dom R
proof
let x be object;
assume x in A();
then reconsider x9 = x as Element of A();
P[x9,x9] by A1;
then [x,x] in R by A5;
hence thesis by XTUPLE_0:def 12;
end;
then dom R = A();
then
A13: A() c= field R by XBOOLE_1:7;
field R = dom R \/ rng R;
then
A14: field R = A() by A13;
A15: R is_reflexive_in A()
by A1,A5;
A16: A() has_upper_Zorn_property_wrt R
proof
let Y such that
A17: Y c= A() and
A18: R|_2 Y is being_linear-order;
for x,y being Element of A() st x in Y & y in Y holds P[x,y] or P[y,x ]
proof
let x,y be Element of A() such that
A19: x in Y and
A20: y in Y;
A21: R|_2 Y is reflexive connected by A18;
Y c= field(R|_2 Y)
proof
let x be object;
assume
A22: x in Y;
then
A23: [x,x] in [:Y,Y:] by ZFMISC_1:87;
[x,x] in R by A15,A17,A22;
then [x,x] in R|_2 Y by A23,XBOOLE_0:def 4;
hence thesis by RELAT_1:15;
end;
then
A24: Y = field(R|_2 Y|_2 Y) by A21,Lm7
.= field(R|_2 Y) by WELLORD1:21;
then
A25: R|_2 Y is_connected_in Y by A21;
A26: R|_2 Y is_reflexive_in Y by A21,A24;
x = y or x <> y;
then [x,y] in R|_2 Y or [y,x] in R|_2 Y by A19,A20,A25,A26;
then [x,y] in R or [y,x] in R by XBOOLE_0:def 4;
hence thesis by A5;
end;
then consider y being Element of A() such that
A27: for x being Element of A() st x in Y holds P[x,y] by A4,A17;
take y;
thus y in A();
let x;
assume
A28: x in Y;
then P[x,y] by A17,A27;
hence thesis by A5,A17,A28;
end;
R is_antisymmetric_in A()
proof
let x,y be object;
assume that
A29: x in A() and
A30: y in A();
reconsider x9 = x, y9 = y as Element of A() by A29,A30;
assume that
A31: [x,y] in R and
A32: [y,x] in R;
A33: P[y9,x9] by A5,A32;
P[x9,y9] by A5,A31;
hence thesis by A2,A33;
end;
then R partially_orders A() by A15,A6;
then consider x such that
A34: x is_maximal_in R by A14,A16,Th63;
take x;
thus x is Element of A() by A14,A34;
let y being Element of A();
assume x <> y;
then
A35: not [x,y] in R by A14,A34;
x in A() by A14,A34;
hence thesis by A5,A35;
end;
scheme
ZornMin{A() -> non empty set, P[set,set]}: ex x being Element of A() st for
y being Element of A() st x <> y holds not P[y,x]
provided
A1: for x being Element of A() holds P[x,x] and
A2: for x,y being Element of A() st P[x,y] & P[y,x] holds x = y and
A3: for x,y,z being Element of A() st P[x,y] & P[y,z] holds P[x,z] and
A4: for X st X c= A() & (for x,y being Element of A() st x in X & y in X
holds P[x,y] or P[y,x]) holds ex y being Element of A() st for x being Element
of A() st x in X holds P[y,x]
proof
consider R being Relation of A() such that
A5: for x,y being Element of A() holds [x,y] in R iff P[x,y] from
RELSET_1:sch 2;
A6: R is_transitive_in A()
proof
let x,y,z be object;
assume that
A7: x in A() and
A8: y in A() and
A9: z in A();
reconsider x9 = x, y9 = y, z9 = z as Element of A() by A7,A8,A9;
assume that
A10: [x,y] in R and
A11: [y,z] in R;
A12: P[y9,z9] by A5,A11;
P[x9,y9] by A5,A10;
then P[x9,z9] by A3,A12;
hence thesis by A5;
end;
A() c= dom R
proof
let x be object;
assume x in A();
then reconsider x9 = x as Element of A();
P[x9,x9] by A1;
then [x,x] in R by A5;
hence thesis by XTUPLE_0:def 12;
end;
then dom R = A();
then
A13: A() c= field R by XBOOLE_1:7;
field R = dom R \/ rng R;
then
A14: field R = A() by A13;
A15: R is_reflexive_in A()
by A1,A5;
A16: A() has_lower_Zorn_property_wrt R
proof
let Y such that
A17: Y c= A() and
A18: R|_2 Y is being_linear-order;
for x,y being Element of A() st x in Y & y in Y holds P[x,y] or P[y,x ]
proof
let x,y be Element of A() such that
A19: x in Y and
A20: y in Y;
A21: R|_2 Y is reflexive connected by A18;
Y c= field(R|_2 Y)
proof
let x be object;
assume
A22: x in Y;
then
A23: [x,x] in [:Y,Y:] by ZFMISC_1:87;
[x,x] in R by A15,A17,A22;
then [x,x] in R|_2 Y by A23,XBOOLE_0:def 4;
hence thesis by RELAT_1:15;
end;
then
A24: Y = field(R|_2 Y|_2 Y) by A21,Lm7
.= field(R|_2 Y) by WELLORD1:21;
then
A25: R|_2 Y is_connected_in Y by A21;
A26: R|_2 Y is_reflexive_in Y by A21,A24;
x = y or x <> y;
then [x,y] in R|_2 Y or [y,x] in R|_2 Y by A19,A20,A25,A26;
then [x,y] in R or [y,x] in R by XBOOLE_0:def 4;
hence thesis by A5;
end;
then consider y being Element of A() such that
A27: for x being Element of A() st x in Y holds P[y,x] by A4,A17;
take y;
thus y in A();
let x;
assume
A28: x in Y;
then P[y,x] by A17,A27;
hence thesis by A5,A17,A28;
end;
R is_antisymmetric_in A()
proof
let x,y be object;
assume that
A29: x in A() and
A30: y in A();
reconsider x9 = x, y9 = y as Element of A() by A29,A30;
assume that
A31: [x,y] in R and
A32: [y,x] in R;
A33: P[y9,x9] by A5,A32;
P[x9,y9] by A5,A31;
hence thesis by A2,A33;
end;
then R partially_orders A() by A15,A6;
then consider x such that
A34: x is_minimal_in R by A14,A16,Th64;
take x;
thus x is Element of A() by A14,A34;
let y being Element of A();
assume x <> y;
then
A35: not [y,x] in R by A14,A34;
x in A() by A14,A34;
hence thesis by A5,A35;
end;
::
:: Orders - continuation.
::
theorem
R partially_orders X & field R = X implies ex P st R c= P & P
linearly_orders X & field P = X
proof
assume that
A1: R partially_orders X and
A2: field R = X;
defpred P[object] means
ex P st $1 = P & R c= P & P partially_orders X & field P = X;
consider Rel being set such that
A3: for x being object holds x in Rel iff x in bool [:X,X:] & P[x]
from XBOOLE_0:sch 1;
A4: for Z st Z <> {} & Z c= Rel & Z is c=-linear holds union Z in Rel
proof
reconsider T = [:X,X:] as Relation;
let Z;
assume that
A5: Z <> {} and
A6: Z c= Rel and
A7: Z is c=-linear;
A8: union bool [:X,X:] = T by ZFMISC_1:81;
Z c= bool [:X,X:]
by A3,A6;
then
A9: union Z c= union bool [:X,X:] by ZFMISC_1:77;
then reconsider S = union Z as Relation;
set y = the Element of Z;
y in Rel by A5,A6;
then consider P such that
A10: y = P and
A11: R c= P and
A12: P partially_orders X and
field P = X by A3;
A13: S is_antisymmetric_in X
proof
let x,y be object;
assume that
A14: x in X and
A15: y in X and
A16: [x,y] in S and
A17: [y,x] in S;
consider X1 such that
A18: [x,y] in X1 and
A19: X1 in Z by A16,TARSKI:def 4;
consider P1 being Relation such that
A20: X1 = P1 and
R c= P1 and
A21: P1 partially_orders X and
field P1 = X by A3,A6,A19;
consider X2 such that
A22: [y,x] in X2 and
A23: X2 in Z by A17,TARSKI:def 4;
X1,X2 are_c=-comparable by A7,A19,A23;
then
A24: X1 c= X2 or X2 c= X1;
consider P2 being Relation such that
A25: X2 = P2 and
R c= P2 and
A26: P2 partially_orders X and
field P2 = X by A3,A6,A23;
A27: P2 is_antisymmetric_in X by A26;
P1 is_antisymmetric_in X by A21;
hence thesis by A14,A15,A18,A22,A24,A20,A25,A27;
end;
A28: S is_transitive_in X
proof
let x,y,z be object;
assume that
A29: x in X and
A30: y in X and
A31: z in X and
A32: [x,y] in S and
A33: [y,z] in S;
consider X1 such that
A34: [x,y] in X1 and
A35: X1 in Z by A32,TARSKI:def 4;
consider P1 being Relation such that
A36: X1 = P1 and
R c= P1 and
A37: P1 partially_orders X and
field P1 = X by A3,A6,A35;
consider X2 such that
A38: [y,z] in X2 and
A39: X2 in Z by A33,TARSKI:def 4;
X1,X2 are_c=-comparable by A7,A35,A39;
then
A40: X1 c= X2 or X2 c= X1;
consider P2 being Relation such that
A41: X2 = P2 and
R c= P2 and
A42: P2 partially_orders X and
field P2 = X by A3,A6,A39;
A43: P2 is_transitive_in X by A42;
P1 is_transitive_in X by A37;
then [x,z] in P1 or [x,z] in P2 by A29,A30,A31,A34,A38,A40,A36,A41,A43;
hence thesis by A35,A39,A36,A41,TARSKI:def 4;
end;
A44: P is_reflexive_in X by A12;
S is_reflexive_in X
proof
let x be object;
assume x in X;
then [x,x] in P by A44;
hence thesis by A5,A10,TARSKI:def 4;
end;
then
A45: S partially_orders X by A28,A13;
A46: field S c= X
proof
let x be object;
A47: now
assume x in dom S;
then consider y being object such that
A48: [x,y] in S by XTUPLE_0:def 12;
consider Y such that
A49: [x,y] in Y and
A50: Y in Z by A48,TARSKI:def 4;
ex P st Y = P & R c= P & P partially_orders X & field P = X by A3,A6
,A50;
hence thesis by A49,RELAT_1:15;
end;
A51: now
assume x in rng S;
then consider y being object such that
A52: [y,x] in S by XTUPLE_0:def 13;
consider Y such that
A53: [y,x] in Y and
A54: Y in Z by A52,TARSKI:def 4;
ex P st Y = P & R c= P & P partially_orders X & field P = X by A3,A6
,A54;
hence thesis by A53,RELAT_1:15;
end;
assume x in field S;
hence thesis by A47,A51,XBOOLE_0:def 3;
end;
A55: R c= S
by A5,A10,A11,TARSKI:def 4;
then X c= field S by A2,RELAT_1:16;
then field S = X by A46;
hence thesis by A3,A9,A8,A55,A45;
end;
R c= [:X,X:] by A2,Lm6;
then Rel <> {} by A1,A2,A3;
then consider Y such that
A56: Y in Rel and
A57: for Z st Z in Rel & Z <> Y holds not Y c= Z by A4,Th67;
consider P such that
A58: Y = P and
A59: R c= P and
A60: P partially_orders X and
A61: field P = X by A3,A56;
take P;
thus R c= P by A59;
thus
A62: P is_reflexive_in X & P is_transitive_in X & P is_antisymmetric_in
X by A60;
thus P is_connected_in X
proof
let x,y be object such that
A63: x in X and
A64: y in X and
x <> y and
A65: not [x,y] in P and
A66: not [y,x] in P;
defpred Q[object,object] means [$1,$2] in P or [$1,x] in P & [y,$2] in P;
consider Q being Relation such that
A67: for z,u being object holds [z,u] in Q iff z in X & u in X & Q[z,u]
from RELAT_1:sch 1;
A68: field Q c= X
proof
let z be object;
A69: now
assume z in dom Q;
then ex u being object st [z,u] in Q by XTUPLE_0:def 12;
hence thesis by A67;
end;
A70: now
assume z in rng Q;
then ex u being object st [u,z] in Q by XTUPLE_0:def 13;
hence thesis by A67;
end;
assume z in field Q;
hence thesis by A69,A70,XBOOLE_0:def 3;
end;
A71: P c= Q
proof
let z,u be object;
assume
A72: [z,u] in P;
then
A73: u in field P by RELAT_1:15;
z in field P by A72,RELAT_1:15;
hence thesis by A61,A67,A72,A73;
end;
then X c= field Q by A61,RELAT_1:16;
then
A74: field Q = X by A68;
A75: Q is_transitive_in X
proof
let a,b,c be object;
assume that
A76: a in X and
A77: b in X and
A78: c in X and
A79: [a,b] in Q and
A80: [b,c] in Q;
A81: [b,c] in P or [b,x] in P & [y,c] in P by A67,A80;
[a,b] in P or [a,x] in P & [y,b] in P by A67,A79;
then [a,c] in P or [a,x] in P & [y,c] in P or [a,x] in P & [y,c] in P
or [y,x] in P by A62,A63,A64,A76,A77,A78,A81;
hence thesis by A66,A67,A76,A78;
end;
A82: Q is_antisymmetric_in X
proof
let a,b be object;
assume that
A83: a in X and
A84: b in X and
A85: [a,b] in Q and
A86: [b,a] in Q;
A87: [b,a] in P or [b,x] in P & [y,a] in P by A67,A86;
[a,b] in P or [a,x] in P & [y,b] in P by A67,A85;
then a = b or [a,x] in P & [y,a] in P or [y,x] in P by A62,A63,A64,A83
,A84,A87;
hence thesis by A62,A63,A64,A66,A83;
end;
Q is_reflexive_in X
by A62,A67;
then
A88: Q partially_orders X by A75,A82;
A89: Q c= [:X,X:]
proof
let y,z be object;
assume
A90: [y,z] in Q;
then
A91: z in X by A67;
y in X by A67,A90;
hence thesis by A91,ZFMISC_1:87;
end;
R c= Q by A59,A71;
then Q in Rel by A3,A89,A74,A88;
then
A92: Q = P by A57,A58,A71;
A93: [y,y] in P by A62,A64;
[x,x] in P by A62,A63;
hence contradiction by A63,A64,A65,A67,A92,A93;
end;
thus thesis by A61;
end;
::
:: Auxiliary theorems.
::
theorem
R c= [:field R,field R:] by Lm6;
theorem
R is reflexive & X c= field R implies field(R|_2 X) = X by Lm7;
theorem
R is_reflexive_in X implies R|_2 X is reflexive by Lm8;
theorem
R is_transitive_in X implies R|_2 X is transitive by Lm9;
theorem
R is_antisymmetric_in X implies R|_2 X is antisymmetric by Lm10;
theorem
R is_connected_in X implies R|_2 X is connected by Lm11;
theorem
R is_connected_in X & Y c= X implies R is_connected_in Y;
theorem
R well_orders X & Y c= X implies R well_orders Y by Lm18;
theorem
R is connected implies R~ is connected by Lm5;
theorem
R is_reflexive_in X implies R~ is_reflexive_in X by Lm12;
theorem
R is_transitive_in X implies R~ is_transitive_in X by Lm13;
theorem
R is_antisymmetric_in X implies R~ is_antisymmetric_in X by Lm14;
theorem
R is_connected_in X implies R~ is_connected_in X by Lm15;
theorem
(R|_2 X)~ = R~|_2 X by Lm16;
theorem
R|_2 {} = {} by Lm17;
begin :: Addenda
:: from COMPTS_1
theorem
Z is finite & Z c= rng f implies ex Y st Y c= dom f & Y is finite & f .:Y = Z
proof
assume that
A1: Z is finite and
A2: Z c= rng f;
per cases;
suppose
A3: Z = {};
take Y = {};
thus Y c= dom f & Y is finite;
thus thesis by A3;
end;
suppose
A4: Z <> {};
deffunc F(object) = f"{$1};
consider g being Function such that
A5: dom g = Z and
A6: for x being object st x in Z holds g.x = F(x) from FUNCT_1:sch 3;
reconsider AA = rng g as non empty set by A4,A5,RELAT_1:42;
set ff = the Choice_Function of AA;
take Y = ff.:AA;
A7: for X being set st X in AA holds X <> {}
proof
let X be set;
assume X in AA;
then consider x being object such that
A8: x in dom g and
A9: g.x=X by FUNCT_1:def 3;
g.x = f"{x} by A5,A6,A8;
hence thesis by A2,A5,A8,A9,FUNCT_1:72;
end;
then
A10: not {} in AA;
thus
A11: Y c= dom f
proof
let x be object;
assume x in Y;
then consider y being object such that
y in dom ff and
A12: y in AA and
A13: ff.y=x by FUNCT_1:def 6;
y in g.:Z by A5,A12,RELAT_1:113;
then consider z being object such that
z in dom g and
A14: z in Z and
A15: g.z=y by FUNCT_1:def 6;
A16: g.z = f"{z} by A6,A14;
x in g.z by A10,A12,A13,A15,Lm2;
hence thesis by A16,FUNCT_1:def 7;
end;
AA = g.:Z by A5,RELAT_1:113;
hence Y is finite by A1;
set z = the Element of AA;
set y = the Element of z;
z <> {} by A7;
then y in z;
then reconsider AA9=union AA as non empty set by TARSKI:def 4;
reconsider f9= ff as Function of AA,AA9 by A10,Lm3;
A17: dom f9 = AA by FUNCT_2:def 1;
for x being object holds x in f.:Y iff x in Z
proof let x be object;
thus x in f.:Y implies x in Z
proof
assume x in f.:(Y);
then consider y being object such that
y in dom f and
A18: y in Y and
A19: f.y = x by FUNCT_1:def 6;
consider z being object such that
A20: z in dom ff and
z in AA and
A21: ff.z=y by A18,FUNCT_1:def 6;
consider a being object such that
A22: a in dom g and
A23: g.a=z by A20,FUNCT_1:def 3;
g.a = f"{a} by A5,A6,A22;
then y in f"{a} by A10,A20,A21,A23,Lm2;
then f.y in {a} by FUNCT_1:def 7;
hence thesis by A5,A19,A22,TARSKI:def 1;
end;
set y=ff.(g.x);
assume
A24: x in Z;
then
A25: g.x in AA by A5,FUNCT_1:def 3;
g.x = f"{x} by A6,A24;
then y in f"{x} by A10,A25,Lm2;
then f.y in {x} by FUNCT_1:def 7;
then
A26: f.y = x by TARSKI:def 1;
ff.(g.x) in rng ff by A17,A25,FUNCT_1:def 3;
then y in Y by A17,RELAT_1:113;
hence thesis by A11,A26,FUNCT_1:def 6;
end;
hence thesis by TARSKI:2;
end;
end;
:: from AMISTD_3, 2006.03.26, A.T.
theorem Th86:
field R is finite implies R is finite
proof
assume field R is finite;
then reconsider A = field R as finite set;
R c= [:A,A:] by Lm6;
hence thesis;
end;
theorem
dom R is finite & rng R is finite implies R is finite
proof
assume that
A1: dom R is finite and
A2: rng R is finite;
field R is finite by A1,A2;
hence thesis by Th86;
end;
:: from AMISTD_3, 2010.01.10, A.T
registration
cluster order_type_of {} -> empty;
coherence
proof
{},RelIncl {} are_isomorphic by WELLORD1:38;
hence thesis by WELLORD2:def 2;
end;
end;
theorem
for O being Ordinal holds order_type_of RelIncl O = O proof let O be Ordinal;
RelIncl O is well-ordering & RelIncl O,RelIncl O are_isomorphic
by WELLORD1:38;
hence thesis by WELLORD2:def 2;
end;
definition
let X be set;
redefine func RelIncl X -> Order of X; :: redefines RelIncl (WELLORD2, definition)
coherence
proof
now
let x be object;
assume
A1: x in RelIncl X;
then consider y,z be object such that
A2: x = [y,z] by RELAT_1:def 1;
z in field RelIncl X by A1,A2,RELAT_1:15;
then
A3: z in X by WELLORD2:def 1;
y in field RelIncl X by A1,A2,RELAT_1:15;
then y in X by WELLORD2:def 1;
hence x in [:X,X:] by A2,A3,ZFMISC_1:87;
end;
then reconsider R = RelIncl X as Relation of X by TARSKI:def 3;
field R = X & R is reflexive by WELLORD2:def 1;
then R is_reflexive_in X;
then dom R = X by Th13;
hence thesis by PARTFUN1:def 2;
end;
end;
theorem
not {} in M implies
for Ch being Choice_Function of M
for X st X in M holds Ch.X in X by Lm2;
theorem
not {} in M implies
for Ch being Choice_Function of M
holds Ch is Function of M, union M by Lm3;