let Y be non empty set ; :: thesis: for PA, PB being a_partition of Y holds ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB)
let PA, PB be a_partition of Y; :: thesis: 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 & ( for A being set st A in PA holds
( A <> {} & ( for B being set holds
( not B in PA or A = B or A misses B ) ) ) ) )
by EQREL_1:def 6;
A4:
( union PB = Y & ( for A being set st A in PB holds
( A <> {} & ( for B being set holds
( not B in PB or A = B or A misses B ) ) ) ) )
by EQREL_1:def 6;
A5:
ERl (PA '\/' PB) c= (ERl PA) "\/" (ERl PB)
proof
let x,
y be
set ;
:: according to RELAT_1:def 3 :: thesis: ( not [x,y] in ERl (PA '\/' PB) or [x,y] in (ERl PA) "\/" (ERl PB) )
assume
[x,y] in ERl (PA '\/' PB)
;
:: thesis: [x,y] in (ERl PA) "\/" (ERl PB)
then consider p0 being
Subset of
Y such that A6:
(
p0 in PA '\/' PB &
x in p0 &
y in p0 )
by Def6;
A7:
p0 is_min_depend PA,
PB
by A6, Def5;
then A8:
(
p0 is_a_dependent_set_of PA &
p0 is_a_dependent_set_of PB & ( for
d being
set st
d c= p0 &
d is_a_dependent_set_of PA &
d is_a_dependent_set_of PB holds
d = p0 ) )
by Def2;
then consider A1 being
set such that A9:
(
A1 c= PA &
A1 <> {} &
p0 = union A1 )
by Def1;
consider a being
set such that A10:
(
x in a &
a in A1 )
by A6, A9, 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 x' =
x as
Element of
Y by A6;
reconsider fx =
<*x'*> as
FinSequence of
Y ;
A11:
fx . 1
= x
by FINSEQ_1:def 8;
then A12:
fx . (len fx) in a
by A10, FINSEQ_1:57;
A13:
1
<= len fx
by FINSEQ_1:57;
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 A14:
a in Ca
by A9, A10, A11, A12, A13;
then consider y5 being
set such that A15:
(
x in y5 &
y5 in Ca )
by A10;
consider z5 being
set such that A16:
(
x' in z5 &
z5 in PB )
by A4, TARSKI:def 4;
y5 /\ z5 <> {}
by A15, A16, XBOOLE_0:def 4;
then A17:
z5 in Cb
by A15, A16;
A18:
pb is_a_dependent_set_of PA
A19:
pb = union Cb
proof
A20:
pb c= union Cb
union Cb c= pb
proof
let x1 be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x1 in union Cb or x1 in pb )
assume
x1 in union Cb
;
:: thesis: x1 in pb
then consider y1 being
set such that A24:
(
x1 in y1 &
y1 in Cb )
by TARSKI:def 4;
consider p being
Element of
PB such that A25:
(
y1 = p & ex
q being
set st
(
q in Ca &
p /\ q <> {} ) )
by A24;
consider q being
set such that A26:
(
q in Ca &
y1 /\ q <> {} )
by A25;
consider pd being
set such that A27:
(
x1 in pd &
pd in PA )
by A3, A24, A25, TARSKI:def 4;
consider pp being
Element of
PA such that A28:
(
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 A26;
consider fd being
FinSequence of
Y such that A29:
( 1
<= len fd &
fd . 1
= x &
fd . (len fd) in q & ( 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 ) ) )
by A28;
reconsider x1 =
x1 as
Element of
Y by A24, A25;
reconsider f =
fd ^ <*x1*> as
FinSequence of
Y ;
len f = (len fd) + (len <*x1*>)
by FINSEQ_1:35;
then A30:
len f = (len fd) + 1
by FINSEQ_1:57;
1
+ 1
<= (len fd) + 1
by A29, XREAL_1:8;
then A31:
1
<= len f
by A30, XXREAL_0:2;
A32:
(fd ^ <*x1*>) . ((len fd) + 1) = x1
by FINSEQ_1:59;
A33:
f . ((len fd) + 1) in y1
by A24, FINSEQ_1:59;
y1 meets q
by A26, XBOOLE_0:def 7;
then consider z0 being
set such that A34:
(
z0 in y1 &
z0 in q )
by XBOOLE_0:3;
A35:
z0 in y1 /\ q
by A34, XBOOLE_0:def 4;
A36:
dom fd = Seg (len fd)
by FINSEQ_1:def 3;
A37:
for
k being
Element of
NAT st 1
<= k &
k <= len fd holds
f . k = fd . k
then A38:
f . 1
= x
by A29;
A39:
f . (len fd) in q
by A29, A37;
A40:
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 A27, A30, A31, A32, A38;
hence
x1 in pb
by A27, TARSKI:def 4;
:: thesis: verum
end;
hence
pb = union Cb
by A20, XBOOLE_0:def 10;
:: thesis: verum
end;
A44:
pb is_a_dependent_set_of PB
now assume
not
pb c= p0
;
:: thesis: contradictionthen
pb \ p0 <> {}
by XBOOLE_1:37;
then consider x1 being
set such that A45:
x1 in pb \ p0
by XBOOLE_0:def 1;
A46:
(
x1 in pb & not
x1 in p0 )
by A45, XBOOLE_0:def 5;
consider y1 being
set such that A47:
(
x1 in y1 &
y1 in Cb )
by A19, A45, TARSKI:def 4;
consider p being
Element of
PB such that A48:
(
y1 = p & ex
q being
set st
(
q in Ca &
p /\ q <> {} ) )
by A47;
consider q being
set such that A49:
(
q in Ca &
y1 /\ q <> {} )
by A48;
consider pp being
Element of
PA such that A50:
(
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 A49;
consider fd being
FinSequence of
Y such that A51:
( 1
<= len fd &
fd . 1
= x &
fd . (len fd) in q & ( 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 ) ) )
by A50;
reconsider x1 =
x1 as
Element of
Y by A47, A48;
reconsider f =
fd ^ <*x1*> as
FinSequence of
Y ;
len f = (len fd) + (len <*x1*>)
by FINSEQ_1:35;
then A52:
len f = (len fd) + 1
by FINSEQ_1:57;
1
+ 1
<= (len fd) + 1
by A51, XREAL_1:8;
then A53:
1
<= len f
by A52, XXREAL_0:2;
A54:
(fd ^ <*x1*>) . ((len fd) + 1) = x1
by FINSEQ_1:59;
A55:
f . ((len fd) + 1) in y1
by A47, FINSEQ_1:59;
y1 meets q
by A49, XBOOLE_0:def 7;
then consider z0 being
set such that A56:
(
z0 in y1 &
z0 in q )
by XBOOLE_0:3;
A57:
z0 in y1 /\ q
by A56, XBOOLE_0:def 4;
A58:
dom fd = Seg (len fd)
by FINSEQ_1:def 3;
A59:
for
k being
Element of
NAT st 1
<= k &
k <= len fd holds
f . k = fd . k
then A60:
f . 1
= x
by A51;
A61:
f . (len fd) in q
by A51, A59;
A62:
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 )
A65:
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 )
hence
contradiction
by A6, A8, A46, A52, A53, A54, A60, Th25;
:: thesis: verum end;
then
y in pb
by A6, A7, A18, A44, Def2;
then consider y1 being
set such that A68:
(
y in y1 &
y1 in Cb )
by A19, TARSKI:def 4;
consider p being
Element of
PB such that A69:
(
y1 = p & ex
q being
set st
(
q in Ca &
p /\ q <> {} ) )
by A68;
consider q being
set such that A70:
(
q in Ca &
y1 /\ q <> {} )
by A69;
consider pd being
set such that A71:
(
y in pd &
pd in PA )
by A3, A68, A69, TARSKI:def 4;
consider pp being
Element of
PA such that A72:
(
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 A70;
consider fd being
FinSequence of
Y such that A73:
( 1
<= len fd &
fd . 1
= x &
fd . (len fd) in q & ( 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 ) ) )
by A72;
reconsider y' =
y as
Element of
Y by A6;
reconsider f =
fd ^ <*y'*> as
FinSequence of
Y ;
A74:
len f = (len fd) + (len <*y'*>)
by FINSEQ_1:35;
then A75:
len f = (len fd) + 1
by FINSEQ_1:57;
then A76:
1
+ 1
<= len f
by A73, XREAL_1:8;
A77:
(fd ^ <*y'*>) . ((len fd) + 1) = y
by FINSEQ_1:59;
A78:
f . ((len fd) + 1) in y1
by A68, FINSEQ_1:59;
y1 meets q
by A70, XBOOLE_0:def 7;
then consider z0 being
set such that A79:
(
z0 in y1 &
z0 in q )
by XBOOLE_0:3;
A80:
z0 in y1 /\ q
by A79, XBOOLE_0:def 4;
A81:
dom fd = Seg (len fd)
by FINSEQ_1:def 3;
A82:
for
k being
Element of
NAT st 1
<= k &
k <= len fd holds
f . k = fd . k
then A83:
f . (len fd) in q
by A73;
A84:
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 )
A87:
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 A89:
( 1
<= len f &
f . 1
= x &
f . (len f) in pd & ( 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 A71, A73, A74, A76, A77, A82, FINSEQ_1:57, XXREAL_0:2;
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 ;
:: thesis: ( 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 )
;
:: thesis: 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 A90:
(
p1 in PA &
p2 in PB &
f . i in p1 &
u in p1 /\ p2 &
f . (i + 1) in p2 )
by A87;
A91:
(
p1 in PA &
p2 in PB &
f . i in p1 &
u in p1 &
u in p2 &
f . (i + 1) in p2 )
by A90, XBOOLE_0:def 4;
reconsider x2 =
f . i as
set ;
reconsider y2 =
f . (i + 1) as
set ;
A92:
[x2,u] in ERl PA
by A91, Def6;
A93:
[u,y2] in ERl PB
by A91, Def6;
A94:
ERl PA c= (ERl PA) \/ (ERl PB)
by XBOOLE_1:7;
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 A91, A92, A93, A94;
:: thesis: verum
end;
then
[x',y'] in (ERl PA) "\/" (ERl PB)
by A75, A77, A89, Th26;
hence
[x,y] in (ERl PA) "\/" (ERl PB)
;
:: thesis: 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; :: thesis: verum