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

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

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