let X be set ; for Y, Z being finite Subset-Family of X st Z c= Y holds
Components Y is_finer_than Components Z
let Y, Z be finite Subset-Family of X; ( Z c= Y implies Components Y is_finer_than Components Z )
assume A1:
Z c= Y
; Components Y is_finer_than Components Z
now for V being set st V in Components Y holds
ex W being set st
( W in Components Z & V c= W )let V be
set ;
( V in Components Y implies ex W being set st
( W in Components Z & V c= W ) )consider p being
FinSequence of
bool X such that A2:
len p = card Y
and A3:
rng p = Y
and A4:
Components Y = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p }
by Def2;
consider p1 being
FinSequence of
bool X such that
len p1 = card Z
and A5:
rng p1 = Z
and A6:
Components Z = { (Intersect (rng (MergeSequence (p1,q)))) where q is FinSequence of BOOLEAN : len q = len p1 }
by Def2;
A7:
p1 is
FinSequence of
rng p
by A1, A3, A5, FINSEQ_1:def 4;
assume
V in Components Y
;
ex W being set st
( W in Components Z & V c= W )then consider q being
FinSequence of
BOOLEAN such that A8:
V = Intersect (rng (MergeSequence (p,q)))
and A9:
len q = len p
by A4;
dom p = dom q
by A9, FINSEQ_3:29;
then A10:
q is
Function of
(dom p),
BOOLEAN
by FINSEQ_2:26;
A11:
p is
one-to-one
by A2, A3, FINSEQ_4:62;
then A12:
rng p1 c= dom (p ")
by A1, A3, A5, FUNCT_1:33;
rng (p ") =
dom p
by A11, FUNCT_1:33
.=
dom q
by A9, FINSEQ_3:29
;
then A13:
rng ((p ") * p1) c= dom q
by RELAT_1:26;
p is
Function of
(dom p),
(rng p)
by FUNCT_2:1;
then
p " is
Function of
(rng p),
(dom p)
by A11, FUNCT_2:25;
then
(p ") * p1 is
FinSequence of
dom p
by A7, FINSEQ_2:32;
then
q * ((p ") * p1) is
FinSequence of
BOOLEAN
by A10, FINSEQ_2:32;
then reconsider q1 =
(q * (p ")) * p1 as
FinSequence of
BOOLEAN by RELAT_1:36;
reconsider W =
Intersect (rng (MergeSequence (p1,q1))) as
set ;
take W =
W;
( W in Components Z & V c= W ) dom q1 =
dom (q * ((p ") * p1))
by RELAT_1:36
.=
dom ((p ") * p1)
by A13, RELAT_1:27
.=
dom p1
by A12, RELAT_1:27
;
then
len q1 = len p1
by FINSEQ_3:29;
hence
W in Components Z
by A6;
V c= W
rng (MergeSequence (p1,q1)) c= rng (MergeSequence (p,q))
proof
let z be
object ;
TARSKI:def 3 ( not z in rng (MergeSequence (p1,q1)) or z in rng (MergeSequence (p,q)) )
assume
z in rng (MergeSequence (p1,q1))
;
z in rng (MergeSequence (p,q))
then consider i being
Nat such that A14:
i in dom (MergeSequence (p1,q1))
and A15:
(MergeSequence (p1,q1)) . i = z
by FINSEQ_2:10;
A16:
i in dom p1
by A14, Th1;
then A17:
i in dom ((p ") * p1)
by A12, RELAT_1:27;
then
((p ") * p1) . i in rng ((p ") * p1)
by FUNCT_1:def 3;
then A18:
((p ") * p1) . i in rng (p ")
by FUNCT_1:14;
then A19:
((p ") * p1) . i in dom p
by A11, FUNCT_1:33;
then reconsider j =
((p ") * p1) . i as
Element of
NAT ;
A20:
q . j =
(q * ((p ") * p1)) . i
by A17, FUNCT_1:13
.=
q1 . i
by RELAT_1:36
;
A21:
p1 is
Function of
(dom p1),
(rng p)
by A1, A3, A5, FUNCT_2:2;
A22:
j in dom p
by A11, A18, FUNCT_1:33;
j in dom (MergeSequence (p,q))
by A19, Th1;
hence
z in rng (MergeSequence (p,q))
by A23, FUNCT_1:def 3;
verum
end; hence
V c= W
by A8, SETFAM_1:44;
verum end;
hence
Components Y is_finer_than Components Z
by SETFAM_1:def 2; verum