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 A6:
[x,y] in ERl (PA '\/' PB)
;
[x,y] in (ERl PA) "\/" (ERl PB)
consider p0 being
Subset of
Y such that A7:
p0 in PA '\/' PB
and A8:
x in p0
and A9:
y in p0
by A6, Def6;
A10:
p0 is_min_depend PA,
PB
by A7, Def5;
A11:
p0 is_a_dependent_set_of PA
by A10, 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;
A18:
fx . (len fx) in a
by A15, A17, FINSEQ_1:57;
A19:
( 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;
A20:
a in Ca
by A13, A16, A17, A18, A19;
consider y5 being
set such that A21:
x in y5
and A22:
y5 in Ca
by A15, A20;
consider z5 being
set such that A23:
x9 in z5
and A24:
z5 in PB
by A4, TARSKI:def 4;
A25:
y5 /\ z5 <> {}
by A21, A23, XBOOLE_0:def 4;
A26:
z5 in Cb
by A22, A24, A25;
A27:
Ca c= PA
A30:
pb is_a_dependent_set_of PA
by A20, A27, Def1;
A31:
pb c= union Cb
proof
let x1 be
set ;
TARSKI:def 3 ( not x1 in pb or x1 in union Cb )
assume A32:
x1 in pb
;
x1 in union Cb
consider y being
set such that A33:
x1 in y
and A34:
y in Ca
by A32, TARSKI:def 4;
A35:
ex
p being
Element of
PA st
(
y = p & 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 ) ) ) )
by A34;
consider z being
set such that A36:
x1 in z
and A37:
z in PB
by A4, A33, A35, TARSKI:def 4;
A38:
y /\ z <> {}
by A33, A36, XBOOLE_0:def 4;
A39:
z in Cb
by A34, A37, A38;
thus
x1 in union Cb
by A36, A39, TARSKI:def 4;
verum
end;
A40:
union Cb c= pb
proof
let x1 be
set ;
TARSKI:def 3 ( not x1 in union Cb or x1 in pb )
assume A41:
x1 in union Cb
;
x1 in pb
consider y1 being
set such that A42:
x1 in y1
and A43:
y1 in Cb
by A41, 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;
consider q being
set such that A45:
q in Ca
and A46:
y1 /\ q <> {}
by A44;
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;
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 )
by A49;
reconsider x1 =
x1 as
Element of
Y by A42, A44;
reconsider f =
fd ^ <*x1*> as
FinSequence of
Y ;
A54:
len f = (len fd) + (len <*x1*>)
by FINSEQ_1:35;
A55:
len f = (len fd) + 1
by A54, FINSEQ_1:57;
A56:
1
+ 1
<= (len fd) + 1
by A50, XREAL_1:8;
A57:
1
<= len f
by A55, A56, XXREAL_0:2;
A58:
f . ((len fd) + 1) in y1
by A42, FINSEQ_1:59;
A59:
y1 meets q
by A46, XBOOLE_0:def 7;
consider z0 being
set such that A60:
(
z0 in y1 &
z0 in q )
by A59, 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
A66:
(
(fd ^ <*x1*>) . ((len fd) + 1) = x1 &
f . 1
= x )
by A50, A51, A63, 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 )
proof
let i be
Element of
NAT ;
( 1 <= i & i < len fd implies 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 ) )
assume A69:
( 1
<= i &
i < len fd )
;
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 )
A70:
f . i = fd . i
by A63, A69;
A71:
( 1
<= i + 1 &
i + 1
<= len fd )
by A69, NAT_1:13;
A72:
f . (i + 1) = fd . (i + 1)
by A63, A71;
thus
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 A53, A69, A70, A72;
verum
end;
A73:
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 )
A80:
pd in Ca
by A47, A48, A55, A57, A66, A73;
thus
x1 in pb
by A47, A80, TARSKI:def 4;
verum
end;
A81:
pb = union Cb
by A31, A40, XBOOLE_0:def 10;
A82:
Cb c= PB
A85:
pb is_a_dependent_set_of PB
by A26, A81, A82, Def1;
A86:
now assume A87:
not
pb c= p0
;
contradictionA88:
pb \ p0 <> {}
by A87, XBOOLE_1:37;
consider x1 being
set such that A89:
x1 in pb \ p0
by A88, 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;
consider q being
set such that A94:
q in Ca
and A95:
y1 /\ q <> {}
by A93;
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;
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 )
by A96;
reconsider x1 =
x1 as
Element of
Y by A91, A93;
reconsider f =
fd ^ <*x1*> as
FinSequence of
Y ;
A101:
len f = (len fd) + (len <*x1*>)
by FINSEQ_1:35;
A102:
len f = (len fd) + 1
by A101, FINSEQ_1:57;
A103:
1
+ 1
<= (len fd) + 1
by A97, XREAL_1:8;
A104:
1
<= len f
by A102, A103, XXREAL_0:2;
A105:
f . ((len fd) + 1) in y1
by A91, FINSEQ_1:59;
A106:
y1 meets q
by A95, XBOOLE_0:def 7;
consider z0 being
set such that A107:
(
z0 in y1 &
z0 in q )
by A106, 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
A113:
(
(fd ^ <*x1*>) . ((len fd) + 1) = x1 &
f . 1
= x )
by A97, A98, A110, 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 )
proof
let i be
Element of
NAT ;
( 1 <= i & i < len fd implies 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 ) )
assume A116:
( 1
<= i &
i < len fd )
;
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 )
A117:
f . i = fd . i
by A110, A116;
A118:
( 1
<= i + 1 &
i + 1
<= len fd )
by A116, NAT_1:13;
A119:
f . (i + 1) = fd . (i + 1)
by A110, A118;
thus
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 A100, A116, A117, A119;
verum
end; 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 )
A127:
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 A128:
( 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 )
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, A128;
A132:
(
x0 in p1 &
x0 in p2 )
by A130, XBOOLE_0:def 4;
thus
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, A132;
verum
end; thus
contradiction
by A8, A11, A12, A90, A102, A104, A113, A127, Th25;
verum end;
A133:
y in pb
by A9, A10, A30, A85, A86, Def2;
consider y1 being
set such that A134:
y in y1
and A135:
y1 in Cb
by A31, A133, 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;
consider q being
set such that A137:
q in Ca
and A138:
y1 /\ q <> {}
by A136;
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;
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 )
by A139;
reconsider y9 =
y as
Element of
Y by A9;
reconsider f =
fd ^ <*y9*> as
FinSequence of
Y ;
A144:
len f = (len fd) + (len <*y9*>)
by FINSEQ_1:35;
A145:
len f = (len fd) + 1
by A144, FINSEQ_1:57;
A146:
1
+ 1
<= len f
by A140, A145, XREAL_1:8;
A147:
f . ((len fd) + 1) in y1
by A134, FINSEQ_1:59;
A148:
y1 meets q
by A138, XBOOLE_0:def 7;
consider z0 being
set such that A149:
(
z0 in y1 &
z0 in q )
by A148, 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
A155:
f . (len fd) in q
by A140, A142, A152;
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 )
proof
let i be
Element of
NAT ;
( 1 <= i & i < len fd implies 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 ) )
assume A157:
( 1
<= i &
i < len fd )
;
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 )
A158:
f . i = fd . i
by A152, A157;
A159:
( 1
<= i + 1 &
i + 1
<= len fd )
by A157, NAT_1:13;
A160:
f . (i + 1) = fd . (i + 1)
by A152, A159;
thus
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 A143, A157, A158, A160;
verum
end;
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;
A170:
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 A171:
( 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) )
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, A171;
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;
A181:
(
ERl PA c= (ERl PA) \/ (ERl PB) &
ERl PB c= (ERl PA) \/ (ERl PB) )
by XBOOLE_1:7;
thus
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, A181;
verum
end;
A182:
[x9,y9] in (ERl PA) "\/" (ERl PB)
by A145, A168, A169, A170, Th26;
thus
[x,y] in (ERl PA) "\/" (ERl PB)
by A182;
verum
end;
A183:
for x1, x2 being set st [x1,x2] in (ERl PA) \/ (ERl PB) holds
[x1,x2] in ERl (PA '\/' PB)
proof
let x1,
x2 be
set ;
( [x1,x2] in (ERl PA) \/ (ERl PB) implies [x1,x2] in ERl (PA '\/' PB) )
assume A184:
[x1,x2] in (ERl PA) \/ (ERl PB)
;
[x1,x2] in ERl (PA '\/' PB)
A185:
(
[x1,x2] in ERl PA or
[x1,x2] in ERl PB )
by A184, XBOOLE_0:def 3;
A186:
( ex
A being
Subset of
Y st
(
A in PA &
x1 in A &
x2 in A ) or ex
B being
Subset of
Y st
(
B in PB &
x1 in B &
x2 in B ) )
by A185, Def6;
thus
[x1,x2] in ERl (PA '\/' PB)
by A187;
verum
end;
A196:
(ERl PA) \/ (ERl PB) c= ERl (PA '\/' PB)
by A183, RELAT_1:def 3;
A197:
(ERl PA) "\/" (ERl PB) c= ERl (PA '\/' PB)
by A196, EQREL_1:def 3;
thus
ERl (PA '\/' PB) = (ERl PA) "\/" (ERl PB)
by A5, A197, XBOOLE_0:def 10; verum