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

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

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