let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y) st G is independent holds
for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
let G be Subset of (PARTITIONS Y); :: thesis: ( G is independent implies for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) )
assume A1:
G is independent
; :: thesis: for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
let P, Q be Subset of (PARTITIONS Y); :: thesis: ( P c= G & Q c= G implies (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) )
assume that
A2:
P c= G
and
A3:
Q c= G
; :: thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
per cases
( P = {} or Q = {} or ( P <> {} & Q <> {} ) )
;
suppose A8:
(
P <> {} &
Q <> {} )
;
:: thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))let x,
y be
Element of
Y;
:: according to RELSET_1:def 2 :: thesis: ( not [x,y] in (ERl ('/\' P)) * (ERl ('/\' Q)) or [x,y] in (ERl ('/\' Q)) * (ERl ('/\' P)) )assume
[x,y] in (ERl ('/\' P)) * (ERl ('/\' Q))
;
:: thesis: [x,y] in (ERl ('/\' Q)) * (ERl ('/\' P))then consider z being
Element of
Y such that A9:
[x,z] in ERl ('/\' P)
and A10:
[z,y] in ERl ('/\' Q)
by RELSET_1:51;
consider A being
Subset of
Y such that A11:
A in '/\' P
and A12:
x in A
and A13:
z in A
by A9, PARTIT1:def 6;
consider B being
Subset of
Y such that A14:
B in '/\' Q
and A15:
z in B
and A16:
y in B
by A10, PARTIT1:def 6;
consider hP being
Function,
FP being
Subset-Family of
Y such that A17:
dom hP = P
and A18:
rng hP = FP
and A19:
for
d being
set st
d in P holds
hP . d in d
and A20:
A = Intersect FP
and
A <> {}
by A11, BVFUNC_2:def 1;
consider hQ being
Function,
FQ being
Subset-Family of
Y such that A21:
dom hQ = Q
and A22:
rng hQ = FQ
and A23:
for
d being
set st
d in Q holds
hQ . d in d
and A24:
B = Intersect FQ
and
B <> {}
by A14, BVFUNC_2:def 1;
reconsider P =
P,
Q =
Q as non
empty Subset of
(PARTITIONS Y) by A8;
deffunc H1(
Element of
P)
-> Element of $1 =
EqClass y,$1;
consider hP' being
Function of
P,
(bool Y) such that A25:
for
p being
Element of
P holds
hP' . p = H1(
p)
from FUNCT_2:sch 4();
A26:
for
d being
set st
d in P holds
hP' . d in d
deffunc H2(
Element of
Q)
-> Element of $1 =
EqClass x,$1;
consider hQ' being
Function of
Q,
(bool Y) such that A27:
for
p being
Element of
Q holds
hQ' . p = H2(
p)
from FUNCT_2:sch 4();
A28:
for
d being
set st
d in Q holds
hQ' . d in d
reconsider FP' =
rng hP',
FQ' =
rng hQ' as
Subset-Family of
Y ;
set A' =
Intersect FP';
set B' =
Intersect FQ';
A29:
dom hP' = P
by FUNCT_2:def 1;
for
a being
set st
a in FP' holds
y in a
then A32:
y in Intersect FP'
by SETFAM_1:58;
A33:
dom hQ' = Q
by FUNCT_2:def 1;
for
a being
set st
a in FQ' holds
x in a
then A36:
x in Intersect FQ'
by SETFAM_1:58;
reconsider G' =
G as non
empty Subset of
(PARTITIONS Y) by A2, A8;
deffunc H3(
set )
-> set = $1;
A37:
for
d being
Element of
G' holds
bool Y meets H3(
d)
consider h' being
Function of
G',
(bool Y) such that A38:
for
d being
Element of
G' holds
h' . d in H3(
d)
from FUNCT_2:sch 11(A37);
set h =
(h' +* hP') +* hQ';
A39:
dom ((h' +* hP') +* hQ') =
(dom (h' +* hP')) \/ Q
by A33, FUNCT_4:def 1
.=
((dom h') \/ P) \/ Q
by A29, FUNCT_4:def 1
.=
(G \/ P) \/ Q
by FUNCT_2:def 1
.=
G \/ Q
by A2, XBOOLE_1:12
.=
G
by A3, XBOOLE_1:12
;
A40:
rng ((h' +* hP') +* hQ') c= (rng (h' +* hP')) \/ (rng hQ')
by FUNCT_4:18;
rng (h' +* hP') c= (rng h') \/ (rng hP')
by FUNCT_4:18;
then
rng (h' +* hP') c= bool Y
by XBOOLE_1:1;
then
(rng (h' +* hP')) \/ (rng hQ') c= bool Y
by XBOOLE_1:8;
then reconsider F =
rng ((h' +* hP') +* hQ') as
Subset-Family of
Y by A40, XBOOLE_1:1;
A41:
for
d being
set st
d in P holds
((h' +* hP') +* hQ') . d = hP' . d
proof
let d be
set ;
:: thesis: ( d in P implies ((h' +* hP') +* hQ') . d = hP' . d )
assume A42:
d in P
;
:: thesis: ((h' +* hP') +* hQ') . d = hP' . d
then reconsider d' =
d as
Element of
P ;
per cases
( d in Q or not d in Q )
;
suppose A43:
d in Q
;
:: thesis: ((h' +* hP') +* hQ') . d = hP' . dthen A44:
hQ . d in d
by A23;
A45:
hP . d in d
by A19, A42;
A46:
hP . d in FP
by A17, A18, A42, FUNCT_1:def 5;
then A47:
x in hP . d
by A12, A20, SETFAM_1:58;
A48:
z in hP . d
by A13, A20, A46, SETFAM_1:58;
A49:
hQ . d in FQ
by A21, A22, A43, FUNCT_1:def 5;
then A50:
y in hQ . d
by A16, A24, SETFAM_1:58;
A51:
z in hQ . d
by A15, A24, A49, SETFAM_1:58;
thus ((h' +* hP') +* hQ') . d =
hQ' . d
by A33, A43, FUNCT_4:14
.=
EqClass x,
d'
by A27, A43
.=
hP . d
by A45, A47, EQREL_1:def 8
.=
EqClass z,
d'
by A45, A48, EQREL_1:def 8
.=
hQ . d
by A44, A51, EQREL_1:def 8
.=
EqClass y,
d'
by A44, A50, EQREL_1:def 8
.=
hP' . d
by A25
;
:: thesis: verum end;
end;
for
d being
set st
d in G holds
((h' +* hP') +* hQ') . d in d
then
Intersect F <> {}
by A1, A39, BVFUNC_2:def 5;
then consider t being
Element of
Y such that A59:
t in Intersect F
by SUBSET_1:10;
for
a being
set st
a in FP' holds
t in a
then A62:
t in Intersect FP'
by SETFAM_1:58;
for
a being
set st
a in FQ' holds
t in a
then A65:
t in Intersect FQ'
by SETFAM_1:58;
then
Intersect FQ' in '/\' Q
by A28, A33, BVFUNC_2:def 1;
then A66:
[x,t] in ERl ('/\' Q)
by A36, A65, PARTIT1:def 6;
Intersect FP' in '/\' P
by A26, A29, A62, BVFUNC_2:def 1;
then
[t,y] in ERl ('/\' P)
by A32, A62, PARTIT1:def 6;
hence
[x,y] in (ERl ('/\' Q)) * (ERl ('/\' P))
by A66, RELSET_1:51;
:: thesis: verum end;