let Y be non empty set ; for PA, PB being a_partition of Y holds ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB)
let PA, PB be a_partition of Y; ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB)
A1:
PA is_finer_than PA '\/' PB
by Th19;
A2:
PB is_finer_than PA '\/' PB
by Th19;
A3:
union PA = Y
by EQREL_1:def 6;
A4:
union PB = Y
by EQREL_1:def 6;
A5:
ERl (PA '\/' PB) c= (ERl PA) "\/" (ERl PB)
proof
let x,
y be
set ;
RELAT_1:def 3 ( not [x,y] in ERl (PA '\/' PB) or [x,y] in (ERl PA) "\/" (ERl PB) )
assume
[x,y] in ERl (PA '\/' PB)
;
[x,y] in (ERl PA) "\/" (ERl PB)
then consider p0 being
Subset of
Y such that A7:
p0 in PA '\/' PB
and A8:
x in p0
and A9:
y in p0
by Def6;
A10:
p0 is_min_depend PA,
PB
by A7, Def5;
then A11:
p0 is_a_dependent_set_of PA
by Def2;
A12:
p0 is_a_dependent_set_of PB
by A10, Def2;
consider A1 being
set such that A13:
A1 c= PA
and
A1 <> {}
and A14:
p0 = union A1
by A11, Def1;
consider a being
set such that A15:
x in a
and A16:
a in A1
by A8, A14, TARSKI:def 4;
reconsider Ca =
{ p where p is Element of PA : ex f being FinSequence of Y st
( 1 <= len f & f . 1 = x & f . (len f) in p & ( for i being Element of NAT st 1 <= i & i < len f holds
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 /\ p2 & f . (i + 1) in p2 ) ) ) } as
set ;
reconsider pb =
union Ca as
set ;
reconsider Cb =
{ p where p is Element of PB : ex q being set st
( q in Ca & p /\ q <> {} ) } as
set ;
reconsider x9 =
x as
Element of
Y by A8;
reconsider fx =
<*x9*> as
FinSequence of
Y ;
A17:
fx . 1
= x
by FINSEQ_1:def 8;
then A18:
fx . (len fx) in a
by A15, FINSEQ_1:57;
( 1
<= len fx & ( for
i being
Element of
NAT st 1
<= i &
i < len fx holds
ex
p1,
p2,
x0 being
set st
(
p1 in PA &
p2 in PB &
fx . i in p1 &
x0 in p1 /\ p2 &
fx . (i + 1) in p2 ) ) )
by FINSEQ_1:57;
then A20:
a in Ca
by A13, A16, A17, A18;
then consider y5 being
set such that A21:
x in y5
and A22:
y5 in Ca
by A15;
consider z5 being
set such that A23:
x9 in z5
and A24:
z5 in PB
by A4, TARSKI:def 4;
y5 /\ z5 <> {}
by A21, A23, XBOOLE_0:def 4;
then A26:
z5 in Cb
by A22, A24;
Ca c= PA
then A30:
pb is_a_dependent_set_of PA
by A20, Def1;
A31:
pb c= union Cb
union Cb c= pb
proof
let x1 be
set ;
TARSKI:def 3 ( not x1 in union Cb or x1 in pb )
assume
x1 in union Cb
;
x1 in pb
then consider y1 being
set such that A42:
x1 in y1
and A43:
y1 in Cb
by TARSKI:def 4;
A44:
ex
p being
Element of
PB st
(
y1 = p & ex
q being
set st
(
q in Ca &
p /\ q <> {} ) )
by A43;
then consider q being
set such that A45:
q in Ca
and A46:
y1 /\ q <> {}
;
consider pd being
set such that A47:
x1 in pd
and A48:
pd in PA
by A3, A42, A44, TARSKI:def 4;
A49:
ex
pp being
Element of
PA st
(
q = pp & ex
f being
FinSequence of
Y st
( 1
<= len f &
f . 1
= x &
f . (len f) in pp & ( for
i being
Element of
NAT st 1
<= i &
i < len f holds
ex
p1,
p2,
x0 being
set st
(
p1 in PA &
p2 in PB &
f . i in p1 &
x0 in p1 /\ p2 &
f . (i + 1) in p2 ) ) ) )
by A45;
then consider fd being
FinSequence of
Y such that A50:
1
<= len fd
and A51:
fd . 1
= x
and A52:
fd . (len fd) in q
and A53:
for
i being
Element of
NAT st 1
<= i &
i < len fd holds
ex
p1,
p2,
x0 being
set st
(
p1 in PA &
p2 in PB &
fd . i in p1 &
x0 in p1 /\ p2 &
fd . (i + 1) in p2 )
;
reconsider x1 =
x1 as
Element of
Y by A42, A44;
reconsider f =
fd ^ <*x1*> as
FinSequence of
Y ;
len f = (len fd) + (len <*x1*>)
by FINSEQ_1:35;
then A55:
len f = (len fd) + 1
by FINSEQ_1:57;
1
+ 1
<= (len fd) + 1
by A50, XREAL_1:8;
then A57:
1
<= len f
by A55, XXREAL_0:2;
A58:
f . ((len fd) + 1) in y1
by A42, FINSEQ_1:59;
y1 meets q
by A46, XBOOLE_0:def 7;
then consider z0 being
set such that A60:
(
z0 in y1 &
z0 in q )
by XBOOLE_0:3;
A61:
z0 in y1 /\ q
by A60, XBOOLE_0:def 4;
A62:
dom fd = Seg (len fd)
by FINSEQ_1:def 3;
A63:
for
k being
Element of
NAT st 1
<= k &
k <= len fd holds
f . k = fd . k
then A66:
(
(fd ^ <*x1*>) . ((len fd) + 1) = x1 &
f . 1
= x )
by A50, A51, FINSEQ_1:59;
A67:
f . (len fd) in q
by A50, A52, A63;
A68:
for
i being
Element of
NAT st 1
<= i &
i < len fd holds
ex
p1,
p2,
x0 being
set st
(
p1 in PA &
p2 in PB &
f . i in p1 &
x0 in p1 /\ p2 &
f . (i + 1) in p2 )
for
i being
Element of
NAT st 1
<= i &
i < len f holds
ex
p1,
p2,
x0 being
set st
(
p1 in PA &
p2 in PB &
f . i in p1 &
x0 in p1 /\ p2 &
f . (i + 1) in p2 )
then
pd in Ca
by A47, A48, A55, A57, A66;
hence
x1 in pb
by A47, TARSKI:def 4;
verum
end;
then A81:
pb = union Cb
by A31, XBOOLE_0:def 10;
Cb c= PB
then A85:
pb is_a_dependent_set_of PB
by A26, A81, Def1;
now assume
not
pb c= p0
;
contradictionthen
pb \ p0 <> {}
by XBOOLE_1:37;
then consider x1 being
set such that A89:
x1 in pb \ p0
by XBOOLE_0:def 1;
A90:
not
x1 in p0
by A89, XBOOLE_0:def 5;
consider y1 being
set such that A91:
x1 in y1
and A92:
y1 in Cb
by A81, A89, TARSKI:def 4;
A93:
ex
p being
Element of
PB st
(
y1 = p & ex
q being
set st
(
q in Ca &
p /\ q <> {} ) )
by A92;
then consider q being
set such that A94:
q in Ca
and A95:
y1 /\ q <> {}
;
A96:
ex
pp being
Element of
PA st
(
q = pp & ex
f being
FinSequence of
Y st
( 1
<= len f &
f . 1
= x &
f . (len f) in pp & ( for
i being
Element of
NAT st 1
<= i &
i < len f holds
ex
p1,
p2,
x0 being
set st
(
p1 in PA &
p2 in PB &
f . i in p1 &
x0 in p1 /\ p2 &
f . (i + 1) in p2 ) ) ) )
by A94;
then consider fd being
FinSequence of
Y such that A97:
1
<= len fd
and A98:
fd . 1
= x
and A99:
fd . (len fd) in q
and A100:
for
i being
Element of
NAT st 1
<= i &
i < len fd holds
ex
p1,
p2,
x0 being
set st
(
p1 in PA &
p2 in PB &
fd . i in p1 &
x0 in p1 /\ p2 &
fd . (i + 1) in p2 )
;
reconsider x1 =
x1 as
Element of
Y by A91, A93;
reconsider f =
fd ^ <*x1*> as
FinSequence of
Y ;
len f = (len fd) + (len <*x1*>)
by FINSEQ_1:35;
then A102:
len f = (len fd) + 1
by FINSEQ_1:57;
1
+ 1
<= (len fd) + 1
by A97, XREAL_1:8;
then A104:
1
<= len f
by A102, XXREAL_0:2;
A105:
f . ((len fd) + 1) in y1
by A91, FINSEQ_1:59;
y1 meets q
by A95, XBOOLE_0:def 7;
then consider z0 being
set such that A107:
(
z0 in y1 &
z0 in q )
by XBOOLE_0:3;
A108:
z0 in y1 /\ q
by A107, XBOOLE_0:def 4;
A109:
dom fd = Seg (len fd)
by FINSEQ_1:def 3;
A110:
for
k being
Element of
NAT st 1
<= k &
k <= len fd holds
f . k = fd . k
then A113:
(
(fd ^ <*x1*>) . ((len fd) + 1) = x1 &
f . 1
= x )
by A97, A98, FINSEQ_1:59;
A114:
f . (len fd) in q
by A97, A99, A110;
A115:
for
i being
Element of
NAT st 1
<= i &
i < len fd holds
ex
p1,
p2,
x0 being
set st
(
p1 in PA &
p2 in PB &
f . i in p1 &
x0 in p1 /\ p2 &
f . (i + 1) in p2 )
A120:
for
i being
Element of
NAT st 1
<= i &
i < len f holds
ex
p1,
p2,
x0 being
set st
(
p1 in PA &
p2 in PB &
f . i in p1 &
x0 in p1 /\ p2 &
f . (i + 1) in p2 )
for
i being
Element of
NAT st 1
<= i &
i < len f holds
ex
p1,
p2,
x0 being
set st
(
p1 in PA &
p2 in PB &
f . i in p1 &
x0 in p1 &
x0 in p2 &
f . (i + 1) in p2 )
proof
let i be
Element of
NAT ;
( 1 <= i & i < len f implies ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 & x0 in p2 & f . (i + 1) in p2 ) )
assume
( 1
<= i &
i < len f )
;
ex p1, p2, x0 being set st
( p1 in PA & p2 in PB & f . i in p1 & x0 in p1 & x0 in p2 & f . (i + 1) in p2 )
then consider p1,
p2,
x0 being
set such that A129:
(
p1 in PA &
p2 in PB &
f . i in p1 )
and A130:
x0 in p1 /\ p2
and A131:
f . (i + 1) in p2
by A120;
(
x0 in p1 &
x0 in p2 )
by A130, XBOOLE_0:def 4;
hence
ex
p1,
p2,
x0 being
set st
(
p1 in PA &
p2 in PB &
f . i in p1 &
x0 in p1 &
x0 in p2 &
f . (i + 1) in p2 )
by A129, A131;
verum
end; hence
contradiction
by A8, A11, A12, A90, A102, A104, A113, Th25;
verum end;
then
y in pb
by A9, A10, A30, A85, Def2;
then consider y1 being
set such that A134:
y in y1
and A135:
y1 in Cb
by A31, TARSKI:def 4;
A136:
ex
p being
Element of
PB st
(
y1 = p & ex
q being
set st
(
q in Ca &
p /\ q <> {} ) )
by A135;
then consider q being
set such that A137:
q in Ca
and A138:
y1 /\ q <> {}
;
A139:
ex
pp being
Element of
PA st
(
q = pp & ex
f being
FinSequence of
Y st
( 1
<= len f &
f . 1
= x &
f . (len f) in pp & ( for
i being
Element of
NAT st 1
<= i &
i < len f holds
ex
p1,
p2,
x0 being
set st
(
p1 in PA &
p2 in PB &
f . i in p1 &
x0 in p1 /\ p2 &
f . (i + 1) in p2 ) ) ) )
by A137;
then consider fd being
FinSequence of
Y such that A140:
1
<= len fd
and A141:
fd . 1
= x
and A142:
fd . (len fd) in q
and A143:
for
i being
Element of
NAT st 1
<= i &
i < len fd holds
ex
p1,
p2,
x0 being
set st
(
p1 in PA &
p2 in PB &
fd . i in p1 &
x0 in p1 /\ p2 &
fd . (i + 1) in p2 )
;
reconsider y9 =
y as
Element of
Y by A9;
reconsider f =
fd ^ <*y9*> as
FinSequence of
Y ;
len f = (len fd) + (len <*y9*>)
by FINSEQ_1:35;
then A145:
len f = (len fd) + 1
by FINSEQ_1:57;
then A146:
1
+ 1
<= len f
by A140, XREAL_1:8;
A147:
f . ((len fd) + 1) in y1
by A134, FINSEQ_1:59;
y1 meets q
by A138, XBOOLE_0:def 7;
then consider z0 being
set such that A149:
(
z0 in y1 &
z0 in q )
by XBOOLE_0:3;
A150:
z0 in y1 /\ q
by A149, XBOOLE_0:def 4;
A151:
dom fd = Seg (len fd)
by FINSEQ_1:def 3;
A152:
for
k being
Element of
NAT st 1
<= k &
k <= len fd holds
f . k = fd . k
then A155:
f . (len fd) in q
by A140, A142;
A156:
for
i being
Element of
NAT st 1
<= i &
i < len fd holds
ex
p1,
p2,
x0 being
set st
(
p1 in PA &
p2 in PB &
f . i in p1 &
x0 in p1 /\ p2 &
f . (i + 1) in p2 )
A161:
for
i being
Element of
NAT st 1
<= i &
i < len f holds
ex
p1,
p2,
x0 being
set st
(
p1 in PA &
p2 in PB &
f . i in p1 &
x0 in p1 /\ p2 &
f . (i + 1) in p2 )
A168:
(
(fd ^ <*y9*>) . ((len fd) + 1) = y & 1
<= len f )
by A146, FINSEQ_1:59, XXREAL_0:2;
A169:
f . 1
= x
by A140, A141, A152;
for
i being
Element of
NAT st 1
<= i &
i < len f holds
ex
u being
set st
(
u in Y &
[(f . i),u] in (ERl PA) \/ (ERl PB) &
[u,(f . (i + 1))] in (ERl PA) \/ (ERl PB) )
proof
let i be
Element of
NAT ;
( 1 <= i & i < len f implies ex u being set st
( u in Y & [(f . i),u] in (ERl PA) \/ (ERl PB) & [u,(f . (i + 1))] in (ERl PA) \/ (ERl PB) ) )
assume
( 1
<= i &
i < len f )
;
ex u being set st
( u in Y & [(f . i),u] in (ERl PA) \/ (ERl PB) & [u,(f . (i + 1))] in (ERl PA) \/ (ERl PB) )
then consider p1,
p2,
u being
set such that A172:
p1 in PA
and A173:
p2 in PB
and A174:
f . i in p1
and A175:
u in p1 /\ p2
and A176:
f . (i + 1) in p2
by A161;
A177:
u in p1
by A175, XBOOLE_0:def 4;
A178:
u in p2
by A175, XBOOLE_0:def 4;
reconsider x2 =
f . i as
set ;
reconsider y2 =
f . (i + 1) as
set ;
A179:
[x2,u] in ERl PA
by A172, A174, A177, Def6;
A180:
[u,y2] in ERl PB
by A173, A176, A178, Def6;
(
ERl PA c= (ERl PA) \/ (ERl PB) &
ERl PB c= (ERl PA) \/ (ERl PB) )
by XBOOLE_1:7;
hence
ex
u being
set st
(
u in Y &
[(f . i),u] in (ERl PA) \/ (ERl PB) &
[u,(f . (i + 1))] in (ERl PA) \/ (ERl PB) )
by A172, A177, A179, A180;
verum
end;
then
[x9,y9] in (ERl PA) "\/" (ERl PB)
by A145, A168, A169, Th26;
hence
[x,y] in (ERl PA) "\/" (ERl PB)
;
verum
end;
for x1, x2 being set st [x1,x2] in (ERl PA) \/ (ERl PB) holds
[x1,x2] in ERl (PA '\/' PB)
then
(ERl PA) \/ (ERl PB) c= ERl (PA '\/' PB)
by RELAT_1:def 3;
then
(ERl PA) "\/" (ERl PB) c= ERl (PA '\/' PB)
by EQREL_1:def 3;
hence
ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB)
by A5, XBOOLE_0:def 10; verum