Copyright (c) 1989 Association of Mizar Users
environ
vocabulary RELAT_1, FUNCT_1, ORDERS_1, ORDINAL1, BOOLE, RELAT_2, WELLORD1,
TARSKI, ZFMISC_1, WELLORD2, SETFAM_1, ORDERS_2, HAHNBAN, PARTFUN1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELAT_2,
RELSET_1, PARTFUN1, WELLORD1, SETFAM_1, STRUCT_0, ORDERS_1, ORDINAL1,
WELLORD2;
constructors RELAT_2, WELLORD1, ORDERS_1, WELLORD2, PARTFUN1, XBOOLE_0;
clusters ORDERS_1, ORDINAL1, RELSET_1, STRUCT_0, SUBSET_1, ZFMISC_1, XBOOLE_0;
requirements BOOLE, SUBSET;
definitions RELAT_2, TARSKI, WELLORD1, RELAT_1, ORDERS_1, ORDINAL1, XBOOLE_0;
theorems ORDERS_1, RELAT_1, RELAT_2, RELSET_1, TARSKI, WELLORD1, ZFMISC_1,
FUNCT_1, ORDINAL1, WELLORD2, SETFAM_1, XBOOLE_0, XBOOLE_1, PARTFUN1;
schemes RELSET_1, TARSKI, RELAT_1, FUNCT_1, ORDINAL1, XBOOLE_0;
begin
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,
A for non empty Poset,
C for Chain of A,
S for Subset of A,
a,a1,a2,a3,a4,b,c1,c2 for Element of A,
A1,A2,B for Ordinal,
L,L1,L2 for T-Sequence;
::
:: Orders.
::
theorem Th1:
dom O = X & rng O = X
proof
thus dom O = X
proof
thus dom O c= X;
let x;
assume x in X;
then [x,x] in O by ORDERS_1:12;
hence thesis by RELAT_1:def 4;
end;
thus rng O c= X;
let x;
assume x in X;
then [x,x] in O by ORDERS_1:12;
hence thesis by RELAT_1:def 5;
end;
theorem Th2:
field O = X
proof
thus X = X \/ X
.= dom O \/ X by Th1
.= dom O \/ rng O by Th1
.= field O by RELAT_1:def 6;
end;
definition let R;
attr R is being_quasi-order means
R is reflexive transitive;
synonym R is_quasi-order;
attr R is being_partial-order means
:Def2: R is reflexive transitive antisymmetric;
synonym R is_partial-order;
attr R is being_linear-order means
:Def3: R is reflexive transitive antisymmetric connected;
synonym R is_linear-order;
end;
canceled 3;
theorem
R is_quasi-order implies R~ is_quasi-order
proof assume
R is reflexive & R is transitive;
hence R~ is reflexive & R~ is transitive by RELAT_2:27,42;
end;
theorem
R is_partial-order implies R~ is_partial-order
proof assume
R is reflexive & R is transitive & R is antisymmetric;
hence R~ is reflexive & R~ is transitive & R~ is antisymmetric
by RELAT_2:27,40,42;
end;
Lm1: R is connected implies R~ is connected
proof assume
A1: x in field R & y in field R & x <> y implies [x,y] in R or [y,x] in R;
A2: field R = field(R~) by RELAT_1:38;
let x,y; assume x in field(R~) & y in field(R~) & x <> y;
then [x,y] in R or [y,x] in R by A1,A2;
hence thesis by RELAT_1:def 7;
end;
theorem Th8:
R is_linear-order implies R~ is_linear-order
proof assume
R is reflexive & R is transitive & R is antisymmetric & R is connected;
hence R~ is reflexive & R~ is transitive & R~ is antisymmetric &
R~ is connected by Lm1,RELAT_2:27,40,42;
end;
theorem
R is well-ordering implies
R is_quasi-order & R is_partial-order & R is_linear-order
proof assume R is reflexive & R is transitive & R is antisymmetric &
R is connected & R is well_founded;
hence R is reflexive & R is transitive &
R is reflexive & R is transitive & R is antisymmetric &
R is reflexive & R is transitive & R is antisymmetric & R is connected;
end;
theorem
R is_linear-order implies R is_quasi-order & R is_partial-order
proof assume R is reflexive & R is transitive & R is antisymmetric &
R is connected;
hence R is reflexive & R is transitive &
R is reflexive & R is transitive & R is antisymmetric;
end;
theorem Th11:
R is_partial-order implies R is_quasi-order
proof assume R is reflexive & R is transitive & R is antisymmetric;
hence R is reflexive & R is transitive;
end;
theorem Th12:
O is_partial-order by Def2;
theorem
O is_quasi-order
proof O is_partial-order by Th12;
hence thesis by Th11;
end;
theorem
O is connected implies O is_linear-order by Def3;
Lm2: R c= [:field R,field R:]
proof let x; assume
A1: x in R;
then consider y,z such that
A2: x = [y,z] by RELAT_1:def 1;
y in field R & z in field R by A1,A2,RELAT_1:30;
hence thesis by A2,ZFMISC_1:106;
end;
Lm3: R is reflexive & X c= field R implies field(R|_2 X) = X
proof assume that
A1: x in field R implies [x,x] in R and
A2: X c= field R;
thus field(R|_2 X) c= X proof let y; thus thesis by WELLORD1:19; end;
let y; assume
y in X;
then [y,y] in R & [y,y] in [:X,X:] by A1,A2,ZFMISC_1:106;
then [y,y] in R|_2 X by WELLORD1:16;
hence thesis by RELAT_1:30;
end;
theorem
R is_quasi-order implies R|_2 X is_quasi-order
proof assume
R is reflexive & R is transitive;
hence R|_2 X is reflexive & R|_2 X is transitive by WELLORD1:22,24;
end;
theorem
Th16: R is_partial-order implies R|_2 X is_partial-order
proof assume R is reflexive & R is transitive & R is antisymmetric;
hence R|_2 X is reflexive & R|_2 X is transitive &
R|_2 X is antisymmetric by WELLORD1:22,24,25;
end;
theorem
R is_linear-order implies R|_2 X is_linear-order
proof assume
R is reflexive & R is transitive & R is antisymmetric & R is connected;
hence R|_2 X is reflexive & R|_2 X is transitive & R|_2 X is antisymmetric
&
R|_2 X is connected by WELLORD1:22,23,24,25;
end;
theorem Th18:
field((the InternalRel of A) |_2 S) = S
proof set P = (the InternalRel of A) |_2 S;
thus field P c= S by WELLORD1:20;
thus S c= field P
proof let x;
assume A1: x in S;
S c= the carrier of A &
the InternalRel of A is_reflexive_in the carrier of A
by ORDERS_1:def 4;
then [x,x] in the InternalRel of A & [x,x] in [:S,S:]
by A1,RELAT_2:def 1,ZFMISC_1:106;
then [x,x] in P by WELLORD1:16;
then x in dom P & x in rng P by RELAT_1:def 4,def 5;
then x in dom P \/ rng P by XBOOLE_0:def 2;
hence thesis by RELAT_1:def 6;
end;
end;
theorem
(the InternalRel of A) |_2 S is_linear-order implies
S is Chain of A
proof assume (the InternalRel of A) |_2 S is_linear-order;
then (the InternalRel of A) |_2 S is connected &
field((the InternalRel of A) |_2 S) = S by Def3,Th18;
then A1: (the InternalRel of A) |_2 S is_connected_in S by RELAT_2:def 14;
S is strongly_connected
proof let x,y;
assume A2: x in S & y in S;
then reconsider a = x, b = y as Element of A;
now per cases;
suppose x = y;
then a <= b;
hence thesis by ORDERS_1:def 9;
suppose x <> y;
then [x,y] in (the InternalRel of A) |_2 S or
[y,x] in (the InternalRel of A) |_2 S by A1,A2,RELAT_2:def 6;
hence thesis by WELLORD1:16;
end;
hence thesis;
end;
hence thesis;
end;
theorem
(the InternalRel of A) |_2 C is_linear-order
proof set P = (the InternalRel of A) |_2 C;
the InternalRel of A is_partial-order by Th12;
then P is_partial-order by Th16;
hence P is reflexive & P is transitive & P is antisymmetric by Def2;
A1: C = field P by Th18;
P is_connected_in C
proof let x,y;
assume that A2: x in C & y in C;
the InternalRel of A is_strongly_connected_in C by ORDERS_1:def 11;
then A3: [x,y] in the InternalRel of A or [y,x] in the InternalRel of A
by A2,RELAT_2:
def 7;
[x,y] in [:C,C:] & [y,x] in [:C,C:] by A2,ZFMISC_1:106;
hence thesis by A3,WELLORD1:16;
end;
hence thesis by A1,RELAT_2:def 14;
end;
theorem Th21:
{} is_quasi-order &
{} is_partial-order &
{} is_linear-order &
{} is well-ordering
proof
A1: field {} = {} \/ {} by RELAT_1:60,def 6
.= {};
thus
A2: {} is reflexive
proof let x; assume x in field {};
hence thesis by A1;
end;
thus
A3: {} is transitive
proof let x,y,z such that x in field {};
thus thesis;
end;
hence {} is reflexive & {} is transitive by A2;
thus
A4: {} is antisymmetric
proof let x,y such that x in field {};
thus thesis;
end;
hence {} is reflexive & {} is transitive & {} is antisymmetric
by A2,A3;
thus {} is connected
proof let x,y such that x in field {};
thus thesis by A1;
end;
hence {} is reflexive & {} is transitive & {} is antisymmetric &
{} is connected by A2,A3,A4;
let Y; assume
Y c= field {} & Y <> {};
hence thesis by A1,XBOOLE_1:3;
end;
theorem
Th22: id X is_quasi-order &
id X is_partial-order
proof
thus id X is reflexive & id X is transitive &
id X is reflexive & id X is transitive &
id X is antisymmetric by RELAT_2:23,24;
end;
definition let R,X;
pred R quasi_orders X means
:Def4: R is_reflexive_in X & R is_transitive_in X;
pred R partially_orders X means
:Def5: R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X;
pred R linearly_orders X means
:Def6: R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X &
R is_connected_in X;
end;
canceled 3;
theorem Th26:
R well_orders X implies
R quasi_orders X & R partially_orders X & R linearly_orders X
proof assume R is_reflexive_in X & R is_transitive_in X &
R is_antisymmetric_in X & R is_connected_in X & R is_well_founded_in X;
hence R is_reflexive_in X & R is_transitive_in X &
R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X &
R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X &
R is_connected_in X;
end;
theorem Th27:
R linearly_orders X implies R quasi_orders X & R partially_orders X
proof assume R is_reflexive_in X & R is_transitive_in X &
R is_antisymmetric_in X & R is_connected_in X;
hence R is_reflexive_in X & R is_transitive_in X &
R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X;
end;
theorem
R partially_orders X implies R quasi_orders X
proof assume R is_reflexive_in X & R is_transitive_in X &
R is_antisymmetric_in X;
hence R is_reflexive_in X & R is_transitive_in X;
end;
theorem
Th29: R is_quasi-order implies R quasi_orders field R
proof assume R is_reflexive_in field R & R is_transitive_in field R;
hence R is_reflexive_in field R & R is_transitive_in field R;
end;
theorem
R quasi_orders Y & X c= Y implies R quasi_orders X
proof assume
R is_reflexive_in Y & R is_transitive_in Y & X c= Y;
hence R is_reflexive_in X & R is_transitive_in X
by ORDERS_1:93,95;
end;
Lm4: R is_reflexive_in X implies R|_2 X is reflexive
proof assume
A1: x in X implies [x,x] in R;
let x; assume x in field(R|_2 X);
then x in X by WELLORD1:19;
then [x,x] in R & [x,x] in [:X,X:] by A1,ZFMISC_1:106;
hence thesis by WELLORD1:16;
end;
Lm5: R is_transitive_in X implies R|_2 X is transitive
proof assume
A1: 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; assume x in field(R|_2 X) & y in field(R|_2 X) & z in
field(R|_2 X);
then A2: x in X & y in X & z in X by WELLORD1:19;
assume [x,y] in R|_2 X & [y,z] in R|_2 X;
then [x,y] in R & [y,z] in R by WELLORD1:16;
then [x,z] in R & [x,z] in [:X,X:] by A1,A2,ZFMISC_1:106;
hence thesis by WELLORD1:16;
end;
Lm6: R is_antisymmetric_in X implies R|_2 X is antisymmetric
proof assume
A1: x in X & y in X & [x,y] in R & [y,x] in R implies x = y;
let x,y; assume x in field(R|_2 X) & y in field(R|_2 X);
then A2: x in X & y in X by WELLORD1:19;
assume [x,y] in R|_2 X & [y,x] in R|_2 X;
then [x,y] in R & [y,x] in R by WELLORD1:16;
hence thesis by A1,A2;
end;
Lm7: R is_connected_in X implies R|_2 X is connected
proof assume
A1: x in X & y in X & x <> y implies [x,y] in R or [y,x] in R;
let x,y; assume x in field(R|_2 X) & y in field(R|_2 X) & x <> y;
then x in X & y in X & x <> y by WELLORD1:19;
then ([x,y] in R or [y,x] in R) & [x,y] in [:X,X:] & [y,x] in [:X,X:]
by A1,ZFMISC_1:106;
hence thesis by WELLORD1:16;
end;
theorem
R quasi_orders X implies R|_2 X is_quasi-order
proof assume R is_reflexive_in X & R is_transitive_in X;
hence R|_2 X is reflexive & R|_2 X is transitive by Lm4,Lm5;
end;
theorem
Th32: R is_partial-order implies R partially_orders field R
proof assume R is_reflexive_in field R & R is_transitive_in field R &
R is_antisymmetric_in field R;
hence R is_reflexive_in field R & R is_transitive_in field R &
R is_antisymmetric_in field R;
end;
theorem
R partially_orders Y & X c= Y implies R partially_orders X
proof assume
R is_reflexive_in Y & R is_transitive_in Y & R is_antisymmetric_in Y &
X c= Y;
hence R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X
by ORDERS_1:93,94,95;
end;
theorem
R partially_orders X implies R|_2 X is_partial-order
proof assume R is_reflexive_in X & R is_transitive_in X &
R is_antisymmetric_in X;
hence R|_2 X is reflexive & R|_2 X is transitive & R|_2 X is antisymmetric
by Lm4,Lm5,Lm6;
end;
Lm8: R is_connected_in X & Y c= X implies R is_connected_in Y
proof assume that A1: R is_connected_in X and A2: Y c= X;
let x,y;
assume x in Y & y in Y;
hence thesis by A1,A2,RELAT_2:def 6;
end;
theorem
R is_linear-order implies R linearly_orders field R
proof assume R is_reflexive_in field R & R is_transitive_in field R &
R is_antisymmetric_in field R & R is_connected_in field R;
hence R is_reflexive_in field R & R is_transitive_in field R &
R is_antisymmetric_in field R & R is_connected_in field R;
end;
theorem
R linearly_orders Y & X c= Y implies R linearly_orders X
proof assume
R is_reflexive_in Y & R is_transitive_in Y & R is_antisymmetric_in Y &
R is_connected_in Y & X c= Y;
hence R is_reflexive_in X & R is_transitive_in X &
R is_antisymmetric_in X & R is_connected_in X
by Lm8,ORDERS_1:93,94,95;
end;
theorem
R linearly_orders X implies R|_2 X is_linear-order
proof assume R is_reflexive_in X & R is_transitive_in X &
R is_antisymmetric_in X & R is_connected_in X;
hence R|_2 X is reflexive & R|_2 X is transitive & R|_2 X is antisymmetric
&
R|_2 X is connected by Lm4,Lm5,Lm6,Lm7;
end;
Lm9: R is_reflexive_in X implies R~ is_reflexive_in X
proof assume
A1: x in X implies [x,x] in R;
let x; assume x in X;
then [x,x] in R by A1;
hence thesis by RELAT_1:def 7;
end;
Lm10: R is_transitive_in X implies R~ is_transitive_in X
proof assume
A1: 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; assume
A2: x in X & y in X & z in X & [x,y] in R~ & [y,z] in R~;
then [y,x] in R & [z,y] in R by RELAT_1:def 7;
then [z,x] in R by A1,A2;
hence thesis by RELAT_1:def 7;
end;
Lm11: R is_antisymmetric_in X implies R~ is_antisymmetric_in X
proof assume
A1: x in X & y in X & [x,y] in R & [y,x] in R implies x = y;
let x,y; assume
A2: x in X & y in X & [x,y] in R~ & [y,x] in R~;
then [x,y] in R & [y,x] in R by RELAT_1:def 7;
hence thesis by A1,A2;
end;
Lm12: R is_connected_in X implies R~ is_connected_in X
proof assume
A1: x in X & y in X & x <> y implies [x,y] in R or [y,x] in R;
let x,y; assume x in X & y in X & x <> y;
then [x,y] in R or [y,x] in R by A1;
hence thesis by RELAT_1:def 7;
end;
theorem
R quasi_orders X implies R~ quasi_orders X
proof assume R is_reflexive_in X & R is_transitive_in X;
hence R~ is_reflexive_in X & R~ is_transitive_in X by Lm9,Lm10;
end;
theorem Th39:
R partially_orders X implies R~ partially_orders X
proof assume R is_reflexive_in X & R is_transitive_in X &
R is_antisymmetric_in X;
hence R~ is_reflexive_in X & R~ is_transitive_in X &
R~ is_antisymmetric_in X by Lm9,Lm10,Lm11;
end;
theorem
R linearly_orders X implies R~ linearly_orders X
proof assume R is_reflexive_in X & R is_transitive_in X &
R is_antisymmetric_in X & R is_connected_in X;
hence R~ is_reflexive_in X & R~ is_transitive_in X &
R~ is_antisymmetric_in X & R~ is_connected_in X
by Lm9,Lm10,Lm11,Lm12;
end;
theorem
O quasi_orders X
proof field O = X by ORDERS_1:97;
then O is_reflexive_in X & O is_transitive_in X by RELAT_2:def 9,def 16;
hence thesis by Def4;
end;
theorem
O partially_orders X
proof field O = X by ORDERS_1:97;
then O is_reflexive_in X & O is_antisymmetric_in X & O is_transitive_in X
by RELAT_2:def 9,def 12,def 16;
hence thesis by Def5;
end;
theorem Th43:
R partially_orders X implies R |_2 X is Order of X
proof assume A1: R partially_orders X;
then
A2: R is_reflexive_in X by Def5;
set S = R |_2 X;
A3: R |_2 X is_reflexive_in X
proof let x;
assume x in X;
then [x,x] in [:X,X:] & [x,x] in R by A2,RELAT_2:def 1,ZFMISC_1:106;
hence [x,x] in R |_2 X by WELLORD1:16;
end;
A4: field S c= X by WELLORD1:20;
field S = dom S \/ rng S by RELAT_1:def 6;
then dom S c= field S & rng S c= field S by XBOOLE_1:7;
then
dom S c= X & rng S c= X by A4,XBOOLE_1:1;
then reconsider S as Relation of X by RELSET_1:11;
A5: dom S = X by A3,ORDERS_1:98;
A6: field S = X by A3,ORDERS_1:98;
A7: R |_2 X is_antisymmetric_in X
proof let x,y;
assume that A8: x in X & y in X and A9: [x,y] in R |_2 X & [y,x] in
R |_2 X;
[x,y] in R & [y,x] in R & R is_antisymmetric_in X
by A1,A9,Def5,WELLORD1:16;
hence thesis by A8,RELAT_2:def 4;
end;
A10: R |_2 X is_transitive_in X
proof let x,y,z;
assume that A11: x in X & y in X & z in X and
A12: [x,y] in R |_2 X & [y,z] in R |_2 X;
[x,y] in R & [y,z] in R & R is_transitive_in X
by A1,A12,Def5,WELLORD1:16;
then [x,z] in R & [x,z] in [:X,X:] by A11,RELAT_2:def 8,ZFMISC_1:106;
hence thesis by WELLORD1:16;
end;
A13: S is total by A5,PARTFUN1:def 4;
A14: S is reflexive by A3,A6,RELAT_2:def 9;
A15: S is antisymmetric by A6,A7,RELAT_2:def 12;
S is transitive by A6,A10,RELAT_2:def 16;
hence thesis by A13,A14,A15;
end;
theorem
R linearly_orders X implies R |_2 X is Order of X
proof assume R linearly_orders X;
then R partially_orders X by Th27;
hence thesis by Th43;
end;
theorem
R well_orders X implies R |_2 X is Order of X
proof assume R well_orders X;
then R partially_orders X by Th26;
hence thesis by Th43;
end;
theorem
the InternalRel of A linearly_orders S implies
S is Chain of A
proof assume the InternalRel of A linearly_orders S;
then the InternalRel of A is_reflexive_in S &
the InternalRel of A is_connected_in S by Def6;
then the InternalRel of A is_strongly_connected_in S by ORDERS_1:92;
hence thesis by ORDERS_1:def 11;
end;
theorem
the InternalRel of A linearly_orders C
proof the InternalRel of A is_reflexive_in the carrier of A &
the InternalRel of A is_transitive_in the carrier of A &
the InternalRel of A is_antisymmetric_in the carrier of A &
C c= the carrier of A by ORDERS_1:def 4,def 5,def 6;
hence the InternalRel of A is_reflexive_in C &
the InternalRel of A is_transitive_in C &
the InternalRel of A is_antisymmetric_in C
by ORDERS_1:93,94,95;
the InternalRel of A is_strongly_connected_in C by ORDERS_1:def 11;
hence thesis by ORDERS_1:92;
end;
theorem
id X quasi_orders X &
id X partially_orders X
proof
A1: field id X = dom id X \/ rng id X by RELAT_1:def 6
.= X \/ rng id X by RELAT_1:71
.= X \/ X by RELAT_1:71 .= X;
id X is_quasi-order & id X is_partial-order by Th22;
hence thesis by A1,Th29,Th32;
end;
definition let R,X;
pred X has_upper_Zorn_property_wrt R means
:Def7: for Y st Y c= X & R|_2 Y is_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_linear-order
ex x st x in X & for y st y in Y holds [x,y] in R;
end;
Lm13: (R|_2 X)~ = R~|_2 X
proof
now let x,y;
thus [x,y] in R~|_2 X implies [y,x] in R|_2 X
proof assume [x,y] in R~|_2 X;
then [x,y] in R~ & [x,y] in [:X,X:] by WELLORD1:16;
then [y,x] in R & [y,x] in [:X,X:] by RELAT_1:def 7,ZFMISC_1:107;
hence thesis by WELLORD1:16;
end;
assume [y,x] in R|_2 X;
then [y,x] in R & [y,x] in [:X,X:] by WELLORD1:16;
then [x,y] in R~ & [x,y] in [:X,X:] by RELAT_1:def 7,ZFMISC_1:107;
hence [x,y] in R~|_2 X by WELLORD1:16;
end;
hence thesis by RELAT_1:def 7;
end;
Lm14:
now let R;
thus R|_2 {} = {}|R|({} qua set) by WELLORD1:17 .= {} by RELAT_1:110;
end;
canceled 2;
theorem
Th51: X has_upper_Zorn_property_wrt R implies X <> {}
proof assume
A1: for Y st Y c= X & R|_2 Y is_linear-order
ex x st x in X & for y st y in Y holds [y,x] in R;
{} c= X & R|_2 {} is_linear-order by Lm14,Th21,XBOOLE_1:2;
then ex x st x in X & for y st y in {} holds [y,x] in R by A1;
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_linear-order
ex x st x in X & for y st y in Y holds [x,y] in R;
{} c= X & R|_2 {} is_linear-order by Lm14,Th21,XBOOLE_1:2;
then ex x st x in X & for y st y in {} holds [x,y] in R by A1;
hence thesis;
end;
theorem
Th53: 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_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)~ & (R|_2 Y)~~ = R|_2 Y by Lm13;
assume
A3: Y c= X & R~|_2 Y is_linear-order;
then R|_2 Y is_linear-order by A2,Th8;
then consider x such that
A4: x in X & for y st y in Y holds [y,x] in R by A1,A3;
take x; thus x in X by A4;
let y; assume y in Y;
then [y,x] in R by A4;
hence [x,y] in R~ by RELAT_1:def 7;
end;
assume
A5: for Y st Y c= X & R~|_2 Y is_linear-order
ex x st x in X & for y st y in Y holds [x,y] in R~;
let Y;
A6: R~|_2 Y = (R|_2 Y)~ & (R|_2 Y)~~ = R|_2 Y by Lm13;
assume
A7: Y c= X & R|_2 Y is_linear-order;
then R~|_2 Y is_linear-order by A6,Th8;
then consider x such that
A8: x in X & for y st y in Y holds [x,y] in R~ by A5,A7;
take x; thus x in X by A8;
let y; assume y in Y;
then [x,y] in R~ by A8;
hence [y,x] in R 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 Th53;
end;
definition let R,x;
pred x is_maximal_in R means
:Def9: 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
:Def10: 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
:Def11: 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
:Def12: x in field R & for y st y in field R & y <> x holds [x,y] in R;
end;
canceled 4;
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;
thus A3: x in field R by A1,Def12;
let y;
assume that A4: y in field R and A5: y <> x and A6: [y,x] in R;
[x,y] in R & R is_antisymmetric_in field R by A1,A2,A4,A5,Def12,RELAT_2:
def 12;
hence thesis by A3,A4,A5,A6,RELAT_2:def 4;
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;
thus A3: x in field R by A1,Def11;
let y;
assume that A4: y in field R and A5: y <> x and A6: [x,y] in R;
[y,x] in R & R is_antisymmetric_in field R by A1,A2,A4,A5,Def11,RELAT_2:
def 12;
hence thesis by A3,A4,A5,A6,RELAT_2:def 4;
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,Def10;
A4: R is_connected_in field R by A2,RELAT_2:def 14;
let y;
assume that A5: y in field R and A6: y <> x;
[x,y] in R or [y,x] in R by A3,A4,A5,A6,RELAT_2:def 6;
hence thesis by A1,A5,A6,Def10;
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,Def9;
A4: R is_connected_in field R by A2,RELAT_2:def 14;
let y;
assume that A5: y in field R and A6: y <> x;
[x,y] in R or [y,x] in R by A3,A4,A5,A6,RELAT_2:def 6;
hence thesis by A1,A5,A6,Def9;
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
A1: x in X & x is_superior_of R & X c= field R & R is_reflexive_in field R;
let Y such that
A2: Y c= X & R|_2 Y is_linear-order;
take x; thus x in X by A1;
let y; assume y in Y;
then y in X by A2;
then y in field R & (y = x or y <> x) by A1;
hence [y,x] in R by A1,Def11,RELAT_2:def 1;
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
A1: x in X & x is_inferior_of R & X c= field R & R is_reflexive_in field R;
let Y such that
A2: Y c= X & R|_2 Y is_linear-order;
take x; thus x in X by A1;
let y; assume y in Y;
then y in X by A2;
then y in field R & (y = x or y <> x) by A1;
hence [x,y] in R by A1,Def12,RELAT_2:def 1;
end;
theorem
Th65: x is_minimal_in R iff x is_maximal_in R~
proof
A1: field R = field(R~) by RELAT_1:38;
thus x is_minimal_in R implies x is_maximal_in R~
proof assume
A2: x in field R & not ex y st y in field R & y <> x & [y,x] in R;
hence x in field(R~) by RELAT_1:38;
let y; assume y in field(R~) & y <> x;
then not [y,x] in R by A1,A2;
hence not [x,y] in R~ by RELAT_1:def 7;
end;
assume
A3: x in field(R~) & not ex y st y in field(R~) & y <> x & [x,y] in R~;
hence x in field R by RELAT_1:38;
let y; assume y in field R & y <> x;
then not [x,y] in R~ by A1,A3;
hence not [y,x] in R 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:38;
thus x is_minimal_in R~ implies x is_maximal_in R
proof assume
A2: x in field(R~) & not ex y st y in field(R~) & y <> x & [y,x] in R~;
hence x in field R by RELAT_1:38;
let y; assume y in field R & y <> x;
then not [y,x] in R~ by A1,A2;
hence not [x,y] in R by RELAT_1:def 7;
end;
assume
A3: x in field R & not ex y st y in field R & y <> x & [x,y] in R;
hence x in field(R~) by RELAT_1:38;
let y; assume y in field(R~) & y <> x;
then not [x,y] in R by A1,A3;
hence not [y,x] in R~ 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:38;
thus x is_inferior_of R implies x is_superior_of R~
proof assume
A2: x in field R & for y st y in field R & y <> x holds [x,y] in R;
hence x in field(R~) by RELAT_1:38;
let y; assume y in field(R~) & y <> x;
then [x,y] in R by A1,A2;
hence [y,x] in R~ by RELAT_1:def 7;
end;
assume
A3: x in field(R~) & for y st y in field(R~) & y <> x holds [y,x] in R~;
hence x in field R by RELAT_1:38;
let y; assume y in field R & y <> x;
then [y,x] in R~ by A1,A3;
hence [x,y] in R 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:38;
thus x is_inferior_of R~ implies x is_superior_of R
proof assume
A2: x in field(R~) & for y st y in field(R~) & y <> x holds [x,y] in R~;
hence x in field R by RELAT_1:38;
let y; assume y in field R & y <> x;
then [x,y] in R~ by A1,A2;
hence [y,x] in R by RELAT_1:def 7;
end;
assume
A3: x in field R & for y st y in field R & y <> x holds [y,x] in R;
hence x in field(R~) by RELAT_1:38;
let y; assume y in field(R~) & y <> x;
then [y,x] in R by A1,A3;
hence [x,y] in R~ by RELAT_1:def 7;
end;
theorem
a is_minimal_in the InternalRel of A iff
for b holds not b < a
proof A1: the carrier of A = field(the InternalRel of A) by Th2;
thus a is_minimal_in the InternalRel of A implies for b holds not b < a
proof assume A2: a is_minimal_in the InternalRel of A;
let b;
a = b or not [b,a] in the InternalRel of A by A1,A2,Def10;
then a = b or not b <= a by ORDERS_1:def 9;
hence thesis by ORDERS_1:def 10;
end;
assume A3: for b holds not b < a;
thus a in field(the InternalRel of A) by A1;
let y;
assume that A4: y in field(the InternalRel of A) and
A5: y <> a and A6: [y,a] in the InternalRel of A;
y is Element of A by A4,Th2;
then reconsider b = y as Element of A;
b <= a by A6,ORDERS_1:def 9;
then b < a by A5,ORDERS_1:def 10;
hence thesis by A3;
end;
theorem
a is_maximal_in the InternalRel of A iff
for b holds not a < b
proof A1: the carrier of A = field(the InternalRel of A) by Th2;
thus a is_maximal_in the InternalRel of A implies for b holds not a < b
proof assume A2: a is_maximal_in the InternalRel of A;
let b;
a = b or not [a,b] in the InternalRel of A by A1,A2,Def9;
then a = b or not a <= b by ORDERS_1:def 9;
hence thesis by ORDERS_1:def 10;
end;
assume A3: for b holds not a < b;
thus a in field(the InternalRel of A) by A1;
let y;
assume that A4: y in field(the InternalRel of A) and
A5: y <> a and A6: [a,y] in the InternalRel of A;
y is Element of A by A4,Th2;
then reconsider b = y as Element of A;
a <= b by A6,ORDERS_1:def 9;
then a < b by A5,ORDERS_1:def 10;
hence thesis by A3;
end;
theorem
a is_superior_of the InternalRel of A iff
for b st a <> b holds b < a
proof A1: the carrier of A = field(the InternalRel of A) by Th2;
thus a is_superior_of the InternalRel of A implies
for b st a <> b holds b < a
proof assume A2: a is_superior_of the InternalRel of A;
let b;
assume A3: a <> b;
then [b,a] in the InternalRel of A by A1,A2,Def11;
then b <= a by ORDERS_1:def 9;
hence thesis by A3,ORDERS_1:def 10;
end;
assume A4: for b st a <> b holds b < a;
thus a in field(the InternalRel of A) by A1;
let y;
assume y in field(the InternalRel of A);
then y is Element of A by Th2;
then reconsider b = y as Element of A;
assume y <> a;
then b < a by A4;
then b <= a by ORDERS_1:def 10;
hence thesis by ORDERS_1:def 9;
end;
theorem
a is_inferior_of the InternalRel of A iff
for b st a <> b holds a < b
proof A1: the carrier of A = field(the InternalRel of A) by Th2;
thus a is_inferior_of the InternalRel of A implies
for b st a <> b holds a < b
proof assume A2: a is_inferior_of the InternalRel of A;
let b;
assume A3: a <> b;
then [a,b] in the InternalRel of A by A1,A2,Def12;
then a <= b by ORDERS_1:def 9;
hence thesis by A3,ORDERS_1:def 10;
end;
assume A4: for b st a <> b holds a < b;
thus a in field(the InternalRel of A) by A1;
let y;
assume y in field(the InternalRel of A);
then y is Element of A by Th2;
then reconsider b = y as Element of A;
assume y <> a;
then a < b by A4;
then a <= b by ORDERS_1:def 10;
hence thesis by ORDERS_1:def 9;
end;
Lm15: 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;
R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X &
R is_connected_in X by A1,WELLORD1:def 5;
hence R is_reflexive_in Y & R is_transitive_in Y & R is_antisymmetric_in Y &
R is_connected_in Y by A2,Lm8,ORDERS_1:93,94,95;
let Z;
assume that A3: Z c= Y and A4: Z <> {};
Z c= X & R is_well_founded_in X by A1,A2,A3,WELLORD1:def 5,XBOOLE_1:1;
hence thesis by A4,WELLORD1:def 3;
end;
::
:: Kuratowski - Zorn Lemma.
::
theorem Th73:
(for C ex a st for b st b in C holds b <= a) implies
ex a st for b holds not a < b
proof assume A1: for C ex a st for b st b in C holds b <= a;
consider f being Choice_Function of BOOL(the carrier of A);
reconsider F = union(Chains(f)) as Chain of f by ORDERS_1:89;
consider a such that A2: for b st b in F holds b <= a by A1;
take a;
let b;
assume A3: a < b;
now let a1;
assume a1 in F;
then a1 <= a by A2;
hence a1 < b by A3,ORDERS_1:32;
end;
then b in {a1 : for a2 st a2 in F holds a2 < a1};
then UpperCone(F) <> {} by ORDERS_1:def 12;
then not UpperCone(F) in {{}} by TARSKI:def 1;
then UpperCone(F) in bool(the carrier of A) \ {{}} by XBOOLE_0:def 4;
then UpperCone(F) in BOOL(the carrier of A) &
not {} in BOOL(the carrier of A) by ORDERS_1:4,def 2;
then A4: f.UpperCone(F) in UpperCone(F) by ORDERS_1:def 1;
then reconsider c = f.UpperCone(F) as Element of A;
c in {a1 : for a2 st a2 in F holds a2 < a1} by A4,ORDERS_1:def 12;
then A5: ex c11 being Element of A st c11 = c &
for a2 st a2 in F holds a2 < c11;
reconsider Z = F \/ {c} as Subset of A;
Z c= the carrier of A &
the InternalRel of A is_reflexive_in the carrier of A &
the InternalRel of A is_antisymmetric_in the carrier of A &
the InternalRel of A is_transitive_in the carrier of A
by ORDERS_1:def 4,def 5,def 6;
then A6: the InternalRel of A is_reflexive_in Z &
the InternalRel of A is_antisymmetric_in Z &
the InternalRel of A is_transitive_in Z
by ORDERS_1:93,94,95;
A7: the InternalRel of A is_connected_in Z
proof let x,y;
assume that A8: x in Z and A9: y in Z;
reconsider x1 = x, y1 = y as Element of A by A8,A9;
now per cases by A8,A9,XBOOLE_0:def 2;
suppose x1 in F & y1 in F;
then x1 <= y1 or y1 <= x1 by ORDERS_1:38;
hence thesis by ORDERS_1:def 9;
suppose x1 in F & y1 in {c};
then x1 in F & y1 = c by TARSKI:def 1;
then x1 < y1 by A5;
then x1 <= y1 by ORDERS_1:def 10;
hence thesis by ORDERS_1:def 9;
suppose x1 in {c} & y1 in F;
then y1 in F & x1 = c by TARSKI:def 1;
then y1 < x1 by A5;
then y1 <= x1 by ORDERS_1:def 10;
hence thesis by ORDERS_1:def 9;
suppose x1 in {c} & y1 in {c};
then c <= c & x1 = c & y1 = c by TARSKI:def 1;
hence thesis;
end;
hence thesis;
end;
the InternalRel of A is_well_founded_in Z
proof let Y;
assume that A10: Y c= Z and A11: Y <> {};
now per cases;
case A12: Y = {c};
take x = c;
thus x in Y by A12,TARSKI:def 1;
assume (the InternalRel of A)-Seg(x) meets Y;
then consider x' being set such that
A13: x' in (the InternalRel of A)-Seg(x) & x' in Y
by XBOOLE_0:3;
x' = c & x' in (the InternalRel of A)-Seg(x)
by A12,A13,TARSKI:def 1;
hence contradiction by WELLORD1:def 1;
case A14: Y <> {c};
set X = Y \ {c};
A15: X c= F
proof let x;
assume that A16: x in X and A17: not x in F;
x in Y by A16,XBOOLE_0:def 4;
then x in {c} & not x in {c} by A10,A16,A17,XBOOLE_0:def 2,
def 4;
hence thesis;
end;
the InternalRel of A well_orders F by ORDERS_1:def 16;
then the InternalRel of A well_orders X by A15,Lm15;
then A18: the InternalRel of A is_well_founded_in X
by WELLORD1:def 5;
now assume X = {};
then Y c= {c} by XBOOLE_1:37;
hence contradiction by A11,A14,ZFMISC_1:39;
end;
then consider x such that A19: x in X and
A20: (the InternalRel of A)-Seg(x) misses X
by A18,WELLORD1:def 3;
A21: (the InternalRel of A)-Seg(x) /\ X = {} by A20,XBOOLE_0:def
7;
take x' = x;
X c= Y by XBOOLE_1:36;
hence x' in Y by A19;
now per cases;
suppose c in Y;
then {c} c= Y by ZFMISC_1:37;
then A22: Y = X \/ {c} by XBOOLE_1:45;
A23: now assume c in (the InternalRel of A)-Seg(x');
then A24: c <> x' & [c,x'] in the InternalRel of A
by WELLORD1:def 1;
x' in F by A15,A19;
then reconsider x'' = x' as Element of A;
c <> x'' & c <= x'' by A24,ORDERS_1:def 9;
then c < x'' & x'' < c by A5,A15,A19,ORDERS_1:def 10;
hence contradiction by ORDERS_1:28;
end;
now assume A25: (the InternalRel of A)-Seg(x') /\ {c} <> {}
;
consider x being
Element of (the InternalRel of A)-Seg(x') /\ {c};
x in {c} by A25,XBOOLE_0:def 3;
then x = c & x in (the InternalRel of A)-Seg(x')
by A25,TARSKI:def 1,XBOOLE_0:def 3;
hence contradiction by A23;
end;
then (the InternalRel of A)-Seg(x') /\ Y = {} \/ {}
by A21,A22,XBOOLE_1:23
.= {};
hence (the InternalRel of A)-Seg(x') misses Y by XBOOLE_0:def
7;
suppose not c in Y;
then Y misses {c} by ZFMISC_1:56;
hence (the InternalRel of A)-Seg(x') misses Y
by A20,XBOOLE_1:83;
end;
hence (the InternalRel of A)-Seg(x') misses Y;
end;
hence thesis;
end;
then A26: the InternalRel of A well_orders Z by A6,A7,WELLORD1:def 5;
the InternalRel of A is_strongly_connected_in Z by A6,A7,ORDERS_1:92;
then A27: Z is Chain of A by ORDERS_1:def 11;
now let a1;
assume A28: a1 in Z;
now per cases;
suppose A29: a1 = c;
InitSegm(Z,c) = F
proof
thus InitSegm(Z,c) c= F
proof let x;
assume that A30: x in InitSegm(Z,c) and A31: not x in F;
A32: x in LowerCone{c} /\ Z by A30,ORDERS_1:def 14;
then x in Z by XBOOLE_0:def 3;
then x in {c} by A31,XBOOLE_0:def 2;
then x = c & x in LowerCone{c} by A32,TARSKI:def 1,XBOOLE_0:
def 3;
hence contradiction by ORDERS_1:50;
end;
let x;
assume A33: x in F;
then A34: x in Z by XBOOLE_0:def 2;
reconsider y = x as Element of A by A33;
y < c by A5,A33;
then x in LowerCone{c} by ORDERS_1:52;
then x in LowerCone{c} /\ Z by A34,XBOOLE_0:def 3;
hence thesis by ORDERS_1:def 14;
end;
hence f.UpperCone(InitSegm(Z,a1)) = a1 by A29;
suppose a1 <> c;
then not a1 in {c} by TARSKI:def 1;
then A35: a1 in F by A28,XBOOLE_0:def 2;
InitSegm(Z,a1) = InitSegm(F,a1)
proof
thus InitSegm(Z,a1) c= InitSegm(F,a1)
proof let x;
assume x in InitSegm(Z,a1);
then A36: x in LowerCone{a1} /\ Z by ORDERS_1:def 14;
then A37: x in LowerCone{a1} by XBOOLE_0:def 3;
now assume A38: not x in F;
x in Z by A36,XBOOLE_0:def 3;
then x in {c} by A38,XBOOLE_0:def 2;
then x = c by TARSKI:def 1;
then c in {c1 : for c2 st c2 in {a1} holds c1 < c2}
by A37,ORDERS_1:
def 13;
then A39: ex c1 st c1 = c &
for c2 st c2 in {a1} holds c1 < c2;
a1 in {a1} by TARSKI:def 1;
then c < a1 & a1 < c by A5,A35,A39;
hence contradiction by ORDERS_1:28;
end;
then x in LowerCone{a1} /\ F by A37,XBOOLE_0:def 3;
hence thesis by ORDERS_1:def 14;
end;
F c= Z by XBOOLE_1:7;
hence thesis by ORDERS_1:65;
end;
hence f.UpperCone(InitSegm(Z,a1)) = a1 by A35,ORDERS_1:def 16;
end;
hence f.UpperCone(InitSegm(Z,a1)) = a1;
end;
then reconsider Z as Chain of f by A26,A27,ORDERS_1:def 16;
c in {c} by TARSKI:def 1;
then Z in Chains(f) & c in Z by ORDERS_1:def 17,XBOOLE_0:def 2;
then c in F by TARSKI:def 4;
hence thesis by A5;
end;
definition let A be non empty set, O be Order of A;
cluster RelStr(#A,O#) -> non empty;
coherence;
end;
theorem Th74:
(for C ex a st for b st b in C holds a <= b) implies
ex a st for b holds not b < a
proof assume A1: for C ex a st for b st b in C holds a <= b;
set X = the carrier of A;
defpred P[Element of A, Element of A]
means
ex a1,a2 st a1 = $2 & a2 = $1 & a1 <= a2;
set R = (the InternalRel of A)~;
A2: for a,b being Element of A holds
[a,b] in R iff b <= a
proof let a,b be Element of A;
[a,b] in R iff [b,a] in the InternalRel of A by RELAT_1:def 7;
hence [a,b] in R iff b <= a by ORDERS_1:def 9;
end;
A3: R is reflexive by RELAT_2:27;
A4: dom R = dom the InternalRel of A by RELAT_2:29
.= X by PARTFUN1:def 4;
A5: R is total by A4,PARTFUN1:def 4;
A6: R is antisymmetric by RELAT_2:40;
R is transitive by RELAT_2:42;
then reconsider R as Order of the carrier of A by A3,A5,A6;
set B = RelStr (# the carrier of A, R #);
for E being Chain of B
ex e being Element of B st
for f being Element of B st f in E holds f <= e
proof let E be Chain of B;
reconsider C = E as Subset of A;
the InternalRel of A is_strongly_connected_in C
proof let x,y;
assume A7: x in C & y in C;
then reconsider e = x, f = y as Element of B
;
A8: (e <= f or f <= e) & R = the InternalRel of B
by A7,ORDERS_1:38;
reconsider e1 = e, f1 = f as Element of A
;
now per cases by A8,ORDERS_1:def 9;
suppose [e,f] in R;
then f1 <= e1 by A2;
hence thesis by ORDERS_1:def 9;
suppose [f,e] in R;
then e1 <= f1 by A2;
hence thesis by ORDERS_1:def 9;
end;
hence thesis;
end;
then reconsider C as Chain of A by ORDERS_1:def 11;
consider a such that A9: for b st b in C holds a <= b by A1;
reconsider e = a as Element of B;
take e;
let f be Element of B;
reconsider b = f as Element of A;
assume f in E;
then a <= b by A9;
then [f,e] in R & R = the InternalRel of B by A2;
hence thesis by ORDERS_1:def 9;
end;
then consider e being Element of B such that
A10: for f being Element of B holds not e < f by Th73;
reconsider d = e as Element of A;
take d;
let b;
reconsider f = b as Element of B;
assume A11: b < d;
then b <= d by ORDERS_1:def 10;
then [e,f] in R & R = the InternalRel of B by A2;
then e <= f & b <> d by A11,ORDERS_1:def 9;
then e < f by ORDERS_1:def 10;
hence thesis by A10;
end;
reserve A,C for Ordinal;
theorem Th75:
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 & R is_transitive_in FIELD &
R is_antisymmetric_in FIELD and
A2: field R = FIELD and
A3: FIELD has_upper_Zorn_property_wrt R;
reconsider XD = FIELD as non empty set by A3,Th51;
consider D such that
A4: D = XD;
not D in {{}} & D in bool D by TARSKI:def 1,ZFMISC_1:def 1;
then reconsider M = (bool D) \ {{}} as non empty set by XBOOLE_0:def 4;
consider f being Choice_Function of M;
{} in {{}} by TARSKI:def 1;
then A5: not {} in M by XBOOLE_0:def 4;
defpred P[set,set] means $1 <> {} & $2 = f.$1 or $1 = {} & $2 = D;
A6: for x st x in bool D ex y st P[x,y]
proof let x such that x in bool D;
x = {} implies thesis;
hence thesis;
end;
A7: for x,y,z st x in bool D & P[x,y] & P[x,z] holds y = z;
consider g such that
A8: dom g = bool D & for x st x in bool D holds P[x,g.x] from FuncEx(A7,A6);
A9: g.{} = D
proof
{} c= D by XBOOLE_1:2;
hence thesis by A8;
end;
A10: X in bool D & X <> {} implies g.X in X
proof assume A11: X in bool D & X <> {};
then P[X,g.X] & P[X,f.X] & not X in {{}} by A8,TARSKI:def 1;
then f.X = g.X & X in M by A11,XBOOLE_0:def 4;
hence g.X in X by A5,ORDERS_1:def 1;
end;
A12: for L holds { d : for x st x in rng L holds x <> d & [x,d] in R } c= D
proof let L,x; 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;
A13: now let A,B,L1,L2; assume that
A14: 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
A15: 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
A16: C c= A & C c= B;
defpred P[Ordinal] means
$1 c= C 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= C implies L1|A2 = L2|A2 and
A19: A1 c= C;
A1 c= A & A1 c= B by A16,A19,XBOOLE_1:1;
then A20: dom(L1|A1) = A1 & dom(L2|A1) = A1 by A14,A15,RELAT_1:91;
now let x; assume
A21: x in A1;
then reconsider A3 = x as Ordinal by ORDINAL1:23;
A3 in C by A19,A21;
then A3 in A & A3 in B & A3 c= A1 & A3 c= C
by A16,A21,ORDINAL1:def 2;
then L1|A3 = L2|A3 & L1.x = L1|A1.x & L2.x = L2|A1.x &
L1.A3 =
g.{ d1 : for x st x in rng(L1|A3) holds x <> d1 & [x,d1] in R } &
L2.A3 =
g.{ d2 : for x st x in rng(L2|A3) holds x <> d2 & [x,d2] in R }
by A14,A15,A18,A21,FUNCT_1:72;
hence L1|A1.x = L2|A1.x;
end;
hence L1|A1 = L2|A1 by A20,FUNCT_1:9;
end;
for A1 holds P[A1] from Transfinite_Ind(A17);
hence L1|C = L2|C;
end;
defpred ON[Ordinal,set] 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 };
A22: ON[A,x] & ON[A,y] implies x = y
proof given L1 such that
A23: x = g.{ d1 : for x st x in rng L1 holds x <> d1 & [x,d1] in R } and
A24: 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
A25: y = g.{ d1 : for x st x in rng L2 holds x <> d1 & [x,d1] in R } and
A26: 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;
A27: for A1 st for A2 st A2 in A1 holds P[A2] holds P[A1]
proof let A1 such that
A28: for A2 st A2 in A1 holds A2 c= A implies L1|A2 = L2|A2 and
A29: A1 c= A;
A30: dom(L1|A1) = A1 & dom(L2|A1) = A1 by A24,A26,A29,RELAT_1:91;
now let x; assume
A31: x in A1;
then reconsider A3 = x as Ordinal by ORDINAL1:23;
A3 in A & A3 c= A1 & A3 c= A by A29,A31,ORDINAL1:def 2;
then L1|A3 = L2|A3 & L1.x = L1|A1.x & L2.x = L2|A1.x &
L1.A3 =
g.{ d1 : for x st x in rng(L1|A3) holds x <> d1 & [x,d1] in R } &
L2.A3 =
g.{ d2 : for x st x in rng(L2|A3) holds x <> d2 & [x,d2] in R }
by A24,A26,A28,A31,FUNCT_1:72;
hence L1|A1.x = L2|A1.x;
end;
hence L1|A1 = L2|A1 by A30,FUNCT_1:9;
end;
for A1 holds P[A1] from Transfinite_Ind(A27);
then L1|A = L2|A & L1 = L1|A & L2 = L2|A by A24,A26,RELAT_1:97;
hence x = y by A23,A25;
end;
A32: for d,A,B st ON[A,d] & ON[B,d] holds A = B
proof let d,A,B;
given L1 such that
A33: d = g.{ d1 : for x st x in rng L1 holds x <> d1 & [x,d1] in R } and
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 };
given L2 such that
A35: d = g.{ d1 : for x st x in rng L2 holds x <> d1 & [x,d1] in R } and
A36: 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 };
A37: now
set X = { d1 : for x st x in rng(L2|A) holds x <> d1 & [x,d1] in R };
set Y = { d1 : for x st x in rng L2 holds x <> d1 & [x,d1] in R };
assume
A38: A in B;
then A39: L2.A = g.X & A c= B & A c= A by A36,ORDINAL1:def 2;
then L2|A = L1|A by A13,A34,A36 .= L1 by A34,RELAT_1:97;
then A40: d in rng L2 by A33,A36,A38,A39,FUNCT_1:def 5;
A41: Y c= D
proof let x; 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;
then A42: P[Y,g.Y] by A8;
A43: not d in d;
now assume Y <> {}; then not Y in
{{}} & P[Y,f.Y] by TARSKI:def 1;
then Y in M & g.Y = f.Y by A8,A41,XBOOLE_0:def 4;
then d in Y by A5,A35,ORDERS_1:def 1;
then ex d1 st
d = d1 & for x st x in rng L2 holds x <> d1 & [x,d1] in R;
hence contradiction by A40;
end;
hence contradiction by A35,A42,A43;
end;
now
set X = { d1 : for x st x in rng(L1|B) holds x <> d1 & [x,d1] in R };
set Y = { d1 : for x st x in rng L1 holds x <> d1 & [x,d1] in R };
assume
A44: B in A;
then A45: L1.B = g.X & B c= A & B c= B by A34,ORDINAL1:def 2;
then L1|B = L2|B by A13,A34,A36 .= L2 by A36,RELAT_1:97;
then A46: d in rng L1 by A34,A35,A44,A45,FUNCT_1:def 5;
A47: Y c= D
proof let x; 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;
then A48: P[Y,g.Y] by A8;
A49: not d in d;
now assume Y <> {}; then not Y in
{{}} & P[Y,f.Y] by TARSKI:def 1;
then Y in M & g.Y = f.Y by A8,A47,XBOOLE_0:def 4;
then d in Y by A5,A33,ORDERS_1:def 1;
then ex d1 st
d = d1 & for x st x in rng L1 holds x <> d1 & [x,d1] in R;
hence contradiction by A46;
end;
hence contradiction by A33,A48,A49;
end;
hence thesis by A37,ORDINAL1:24;
end;
defpred OM[Ordinal] means ON[$1,D];
A50: ex A st OM[A]
proof assume
A51: for A holds not ON[A,D];
defpred OO[Ordinal] means
ex d st ON[$1,d];
A52: for A st for B st B in A holds OO[B] holds OO[A]
proof let A such that
A53: for B st B in A ex d st ON[B,d];
defpred P[set,set] means
ex C st $1 = C & ON[C,$2];
A54: for x,y,z st x in A & P[x,y] & P[x,z] holds y = z by A22;
A55: for x st x in A ex y st P[x,y]
proof let x; assume
A56: x in A;
then reconsider C = x as Ordinal by ORDINAL1:23;
consider d such that
A57: ON[C,d] by A53,A56;
reconsider y = d as set;
take y,C; thus thesis by A57;
end;
consider h such that
A58: dom h = A & for x st x in A holds P[x,h.x]
from FuncEx(A54,A55);
reconsider h as T-Sequence by A58,ORDINAL1:def 7;
set X = { d1 : for x st x in rng h holds x <> d1 & [x,d1] in R };
A59: 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 A58;
let B,L; assume
A60: B in A & L = h|B;
then ex C st B = C & ON[C,h.B] by A58;
then consider L1 such that
A61: h.B = g.{d1: for x st x in rng L1 holds x <> d1 & [x,d1] in
R } and
A62: 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 };
A63: for x st x in B holds L1.x = h|B.x
proof let x; assume
A64: x in B;
then reconsider A1 = x as Ordinal by ORDINAL1:23;
A65: ON[A1,L1.x]
proof reconsider K = L1|A1 as T-Sequence;
take K;
thus L1.x =
g.{d1: for x st x in rng K holds x <> d1 & [x,d1] in R }
by A62,A64;
A1 c= B by A64,ORDINAL1:def 2;
hence dom K = A1 by A62,RELAT_1:91;
let A2,L2; assume
A66: A2 in A1 & L2 = K|A2;
then A67: A2 c= A1 & A2 in B by A64,ORDINAL1:19,def 2;
then L2 = L1|A2 & K.A2 = L1.A2 by A66,FUNCT_1:72,82;
hence thesis by A62,A67;
end;
A1 in A by A60,A64,ORDINAL1:19;
then A68: ex A2 st x = A2 & ON[A2,h.x] by A58;
h|B.x = h.x by A64,FUNCT_1:72;
hence thesis by A22,A65,A68;
end;
B c= A by A60,ORDINAL1:def 2;
then dom(h|B) = B by A58,RELAT_1:91;
then h|B = L1 by A62,A63,FUNCT_1:9;
hence thesis by A60,A61;
end;
then A69: X <> {} by A9,A51;
A70: X c= D
proof let x; 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;
then g.X in X by A10,A69;
then reconsider d = g.X as Element of D by A70;
take d; thus thesis by A59;
end;
A71: for A holds OO[A] from Transfinite_Ind(A52);
defpred P[set,set] means
ex A st $2 = A & ON[A,$1];
A72: for x,y,z st P[x,y] & P[x,z] holds y = z
proof let x,y,z;
given A1 such that
A73: y = A1 & ON[A1,x];
given A2 such that
A74: z = A2 & ON[A2,x];
consider d1 such that
A75: ON[A1,d1] by A71;
consider d2 such that
A76: ON[A2,d2] by A71;
d1 = x & d2 = x by A22,A73,A74,A75,A76;
hence thesis by A32,A73,A74;
end;
consider X such that
A77: x in X iff ex y st y in D & P[y,x] from Fraenkel(A72);
for A holds A in X
proof let A; ex d st ON[A,d] by A71;
hence thesis by A77;
end;
hence contradiction by ORDINAL1:38;
end;
consider A such that
A78: OM[A] & for B st OM[B] holds A c= B from Ordinal_Min(A50);
defpred P[set] means ex B st B in A & ON[B,$1];
consider X such that
A79: x in X iff x in D & P[x] from Separation;
D <> {} & D in bool D by ZFMISC_1:def 1;
then reconsider d = g.D as Element of D by A10;
A80: d in D & ON[{},d]
proof thus d in D;
deffunc H(Ordinal) = 0;
consider L such that
A81: dom L = {} &
for B,L1 st B in {} & L1 = L|B holds L.B = H(L1) from TS_Exist;
take L;
A82: { d1 : for x st x in rng L holds x <> d1 & [x,d1] in R } c= D by A12;
D c= { d1 : for x st x in rng L holds x <> d1 & [x,d1] in R }
proof let x; 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 A81,RELAT_1:65;
hence thesis;
end;
hence d = g.{ d1 : for x st x in rng L holds x <> d1 & [x,d1] in
R } by A82,XBOOLE_0:def 10;
thus dom L = {} by A81;
thus thesis;
end;
not Y in Y;
then d <> D;
then {} c= A & {} <> A by A22,A78,A80,XBOOLE_1:2;
then {} c< A by XBOOLE_0:def 8;
then {} in A by ORDINAL1:21;
then reconsider X as non empty set by A79,A80;
A83: X c= D proof let x; thus thesis by A79; end;
R|_2 X is_linear-order
proof
R is reflexive by A1,A2,RELAT_2:def 9;
hence
R|_2 X is reflexive by WELLORD1:22;
R is transitive by A1,A2,RELAT_2:def 16;
hence R|_2 X is transitive by WELLORD1:24;
R is antisymmetric by A1,A2,RELAT_2:def 12;
hence R|_2 X is antisymmetric by WELLORD1:25;
thus R|_2 X is connected
proof let x,y; assume
x in field(R|_2 X) & y in field(R|_2 X);
then A84: x in X & y in X by WELLORD1:19;
then reconsider x' = x, y' = y as Element of D by A79;
A85: [x,y] in [:X,X:] & [y,x] in [:X,X:] by A84,ZFMISC_1:106;
consider A1 such that
A86: A1 in A & ON[A1,x] by A79,A84;
consider A2 such that
A87: A2 in A & ON[A2,y] by A79,A84;
consider L1 such that
A88: x' = g.{ d1 : for x st x in rng L1 holds x <> d1 & [x,d1] in R } and
A89: 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 A86;
consider L2 such that
A90: y' = g.{ d1 : for x st x in rng L2 holds x <> d1 & [x,d1] in R } and
A91: 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 A87;
A92: now
set Z = { d1 : for x st x in rng(L2|A1) holds x <> d1 & [x,d1] in
R };
set Y = { d1 : for x st x in rng L2 holds x <> d1 & [x,d1] in R };
assume
A93: A1 in A2;
then A94: L2.A1 = g.Z & A1 c= A2 & A1 c= A1 by A91,ORDINAL1:def 2;
then L2|A1 = L1|A1 by A13,A89,A91 .= L1 by A89,RELAT_1:97;
then A95: x' in rng L2 by A88,A91,A93,A94,FUNCT_1:def 5;
A96: Y c= D by A12;
not y' in y';
then Y <> {} by A9,A90;
then y' in Y by A10,A90,A96;
then ex d1 st
y' = d1 & for x st x in rng L2 holds x <> d1 & [x,d1] in R;
then [x,y] in R by A95;
hence thesis by A85,WELLORD1:16;
end;
A97: now
set Z = { d1 : for x st x in rng(L1|A2) holds x <> d1 & [x,d1] in
R };
set Y = { d1 : for x st x in rng L1 holds x <> d1 & [x,d1] in R };
assume
A98: A2 in A1;
then A99: L1.A2 = g.Z & A2 c= A1 & A2 c= A2 by A89,ORDINAL1:def 2;
then L1|A2 = L2|A2 by A13,A89,A91 .= L2 by A91,RELAT_1:97;
then A100: y' in rng L1 by A89,A90,A98,A99,FUNCT_1:def 5;
A101: Y c= D by A12;
not d1 in d1;
then Y <> {} by A9,A88;
then x' in Y by A10,A88,A101;
then ex d1 st
x' = d1 & for x st x in rng L1 holds x <> d1 & [x,d1] in R;
then [y,x] in R by A100;
hence thesis by A85,WELLORD1:16;
end;
A1 = A2 implies thesis by A22,A86,A87;
hence thesis by A92,A97,ORDINAL1:24;
end;
end;
then consider x such that
A102: x in D & for y st y in X holds [y,x] in R by A3,A4,A83,Def7;
take x;
thus x in field R by A2,A4,A102;
let y such that
A103: y in field R & y <> x & [x,y] in R;
consider L such that
A104: D = g.{ d1 : for x st x in rng L holds x <> d1 & [x,d1] in R } and
A105: 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 A78;
A106: rng L c= X
proof let z; assume
z in rng L;
then consider y such that
A107: y in dom L & z = L.y by FUNCT_1:def 5;
reconsider y as Ordinal by A107,ORDINAL1:23;
A108: ON[y,z]
proof reconsider K = L|y as T-Sequence;
take K;
thus z = g.{ d2 : for x st x in rng K holds x <> d2 & [x,d2] in R }
by A105,A107;
y c= dom L by A107,ORDINAL1:def 2;
hence
A109: dom K = y by RELAT_1:91;
let B,L1; assume
A110: B in y & L1 = K|B;
then A111: K.B = L.B by A109,FUNCT_1:70;
B c= y by A110,ORDINAL1:def 2;
then L1 = L|B & B in A by A105,A107,A110,FUNCT_1:82,ORDINAL1:19;
hence K.B = g.{ d1 : for x st x in rng L1 holds x <> d1 & [x,d1] in
R }
by A105,A111;
end;
set Z = { d2 : for x st x in rng(L|y) holds x <> d2 & [x,d2] in R };
A112: now assume Z = {}; then z = D by A9,A105,A107;
then dom L c= y by A78,A105,A108;
hence contradiction by A107,ORDINAL1:7;
end;
A113: Z c= D by A12;
then g.Z in Z by A10,A112;
then z in Z by A105,A107; hence z in X by A79,A105,A107,A108,A113;
end;
set Z = { d1 : for x st x in rng L holds x <> d1 & [x,d1] in R };
A114: now assume y in X;
then [y,x] in R & R is_antisymmetric_in field R by A1,A2,A102;
hence contradiction by A2,A4,A102,A103,RELAT_2:def 4;
end;
reconsider y' = y as Element of D by A2,A4,A103;
now let z; assume A115: z in rng L;
hence z <> y' by A106,A114;
reconsider z' = z as Element of X by A106,A115;
[z',x] in R & R is_transitive_in field R & z in D
by A1,A2,A79,A102,A106,A115;
hence [z,y] in R by A2,A4,A102,A103,RELAT_2:def 8;
end;
then A116: y in Z & Z c= D by A12;
then D in Z by A10,A104;
hence contradiction by A116,ORDINAL1:7;
end;
theorem
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 & field R = X &
X has_lower_Zorn_property_wrt R;
R = R~~;
then X has_upper_Zorn_property_wrt R~ & R~ partially_orders X &
field(R~) = X by A1,Th39,Th53,RELAT_1:38;
then consider x such that
A2: x is_maximal_in R~ by Th75;
take x; thus thesis by A2,Th65;
end;
theorem Th77:
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: field R = D by WELLORD2:def 1;
A4: R partially_orders D
proof
R is reflexive & R is transitive & R is antisymmetric
by WELLORD2:2,3,5;
hence R is_reflexive_in D & R is_transitive_in D &
R is_antisymmetric_in D by A3,RELAT_2:def 9,def 12,def 16;
end;
D has_upper_Zorn_property_wrt R
proof let Z; assume
A5: Z c= D & R|_2 Z is_linear-order;
then R|_2 Z is connected by Def3;
then A6: R|_2 Z is_connected_in field(R|_2 Z) by RELAT_2:def 14;
A7: Z c= field(R|_2 Z)
proof let x; assume x in Z;
then [x,x] in [:Z,Z:] & [x,x] in R by A5,WELLORD2:def 1,ZFMISC_1:106
;
then [x,x] in R|_2 Z by WELLORD1:16;
hence thesis by RELAT_1:30;
end;
set Q = R|_2 Z;
Z is c=-linear
proof let X1,X2; assume
A8: X1 in Z & X2 in Z;
then X1 <> X2 implies [X1,X2] in Q or [X2,X1] in Q by A6,A7,RELAT_2:
def 6
;
then (X1 <> X2 implies [X1,X2] in R or [X2,X1] in R) & X1 in D & X2
in D &
X1 c= X1 by A5,A8,WELLORD1:16;
hence X1 c= X2 or X2 c= X1 by WELLORD2:def 1;
end;
then consider Y such that
A9: Y in X & for X1 st X1 in Z holds X1 c= Y by A2,A5;
take x = Y; thus x in D by A9;
let y; assume y in Z;
then y c= Y & y in D by A5,A9;
hence thesis by A9,WELLORD2:def 1;
end;
then consider x such that
A10: x is_maximal_in R by A3,A4,Th75;
take Y = x;
A11: Y in field R & not ex y st y in field R & y <> Y & [Y,y] in
R by A10,Def9;
thus Y in X by A3,A10,Def9;
let Z; assume
A12: Z in X & Z <> Y;
then not [Y,Z] in R by A3,A10,Def9;
hence not Y c= Z by A3,A11,A12,WELLORD2:def 1;
end;
theorem Th78:
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: field R = field RelIncl D by RELAT_1:38 .= D by WELLORD2:def 1;
A4: 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;
A5: R partially_orders D
proof
RelIncl D is reflexive & RelIncl D is transitive &
RelIncl D is antisymmetric & field RelIncl D = D
by WELLORD2:2,3,5,def 1;
then RelIncl D is_reflexive_in D & RelIncl D is_transitive_in D &
RelIncl D is_antisymmetric_in D by RELAT_2:def 9,def 12,def 16;
hence R is_reflexive_in D & R is_transitive_in D &
R is_antisymmetric_in D by Lm9,Lm10,Lm11;
end;
D has_upper_Zorn_property_wrt R
proof let Z; assume
A6: Z c= D & R|_2 Z is_linear-order;
then R|_2 Z is connected by Def3;
then A7: R|_2 Z is_connected_in field(R|_2 Z) by RELAT_2:def 14;
A8: Z c= field(R|_2 Z)
proof let x; assume x in Z;
then [x,x] in [:Z,Z:] & [x,x] in R by A4,A6,ZFMISC_1:106;
then [x,x] in R|_2 Z by WELLORD1:16;
hence thesis by RELAT_1:30;
end;
set Q = R|_2 Z;
Z is c=-linear
proof let X1,X2; assume
A9: X1 in Z & X2 in Z;
then X1 <> X2 implies [X1,X2] in Q or [X2,X1] in Q by A7,A8,RELAT_2:
def 6
;
then (X1 <> X2 implies [X1,X2] in R or [X2,X1] in R) & X1 in D & X2
in D
by A6,A9,WELLORD1:16;
then (X1 <> X2 implies [X1,X2] in RelIncl D or [X2,X1] in RelIncl D)
&
X1 in D & X2 in D & X1 c= X1 by RELAT_1:def 7;
hence X1 c= X2 or X2 c= X1 by WELLORD2:def 1;
end;
then consider Y such that
A10: Y in X & for X1 st X1 in Z holds Y c= X1 by A2,A6;
take x = Y; thus x in D by A10;
let y; assume y in Z;
then Y c= y & y in D by A6,A10;
then [Y,y] in RelIncl D by A10,WELLORD2:def 1;
hence thesis by RELAT_1:def 7;
end;
then consider x such that
A11: x is_maximal_in R by A3,A5,Th75;
take Y = x;
A12: Y in field R & not ex y st y in field R & y <> Y & [Y,y] in
R by A11,Def9;
thus Y in X by A3,A11,Def9;
let Z; assume
A13: Z in X & Z <> Y;
then not [Y,Z] in R by A3,A11,Def9;
then not [Z,Y] in RelIncl D by RELAT_1:def 7;
hence not Z c= Y by A3,A12,A13,WELLORD2:def 1;
end;
theorem Th79:
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 let Z such that
A3: Z c= X & Z is c=-linear;
consider x being Element of X;
Z <> {} or Z = {};
then consider Y such that
A4: Y = union Z & Z <> {} or Y = x & Z = {};
take Y;
thus thesis by A1,A2,A3,A4,ZFMISC_1:92;
end;
hence thesis by A1,Th77;
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 let Z such that
A3: Z c= X & Z is c=-linear;
consider x being Element of X;
Z <> {} or Z = {};
then consider Y such that
A4: Y = meet Z & Z <> {} or Y = x & Z = {};
take Y;
thus thesis by A1,A2,A3,A4,SETFAM_1:4;
end;
hence thesis by A1,Th78;
end;
scheme Zorn_Max{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
defpred PP[set,set] means P[$1,$2];
consider R being Relation of A() such that
A5: for x,y being Element of A() holds [x,y] in R iff PP[x,y]
from Rel_On_Dom_Ex;
A6: A() c= dom R
proof let x;
assume x in A();
then reconsider x' = x as Element of A();
P[x',x'] by A1;
then [x,x] in R by A5;
hence thesis by RELAT_1:def 4;
end;
A7: dom R = A() by A6,XBOOLE_0:def 10;
then
A8: R is total by PARTFUN1:def 4;
A9: field R = dom R \/ rng R by RELAT_1:def 6;
then
A10: field R c= A();
A() c= field R by A7,A9,XBOOLE_1:7;
then
A11: field R = A() by A10,XBOOLE_0:def 10;
R is_reflexive_in A()
proof let x;
assume x in A();
then reconsider x' = x as Element of A();
P[x',x'] by A1;
hence thesis by A5;
end;
then
A12: R is reflexive by A11,RELAT_2:def 9;
R is_antisymmetric_in A()
proof let x,y;
assume x in A() & y in A();
then reconsider x' = x, y' = y as Element of A();
assume [x,y] in R & [y,x] in R;
then P[x',y'] & P[y',x'] by A5;
hence thesis by A2;
end;
then
A13: R is antisymmetric by A11,RELAT_2:def 12;
R is_transitive_in A()
proof
let x,y,z;
assume x in A() & y in A() & z in A();
then reconsider x' = x, y' = y, z' = z as Element of A();
assume [x,y] in R & [y,z] in R;
then P[x',y'] & P[y',z'] by A5;
then P[x',z'] by A3;
hence thesis by A5;
end;
then R is transitive by A11,RELAT_2:def 16;
then reconsider R as Order of A() by A8,A12,A13;
set B = RelStr (# A(),R #);
now let C be Chain of B;
now let x,y be Element of A();
reconsider a = x, b = y as Element of B;
assume x in C & y in C;
then a <= b or b <= a by ORDERS_1:38;
then [a,b] in R or [b,a] in R by ORDERS_1:def 9;
hence P[x,y] or P[y,x] by A5;
end;
then consider y being Element of A() such that
A14: for x being Element of A() st x in C holds P[x,y] by A4;
reconsider a' = y as Element of B;
take a = a';
let b be Element of B;
reconsider x = b as Element of A();
assume b in C;
then P[x,y] by A14;
then [x,y] in R by A5;
hence b <= a by ORDERS_1:def 9;
end;
then consider a being Element of B such that
A15: for b being Element of B holds not a < b by Th73;
reconsider x = a as Element of A();
take x;
let y be Element of A();
reconsider b = y as Element of B;
assume A16: x <> y;
not a < b by A15;
then not a <= b by A16,ORDERS_1:def 10;
then not [x,y] in R by ORDERS_1:def 9;
hence thesis by A5;
end;
scheme Zorn_Min{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
defpred PP[set,set] means P[$1,$2];
consider R being Relation of A() such that
A5: for x,y being Element of A() holds [x,y] in R iff PP[x,y]
from Rel_On_Dom_Ex;
A6: A() c= dom R
proof let x;
assume x in A();
then reconsider x' = x as Element of A();
P[x',x'] by A1;
then [x,x] in R by A5;
hence thesis by RELAT_1:def 4;
end;
A7: dom R = A() by A6,XBOOLE_0:def 10;
then
A8: R is total by PARTFUN1:def 4;
A9: field R = dom R \/ rng R by RELAT_1:def 6;
then
A10: field R c= A();
A() c= field R by A7,A9,XBOOLE_1:7;
then
A11: field R = A() by A10,XBOOLE_0:def 10;
R is_reflexive_in A()
proof let x;
assume x in A();
then reconsider x' = x as Element of A();
P[x',x'] by A1;
hence thesis by A5;
end;
then
A12: R is reflexive by A11,RELAT_2:def 9;
R is_antisymmetric_in A()
proof let x,y;
assume x in A() & y in A();
then reconsider x' = x, y' = y as Element of A();
assume [x,y] in R & [y,x] in R;
then P[x',y'] & P[y',x'] by A5;
hence thesis by A2;
end;
then
A13: R is antisymmetric by A11,RELAT_2:def 12;
R is_transitive_in A()
proof
let x,y,z;
assume x in A() & y in A() & z in A();
then reconsider x' = x, y' = y, z' = z as Element of A();
assume [x,y] in R & [y,z] in R;
then P[x',y'] & P[y',z'] by A5;
then P[x',z'] by A3;
hence thesis by A5;
end;
then R is transitive by A11,RELAT_2:def 16;
then reconsider R as Order of A() by A8,A12,A13;
reconsider R as Order of A();
set B = RelStr (# A(),R #);
now let C be Chain of B;
now let x,y be Element of A();
reconsider a = x, b = y as Element of B;
assume x in C & y in C;
then a <= b or b <= a by ORDERS_1:38;
then [a,b] in R or [b,a] in R by ORDERS_1:def 9;
hence P[x,y] or P[y,x] by A5;
end;
then consider y being Element of A() such that
A14: for x being Element of A() st x in C holds P[y,x] by A4;
reconsider a' = y as Element of B;
take a = a';
let b be Element of B;
reconsider x = b as Element of A();
assume b in C;
then P[y,x] by A14;
then [y,x] in R by A5;
hence a <= b by ORDERS_1:def 9;
end;
then consider a being Element of B such that
A15: for b being Element of B holds not b < a by Th74;
reconsider x = a as Element of A();
take x;
let y be Element of A();
reconsider b = y as Element of B;
assume A16: x <> y;
not b < a by A15;
then not b <= a by A16,ORDERS_1:def 10;
then not [y,x] in R by ORDERS_1:def 9;
hence thesis by A5;
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
A1: R partially_orders X & field R = X;
defpred P[set] means
ex P st $1 = P & R c= P & P partially_orders X & field P = X;
consider Rel being set such that
A2: x in Rel iff x in bool [:X,X:] & P[x]
from Separation;
R c= [:X,X:] by A1,Lm2;
then A3: Rel <> {} by A1,A2;
for Z st Z <> {} & Z c= Rel & Z is c=-linear
holds union Z in Rel
proof let Z; assume that
A4: Z <> {} & Z c= Rel and
A5: Z is c=-linear;
reconsider T = [:X,X:] as Relation by RELAT_1:6;
Z c= bool [:X,X:]
proof let x; assume x in Z; hence thesis by A2,A4;
end;
then A6: union Z c= union bool [:X,X:] & union bool [:X,X:] = T
by ZFMISC_1:95,99;
then reconsider S = union Z as Relation by RELAT_1:3;
consider y being Element of Z;
y in Rel by A4,TARSKI:def 3;
then consider P such that
A7: y = P & R c= P & P partially_orders X & field P = X by A2;
A8: P is_reflexive_in X by A7,Def5;
A9: R c= S
proof let x,y; assume
[x,y] in R;
hence thesis by A4,A7,TARSKI:def 4;
end;
A10: field S = X
proof
thus field S c= X
proof let x; assume x in field S;
then A11: x in dom S \/ rng S by RELAT_1:def 6;
A12: now assume x in dom S;
then consider y such that
A13: [x,y] in S by RELAT_1:def 4;
consider Y such that
A14: [x,y] in Y & Y in Z by A13,TARSKI:def 4;
ex P st
Y = P & R c= P & P partially_orders X & field P = X by A2,A4,A14;
hence thesis by A14,RELAT_1:30;
end;
now assume x in rng S;
then consider y such that
A15: [y,x] in S by RELAT_1:def 5;
consider Y such that
A16: [y,x] in Y & Y in Z by A15,TARSKI:def 4;
ex P st
Y = P & R c= P & P partially_orders X & field P = X by A2,A4,A16;
hence thesis by A16,RELAT_1:30;
end;
hence thesis by A11,A12,XBOOLE_0:def 2;
end;
thus X c= field S by A1,A9,RELAT_1:31;
end;
S partially_orders X
proof
thus S is_reflexive_in X
proof let x; assume x in X;
then [x,x] in P by A8,RELAT_2:def 1;
hence thesis by A4,A7,TARSKI:def 4;
end;
thus S is_transitive_in X
proof let x,y,z; assume
A17: x in X & y in X & z in X & [x,y] in S & [y,z] in S;
then consider X1 such that
A18: [x,y] in X1 & X1 in Z by TARSKI:def 4;
consider X2 such that
A19: [y,z] in X2 & X2 in Z by A17,TARSKI:def 4;
X1,X2 are_c=-comparable by A5,A18,A19,ORDINAL1:def 9;
then A20: X1 c= X2 or X2 c= X1 by XBOOLE_0:def 9;
consider P1 being Relation such that
A21: X1 = P1 & R c= P1 & P1 partially_orders X & field P1 = X by A2,A4
,A18;
consider P2 being Relation such that
A22: X2 = P2 & R c= P2 & P2 partially_orders X & field P2 = X by A2,A4
,A19;
P1 is_transitive_in X & P2 is_transitive_in X by A21,A22,Def5;
then [x,z] in P1 or [x,z] in
P2 by A17,A18,A19,A20,A21,A22,RELAT_2:def 8;
hence thesis by A18,A19,A21,A22,TARSKI:def 4;
end;
thus S is_antisymmetric_in X
proof let x,y; assume
A23: x in X & y in X & [x,y] in S & [y,x] in S;
then consider X1 such that
A24: [x,y] in X1 & X1 in Z by TARSKI:def 4;
consider X2 such that
A25: [y,x] in X2 & X2 in Z by A23,TARSKI:def 4;
X1,X2 are_c=-comparable by A5,A24,A25,ORDINAL1:def 9;
then A26: X1 c= X2 or X2 c= X1 by XBOOLE_0:def 9;
consider P1 being Relation such that
A27: X1 = P1 & R c= P1 & P1 partially_orders X & field P1 = X by A2,A4
,A24;
consider P2 being Relation such that
A28: X2 = P2 & R c= P2 & P2 partially_orders X & field P2 = X by A2,A4
,A25;
P1 is_antisymmetric_in X & P2 is_antisymmetric_in X by A27,A28,Def5
;
hence thesis by A23,A24,A25,A26,A27,A28,RELAT_2:def 4;
end;
end;
hence thesis by A2,A6,A9,A10;
end;
then consider Y such that
A29: Y in Rel & for Z st Z in Rel & Z <> Y holds not Y c= Z by A3,Th79;
consider P such that
A30: Y = P & R c= P & P partially_orders X & field P = X by A2,A29;
take P; thus R c= P by A30;
thus
A31: P is_reflexive_in X & P is_transitive_in X & P is_antisymmetric_in X
by A30,Def5;
thus P is_connected_in X
proof let x,y such that
A32: x in X & y in X & x <> y & not [x,y] in P & not [y,x] in P;
defpred Q[set,set] means
[$1,$2] in P or [$1,x] in P & [y,$2] in P;
consider Q being Relation such that
A33: [z,u] in Q iff z in X & u in X & Q[z,u]
from Rel_Existence;
A34: P c= Q
proof let z,u; assume
A35: [z,u] in P;
then z in field P & u in field P by RELAT_1:30;
hence thesis by A30,A33,A35;
end;
then A36: R c= Q by A30,XBOOLE_1:1;
A37: Q c= [:X,X:]
proof let x; assume
A38: x in Q;
then consider y,z such that
A39: x = [y,z] by RELAT_1:def 1;
y in X & z in X by A33,A38,A39;
hence thesis by A39,ZFMISC_1:106;
end;
A40: field Q = X
proof
thus field Q c= X
proof let z; assume
z in field Q;
then A41: z in dom Q \/ rng Q by RELAT_1:def 6;
A42: now assume z in dom Q;
then ex u st [z,u] in Q by RELAT_1:def 4;
hence z in X by A33;
end;
now assume z in rng Q;
then ex u st [u,z] in Q by RELAT_1:def 5;
hence z in X by A33;
end;
hence thesis by A41,A42,XBOOLE_0:def 2;
end;
thus X c= field Q by A30,A34,RELAT_1:31;
end;
Q partially_orders X
proof
thus Q is_reflexive_in X
proof let z; assume
A43: z in X;
then [z,z] in P by A31,RELAT_2:def 1;
hence [z,z] in Q by A33,A43;
end;
thus Q is_transitive_in X
proof let a,b,c be set; assume
A44: a in X & b in X & c in X & [a,b] in Q & [b,c] in Q;
then ([a,b] in P or [a,x] in P & [y,b] in P) &
([b,c] in P or [b,x] in P & [y,c] in P) by A33;
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 A31,A32,A44,RELAT_2:def 8;
hence [a,c] in Q by A32,A33,A44;
end;
thus Q is_antisymmetric_in X
proof let a,b be set; assume
A45: a in X & b in X & [a,b] in Q & [b,a] in Q;
then ([a,b] in P or [a,x] in P & [y,b] in P) &
([b,a] in P or [b,x] in P & [y,a] in P) by A33;
then a = b or [a,x] in P & [y,a] in P or [y,x] in P
by A31,A32,A45,RELAT_2:def 4,def 8;
hence a = b by A31,A32,A45,RELAT_2:def 8;
end;
end;
then Q in Rel by A2,A36,A37,A40;
then A46: Q = P by A29,A30,A34;
[x,x] in P & [y,y] in P & x in X & y in X by A31,A32,RELAT_2:def 1;
hence contradiction by A32,A33,A46;
end;
thus field P = X by A30;
end;
::
:: Auxiliary theorems.
::
theorem
R c= [:field R,field R:] by Lm2;
theorem
R is reflexive & X c= field R implies field(R|_2 X) = X by Lm3;
theorem
R is_reflexive_in X implies R|_2 X is reflexive by Lm4;
theorem
R is_transitive_in X implies R|_2 X is transitive by Lm5;
theorem
R is_antisymmetric_in X implies R|_2 X is antisymmetric by Lm6;
theorem
R is_connected_in X implies R|_2 X is connected by Lm7;
theorem
R is_connected_in X & Y c= X implies R is_connected_in Y by Lm8;
theorem
R well_orders X & Y c= X implies R well_orders Y by Lm15;
theorem
R is connected implies R~ is connected by Lm1;
theorem
R is_reflexive_in X implies R~ is_reflexive_in X by Lm9;
theorem
R is_transitive_in X implies R~ is_transitive_in X by Lm10;
theorem
R is_antisymmetric_in X implies R~ is_antisymmetric_in X by Lm11;
theorem
R is_connected_in X implies R~ is_connected_in X by Lm12;
theorem
(R|_2 X)~ = R~|_2 X by Lm13;
theorem
R|_2 {} = {} by Lm14;