let T be 1-sorted ; for F being finite Subset-Family of T
for F1 being Subset-Family of T st F is Cover of T & F1 = F \ { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } holds
F1 is Cover of T
let F be finite Subset-Family of T; for F1 being Subset-Family of T st F is Cover of T & F1 = F \ { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } holds
F1 is Cover of T
let F1 be Subset-Family of T; ( F is Cover of T & F1 = F \ { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } implies F1 is Cover of T )
assume that
A1:
the carrier of T c= union F
and
A2:
F1 = F \ { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) }
; SETFAM_1:def 11 F1 is Cover of T
set ZAW = { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } ;
thus
the carrier of T c= union F1
SETFAM_1:def 11 verumproof
let t be
object ;
TARSKI:def 3 ( not t in the carrier of T or t in union F1 )
assume
t in the
carrier of
T
;
t in union F1
then consider Z being
set such that A3:
t in Z
and A4:
Z in F
by A1, TARSKI:def 4;
set ALL =
{ X where X is Subset of T : ( Z c< X & X in F ) } ;
per cases
( { X where X is Subset of T : ( Z c< X & X in F ) } is empty or not { X where X is Subset of T : ( Z c< X & X in F ) } is empty )
;
suppose
not
{ X where X is Subset of T : ( Z c< X & X in F ) } is
empty
;
t in union F1then consider w being
object such that A9:
w in { X where X is Subset of T : ( Z c< X & X in F ) }
;
consider R being
Relation of
{ X where X is Subset of T : ( Z c< X & X in F ) } such that A10:
for
x,
y being
set holds
(
[x,y] in R iff (
x in { X where X is Subset of T : ( Z c< X & X in F ) } &
y in { X where X is Subset of T : ( Z c< X & X in F ) } &
S1[
x,
y] ) )
from RELSET_1:sch 5();
A11:
R is_reflexive_in { X where X is Subset of T : ( Z c< X & X in F ) }
by A10;
then A12:
field R = { X where X is Subset of T : ( Z c< X & X in F ) }
by ORDERS_1:13;
A13:
R partially_orders { X where X is Subset of T : ( Z c< X & X in F ) }
proof
thus
R is_reflexive_in { X where X is Subset of T : ( Z c< X & X in F ) }
by A11;
ORDERS_1:def 8 ( R is_transitive_in { X where X is Subset of T : ( Z c< X & X in F ) } & R is_antisymmetric_in { X where X is Subset of T : ( Z c< X & X in F ) } )
thus
R is_transitive_in { X where X is Subset of T : ( Z c< X & X in F ) }
R is_antisymmetric_in { X where X is Subset of T : ( Z c< X & X in F ) } proof
let x,
y,
z be
object ;
RELAT_2:def 8 ( not x in { X where X is Subset of T : ( Z c< X & X in F ) } or not y in { X where X is Subset of T : ( Z c< X & X in F ) } or not z in { X where X is Subset of T : ( Z c< X & X in F ) } or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that A14:
x in { X where X is Subset of T : ( Z c< X & X in F ) }
and
y in { X where X is Subset of T : ( Z c< X & X in F ) }
and A15:
z in { X where X is Subset of T : ( Z c< X & X in F ) }
;
( not [x,y] in R or not [y,z] in R or [x,z] in R )
assume A16:
(
[x,y] in R &
[y,z] in R )
;
[x,z] in R
reconsider x =
x,
y =
y,
z =
z as
set by TARSKI:1;
(
x c= y &
y c= z )
by A10, A16;
then
x c= z
;
hence
[x,z] in R
by A10, A14, A15;
verum
end;
let x,
y be
object ;
RELAT_2:def 4 ( not x in { X where X is Subset of T : ( Z c< X & X in F ) } or not y in { X where X is Subset of T : ( Z c< X & X in F ) } or not [x,y] in R or not [y,x] in R or x = y )
assume that
x in { X where X is Subset of T : ( Z c< X & X in F ) }
and
y in { X where X is Subset of T : ( Z c< X & X in F ) }
;
( not [x,y] in R or not [y,x] in R or x = y )
assume A17:
(
[x,y] in R &
[y,x] in R )
;
x = y
reconsider x =
x,
y =
y as
set by TARSKI:1;
(
x c= y &
y c= x )
by A10, A17;
hence
x = y
by XBOOLE_0:def 10;
verum
end; A18:
R is
reflexive
by A11, A12;
{ X where X is Subset of T : ( Z c< X & X in F ) } has_upper_Zorn_property_wrt R
proof
let Y be
set ;
ORDERS_1:def 10 ( not Y c= { X where X is Subset of T : ( Z c< X & X in F ) } or not R |_2 Y is being_linear-order or ex b1 being set st
( b1 in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b2 being set holds
( not b2 in Y or [b2,b1] in R ) ) ) )
assume that A19:
Y c= { X where X is Subset of T : ( Z c< X & X in F ) }
and A20:
R |_2 Y is
being_linear-order
;
ex b1 being set st
( b1 in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b2 being set holds
( not b2 in Y or [b2,b1] in R ) ) )
per cases
( not Y is empty or Y is empty )
;
suppose A21:
not
Y is
empty
;
ex b1 being set st
( b1 in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b2 being set holds
( not b2 in Y or [b2,b1] in R ) ) )defpred S2[
set ]
means ( not $1 is
empty & $1
c= Y implies
union $1
in Y );
take
union Y
;
( union Y in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b1 being set holds
( not b1 in Y or [b1,(union Y)] in R ) ) )A22:
S2[
{} ]
;
A23:
for
A,
B being
set st
A in Y &
B in Y holds
A \/ B in Y
A27:
for
x,
B being
set st
x in Y &
B c= Y &
S2[
B] holds
S2[
B \/ {x}]
consider y being
object such that A31:
y in Y
by A21;
y in { X where X is Subset of T : ( Z c< X & X in F ) }
by A19, A31;
then consider X being
Subset of
T such that A32:
X = y
and A33:
Z c< X
and
X in F
;
A34:
X c= union Y
by A31, A32, ZFMISC_1:74;
then A35:
Z <> union Y
by A33, XBOOLE_0:def 8;
Z c= X
by A33;
then
Z c= union Y
by A34;
then A36:
Z c< union Y
by A35;
A37:
{ X where X is Subset of T : ( Z c< X & X in F ) } c= F
then A38:
Y c= F
by A19;
A39:
Y is
finite
by A19, A37;
S2[
Y]
from FINSET_1:sch 2(A39, A22, A27);
then
union Y in F
by A21, A38;
hence A40:
union Y in { X where X is Subset of T : ( Z c< X & X in F ) }
by A36;
for b1 being set holds
( not b1 in Y or [b1,(union Y)] in R )let z be
set ;
( not z in Y or [z,(union Y)] in R )assume A41:
z in Y
;
[z,(union Y)] in Rthen
S1[
z,
union Y]
by ZFMISC_1:74;
hence
[z,(union Y)] in R
by A10, A19, A40, A41;
verum end; suppose A42:
Y is
empty
;
ex b1 being set st
( b1 in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b2 being set holds
( not b2 in Y or [b2,b1] in R ) ) )reconsider w =
w as
set by TARSKI:1;
take
w
;
( w in { X where X is Subset of T : ( Z c< X & X in F ) } & ( for b1 being set holds
( not b1 in Y or [b1,w] in R ) ) )thus
w in { X where X is Subset of T : ( Z c< X & X in F ) }
by A9;
for b1 being set holds
( not b1 in Y or [b1,w] in R )thus
for
b1 being
set holds
( not
b1 in Y or
[b1,w] in R )
by A42;
verum end; end;
end; then consider M being
set such that A43:
M is_maximal_in R
by A12, A13, ORDERS_1:63;
A44:
M in field R
by A43;
then A45:
ex
X being
Subset of
T st
(
X = M &
Z c< X &
X in F )
by A12;
now not M in { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) } assume
M in { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c< Y ) ) }
;
contradictionthen consider H being
Subset of
T such that A46:
M = H
and
H in F
and A47:
ex
Y being
Subset of
T st
(
Y in F &
H c< Y )
;
consider Y being
Subset of
T such that A48:
Y in F
and A49:
H c< Y
by A47;
Z c< Y
by A45, A46, A49, XBOOLE_1:56;
then A50:
Y in { X where X is Subset of T : ( Z c< X & X in F ) }
by A48;
H c= Y
by A49;
then
[M,Y] in R
by A10, A12, A44, A46, A50;
hence
contradiction
by A12, A43, A46, A49, A50;
verum end; then A51:
M in F1
by A2, A45, XBOOLE_0:def 5;
Z c= M
by A45;
hence
t in union F1
by A3, A51, TARSKI:def 4;
verum end; end;
end;