let Y be non empty set ; :: thesis: for G being Subset of ()
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J holds
CompF (A,G) = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J

let G be Subset of (); :: thesis: for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J holds
CompF (A,G) = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J

let A, B, C, D, E, F, J be a_partition of Y; :: thesis: ( G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J implies CompF (A,G) = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J )
assume that
A1: G = {A,B,C,D,E,F,J} and
A2: A <> B and
A3: A <> C and
A4: ( A <> D & A <> E ) and
A5: ( A <> F & A <> J ) and
A6: ( B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J ) ; :: thesis: CompF (A,G) = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
A7: G \ {A} = ({A} \/ {B,C,D,E,F,J}) \ {A} by ;
( not D in {A} & not E in {A} ) by ;
then A8: {D,E} \ {A} = {D,E} by ZFMISC_1:63;
A9: ( not F in {A} & not J in {A} ) by ;
A10: not C in {A} by ;
A11: not B in {A} by ;
{B,C,D,E,F,J} \ {A} = ({B} \/ {C,D,E,F,J}) \ {A} by ENUMSET1:11
.= ({B} \ {A}) \/ ({C,D,E,F,J} \ {A}) by XBOOLE_1:42
.= {B} \/ ({C,D,E,F,J} \ {A}) by
.= {B} \/ (({C} \/ {D,E,F,J}) \ {A}) by ENUMSET1:7
.= {B} \/ (({C} \ {A}) \/ ({D,E,F,J} \ {A})) by XBOOLE_1:42
.= {B} \/ (({C} \ {A}) \/ (({D,E} \/ {F,J}) \ {A})) by ENUMSET1:5
.= {B} \/ (({C} \ {A}) \/ (({D,E} \ {A}) \/ ({F,J} \ {A}))) by XBOOLE_1:42
.= {B} \/ (({C} \ {A}) \/ ({D,E} \/ {F,J})) by
.= {B} \/ ({C} \/ ({D,E} \/ {F,J})) by
.= {B} \/ ({C} \/ {D,E,F,J}) by ENUMSET1:5
.= {B} \/ {C,D,E,F,J} by ENUMSET1:7
.= {B,C,D,E,F,J} by ENUMSET1:11 ;
then A12: G \ {A} = ({A} \ {A}) \/ {B,C,D,E,F,J} by
.= {} \/ {B,C,D,E,F,J} by XBOOLE_1:37 ;
A13: '/\' (G \ {A}) c= ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in '/\' (G \ {A}) or x in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J )
reconsider xx = x as set by TARSKI:1;
assume x in '/\' (G \ {A}) ; :: thesis: x in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
then consider h being Function, FF being Subset-Family of Y such that
A14: dom h = G \ {A} and
A15: rng h = FF and
A16: for d being set st d in G \ {A} holds
h . d in d and
A17: x = Intersect FF and
A18: x <> {} by BVFUNC_2:def 1;
A19: C in G \ {A} by ;
then A20: h . C in C by A16;
set mbcd = ((h . B) /\ (h . C)) /\ (h . D);
A21: E in G \ {A} by ;
then A22: h . E in rng h by ;
set mbc = (h . B) /\ (h . C);
A23: B in G \ {A} by ;
then h . B in B by A16;
then A24: (h . B) /\ (h . C) in INTERSECTION (B,C) by ;
A25: h . B in rng h by ;
then A26: Intersect FF = meet (rng h) by ;
A27: h . C in rng h by ;
A28: F in G \ {A} by ;
then A29: h . F in rng h by ;
set mbcdef = ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F);
set mbcde = (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E);
A30: not x in by ;
A31: J in G \ {A} by ;
then A32: h . J in rng h by ;
A33: D in G \ {A} by ;
then A34: h . D in rng h by ;
A35: xx c= (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)
proof
let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in xx or m in (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) )
assume A36: m in xx ; :: thesis: m in (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)
then ( m in h . B & m in h . C ) by ;
then A37: m in (h . B) /\ (h . C) by XBOOLE_0:def 4;
m in h . D by ;
then A38: m in ((h . B) /\ (h . C)) /\ (h . D) by ;
m in h . E by ;
then A39: m in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) by ;
m in h . F by ;
then A40: m in ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) by ;
m in h . J by ;
hence m in (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) by ; :: thesis: verum
end;
then ((h . B) /\ (h . C)) /\ (h . D) <> {} by A18;
then A41: not ((h . B) /\ (h . C)) /\ (h . D) in by TARSKI:def 1;
(((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) c= xx
proof
A42: rng h c= {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng h or u in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)} )
assume u in rng h ; :: thesis: u in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
then consider x1 being object such that
A43: x1 in dom h and
A44: u = h . x1 by FUNCT_1:def 3;
( x1 = B or x1 = C or x1 = D or x1 = E or x1 = F or x1 = J ) by ;
hence u in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)} by ; :: thesis: verum
end;
let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) or m in xx )
assume A45: m in (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) ; :: thesis: m in xx
then A46: m in h . J by XBOOLE_0:def 4;
A47: m in ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) by ;
then A48: m in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) by XBOOLE_0:def 4;
then A49: m in h . E by XBOOLE_0:def 4;
A50: m in ((h . B) /\ (h . C)) /\ (h . D) by ;
then A51: m in h . D by XBOOLE_0:def 4;
m in (h . B) /\ (h . C) by ;
then A52: ( m in h . B & m in h . C ) by XBOOLE_0:def 4;
m in h . F by ;
then for y being set st y in rng h holds
m in y by ;
hence m in xx by ; :: thesis: verum
end;
then A53: (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) = x by ;
(h . B) /\ (h . C) <> {} by ;
then not (h . B) /\ (h . C) in by TARSKI:def 1;
then (h . B) /\ (h . C) in (INTERSECTION (B,C)) \ by ;
then A54: (h . B) /\ (h . C) in B '/\' C by PARTIT1:def 4;
h . D in D by ;
then ((h . B) /\ (h . C)) /\ (h . D) in INTERSECTION ((B '/\' C),D) by ;
then ((h . B) /\ (h . C)) /\ (h . D) in (INTERSECTION ((B '/\' C),D)) \ by ;
then A55: ((h . B) /\ (h . C)) /\ (h . D) in (B '/\' C) '/\' D by PARTIT1:def 4;
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) <> {} by ;
then A56: not (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in by TARSKI:def 1;
h . E in E by ;
then (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in INTERSECTION (((B '/\' C) '/\' D),E) by ;
then (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in (INTERSECTION (((B '/\' C) '/\' D),E)) \ by ;
then A57: (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in ((B '/\' C) '/\' D) '/\' E by PARTIT1:def 4;
((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) <> {} by ;
then A58: not ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in by TARSKI:def 1;
h . F in F by ;
then ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in INTERSECTION ((((B '/\' C) '/\' D) '/\' E),F) by ;
then ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in (INTERSECTION ((((B '/\' C) '/\' D) '/\' E),F)) \ by ;
then A59: ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in (((B '/\' C) '/\' D) '/\' E) '/\' F by PARTIT1:def 4;
h . J in J by ;
then x in INTERSECTION (((((B '/\' C) '/\' D) '/\' E) '/\' F),J) by ;
then x in (INTERSECTION (((((B '/\' C) '/\' D) '/\' E) '/\' F),J)) \ by ;
hence x in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J by PARTIT1:def 4; :: thesis: verum
end;
A60: ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J c= '/\' (G \ {A})
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J or x in '/\' (G \ {A}) )
reconsider xx = x as set by TARSKI:1;
assume A61: x in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J ; :: thesis: x in '/\' (G \ {A})
then A62: x <> {} by EQREL_1:def 4;
x in (INTERSECTION (((((B '/\' C) '/\' D) '/\' E) '/\' F),J)) \ by ;
then consider bcdef, j being set such that
A63: bcdef in (((B '/\' C) '/\' D) '/\' E) '/\' F and
A64: j in J and
A65: x = bcdef /\ j by SETFAM_1:def 5;
bcdef in (INTERSECTION ((((B '/\' C) '/\' D) '/\' E),F)) \ by ;
then consider bcde, f being set such that
A66: bcde in ((B '/\' C) '/\' D) '/\' E and
A67: f in F and
A68: bcdef = bcde /\ f by SETFAM_1:def 5;
bcde in (INTERSECTION (((B '/\' C) '/\' D),E)) \ by ;
then consider bcd, e being set such that
A69: bcd in (B '/\' C) '/\' D and
A70: e in E and
A71: bcde = bcd /\ e by SETFAM_1:def 5;
bcd in (INTERSECTION ((B '/\' C),D)) \ by ;
then consider bc, d being set such that
A72: bc in B '/\' C and
A73: d in D and
A74: bcd = bc /\ d by SETFAM_1:def 5;
bc in (INTERSECTION (B,C)) \ by ;
then consider b, c being set such that
A75: ( b in B & c in C ) and
A76: bc = b /\ c by SETFAM_1:def 5;
set h = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j);
A77: ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B = b by ;
A78: dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) = {J,B,C,D,E,F} by Th38
.= {J} \/ {B,C,D,E,F} by ENUMSET1:11
.= {B,C,D,E,F,J} by ENUMSET1:15 ;
then D in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) by ENUMSET1:def 4;
then A79: ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) by FUNCT_1:def 3;
A80: for p being set st p in G \ {A} holds
((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . p in p
proof
let p be set ; :: thesis: ( p in G \ {A} implies ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . p in p )
assume p in G \ {A} ; :: thesis: ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . p in p
then ( p = B or p = C or p = D or p = E or p = F or p = J ) by ;
hence ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . p in p by A6, A64, A67, A70, A73, A75, Th37; :: thesis: verum
end;
E in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) by ;
then A81: ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) by FUNCT_1:def 3;
C in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) by ;
then A82: ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) by FUNCT_1:def 3;
A83: ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C = c by ;
A84: rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) c= {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)}
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) or t in {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)} )
assume t in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) ; :: thesis: t in {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)}
then consider x1 being object such that
A85: x1 in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) and
A86: t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . x1 by FUNCT_1:def 3;
( x1 = B or x1 = C or x1 = D or x1 = E or x1 = F or x1 = J ) by ;
hence t in {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)} by ; :: thesis: verum
end;
J in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) by ;
then A87: ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) by FUNCT_1:def 3;
F in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) by ;
then A88: ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) by FUNCT_1:def 3;
B in dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) by ;
then A89: ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) by FUNCT_1:def 3;
{(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)} c= rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) by ;
then A90: rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) = {(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F),(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J)} by ;
A91: ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J = j by ;
A92: ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F = f by ;
A93: ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E = e by ;
A94: ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D = d by ;
rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) c= bool Y
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) or t in bool Y )
assume t in rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) ; :: thesis: t in bool Y
then ( t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . D or t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . B or t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . C or t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . E or t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . F or t = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) . J ) by ;
hence t in bool Y by A64, A67, A70, A73, A75, A94, A77, A83, A93, A92, A91; :: thesis: verum
end;
then reconsider FF = rng ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) as Subset-Family of Y ;
A95: dom ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) = {J,B,C,D,E,F} by Th38
.= {J} \/ {B,C,D,E,F} by ENUMSET1:11
.= {B,C,D,E,F,J} by ENUMSET1:15 ;
reconsider h = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j) as Function ;
A96: xx c= Intersect FF
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in xx or u in Intersect FF )
assume A97: u in xx ; :: thesis: u in Intersect FF
for y being set st y in FF holds
u in y
proof
let y be set ; :: thesis: ( y in FF implies u in y )
assume A98: y in FF ; :: thesis: u in y
now :: thesis: ( ( y = h . D & u in y ) or ( y = h . B & u in y ) or ( y = h . C & u in y ) or ( y = h . E & u in y ) or ( y = h . F & u in y ) or ( y = h . J & u in y ) )
per cases ( y = h . D or y = h . B or y = h . C or y = h . E or y = h . F or y = h . J ) by ;
case A99: y = h . D ; :: thesis: u in y
u in ((d /\ ((b /\ c) /\ e)) /\ f) /\ j by ;
then u in (d /\ (((b /\ c) /\ e) /\ f)) /\ j by XBOOLE_1:16;
then u in d /\ ((((b /\ c) /\ e) /\ f) /\ j) by XBOOLE_1:16;
hence u in y by ; :: thesis: verum
end;
case A100: y = h . B ; :: thesis: u in y
u in (((c /\ (d /\ b)) /\ e) /\ f) /\ j by ;
then u in ((c /\ ((d /\ b) /\ e)) /\ f) /\ j by XBOOLE_1:16;
then u in ((c /\ ((d /\ e) /\ b)) /\ f) /\ j by XBOOLE_1:16;
then u in (c /\ (((d /\ e) /\ b) /\ f)) /\ j by XBOOLE_1:16;
then u in c /\ ((((d /\ e) /\ b) /\ f) /\ j) by XBOOLE_1:16;
then u in c /\ (((d /\ e) /\ (f /\ b)) /\ j) by XBOOLE_1:16;
then u in c /\ ((d /\ e) /\ ((f /\ b) /\ j)) by XBOOLE_1:16;
then u in c /\ ((d /\ e) /\ (f /\ (j /\ b))) by XBOOLE_1:16;
then u in (c /\ (d /\ e)) /\ (f /\ (j /\ b)) by XBOOLE_1:16;
then u in ((c /\ (d /\ e)) /\ f) /\ (j /\ b) by XBOOLE_1:16;
then u in (((c /\ (d /\ e)) /\ f) /\ j) /\ b by XBOOLE_1:16;
hence u in y by ; :: thesis: verum
end;
case A101: y = h . C ; :: thesis: u in y
u in (((c /\ (d /\ b)) /\ e) /\ f) /\ j by ;
then u in ((c /\ ((d /\ b) /\ e)) /\ f) /\ j by XBOOLE_1:16;
then u in ((c /\ ((d /\ e) /\ b)) /\ f) /\ j by XBOOLE_1:16;
then u in (c /\ (((d /\ e) /\ b) /\ f)) /\ j by XBOOLE_1:16;
then u in c /\ ((((d /\ e) /\ b) /\ f) /\ j) by XBOOLE_1:16;
hence u in y by ; :: thesis: verum
end;
case A102: y = h . E ; :: thesis: u in y
u in (((b /\ c) /\ d) /\ (f /\ e)) /\ j by ;
then u in ((b /\ c) /\ d) /\ ((f /\ e) /\ j) by XBOOLE_1:16;
then u in ((b /\ c) /\ d) /\ ((f /\ j) /\ e) by XBOOLE_1:16;
then u in (((b /\ c) /\ d) /\ (f /\ j)) /\ e by XBOOLE_1:16;
hence u in y by ; :: thesis: verum
end;
case A103: y = h . F ; :: thesis: u in y
u in ((((b /\ c) /\ d) /\ e) /\ j) /\ f by ;
hence u in y by ; :: thesis: verum
end;
case y = h . J ; :: thesis: u in y
hence u in y by ; :: thesis: verum
end;
end;
end;
hence u in y ; :: thesis: verum
end;
then u in meet FF by ;
hence u in Intersect FF by ; :: thesis: verum
end;
A104: Intersect FF = meet (rng h) by ;
Intersect FF c= xx
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Intersect FF or t in xx )
assume A105: t in Intersect FF ; :: thesis: t in xx
h . C in rng h by ;
then A106: t in c by ;
h . B in rng h by ;
then t in b by ;
then A107: t in b /\ c by ;
h . D in rng h by ;
then t in d by ;
then A108: t in (b /\ c) /\ d by ;
h . E in rng h by ;
then t in e by ;
then A109: t in ((b /\ c) /\ d) /\ e by ;
h . F in rng h by ;
then t in f by ;
then A110: t in (((b /\ c) /\ d) /\ e) /\ f by ;
h . J in rng h by ;
then t in j by ;
hence t in xx by ; :: thesis: verum
end;
then x = Intersect FF by ;
hence x in '/\' (G \ {A}) by ; :: thesis: verum
end;
CompF (A,G) = '/\' (G \ {A}) by BVFUNC_2:def 7;
hence CompF (A,G) = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J by ; :: thesis: verum