:: BVFUNC23 semantic presentation

theorem E1: :: BVFUNC23:1
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4, b5, b6, b7, b8 being a_partition of b1 holds
( ( b2 = {b3,b4,b5,b6,b7,b8} ) implies ( not b3 <> b4 or not b3 <> b5 or not b3 <> b6 or not b3 <> b7 or not b3 <> b8 or not b4 <> b5 or not b4 <> b6 or not b4 <> b7 or not b4 <> b8 or not b5 <> b6 or not b5 <> b7 or not b5 <> b8 or not b6 <> b7 or not b6 <> b8 or not b7 <> b8 or CompF b3,b2 = (((b4 '/\' b5) '/\' b6) '/\' b7) '/\' b8 ) )
proof
let c1 be non empty set ;
let c2 be Subset of (PARTITIONS c1);
let c3, c4, c5, c6, c7, c8 be a_partition of c1;
assume E2: ( c2 = {c3,c4,c5,c6,c7,c8} & c3 <> c4 & c3 <> c5 & c3 <> c6 & c3 <> c7 & c3 <> c8 & c4 <> c5 & c4 <> c6 & c4 <> c7 & c4 <> c8 & c5 <> c6 & c5 <> c7 & c5 <> c8 & c6 <> c7 & c6 <> c8 & c7 <> c8 ) ;
E3: CompF c3,c2 = '/\' (c2 \ {c3}) by BVFUNC_2:def 7;
E4: c2 \ {c3} = ({c3} \/ {c4,c5,c6,c7,c8}) \ {c3} by E2, ENUMSET1:51
.= ({c3} \ {c3}) \/ ({c4,c5,c6,c7,c8} \ {c3}) by XBOOLE_1:42 ;
E5: not c4 in {c3} by E2, TARSKI:def 1;
E6: not c5 in {c3} by E2, TARSKI:def 1;
E7: not c6 in {c3} by E2, TARSKI:def 1;
E8: not c7 in {c3} by E2, TARSKI:def 1;
E9: not c8 in {c3} by E2, TARSKI:def 1;
E10: {c4,c5,c6,c7,c8} \ {c3} = ({c4} \/ {c5,c6,c7,c8}) \ {c3} by ENUMSET1:47
.= ({c4} \ {c3}) \/ ({c5,c6,c7,c8} \ {c3}) by XBOOLE_1:42
.= {c4} \/ ({c5,c6,c7,c8} \ {c3}) by E5, ZFMISC_1:67
.= {c4} \/ (({c5} \/ {c6,c7,c8}) \ {c3}) by ENUMSET1:44
.= {c4} \/ (({c5} \ {c3}) \/ ({c6,c7,c8} \ {c3})) by XBOOLE_1:42
.= {c4} \/ (({c5} \ {c3}) \/ (({c6,c7} \/ {c8}) \ {c3})) by ENUMSET1:43
.= {c4} \/ (({c5} \ {c3}) \/ (({c6,c7} \ {c3}) \/ ({c8} \ {c3}))) by XBOOLE_1:42
.= {c4} \/ (({c5} \ {c3}) \/ ({c6,c7} \/ ({c8} \ {c3}))) by E7, E8, ZFMISC_1:72
.= {c4} \/ (({c5} \ {c3}) \/ ({c6,c7} \/ {c8})) by E9, ZFMISC_1:67
.= {c4} \/ ({c5} \/ ({c6,c7} \/ {c8})) by E6, ZFMISC_1:67
.= {c4} \/ ({c5} \/ {c6,c7,c8}) by ENUMSET1:43
.= {c4} \/ {c5,c6,c7,c8} by ENUMSET1:44
.= {c4,c5,c6,c7,c8} by ENUMSET1:47 ;
c3 in {c3} by TARSKI:def 1;
then E11: {c3} \ {c3} = {} by ZFMISC_1:68;
E12: (((c4 '/\' c5) '/\' c6) '/\' c7) '/\' c8 c= '/\' (c2 \ {c3})
proof
let c9 be set ; :: uses TARSKI:def 3
assume E13: c9 in (((c4 '/\' c5) '/\' c6) '/\' c7) '/\' c8 ;
then c9 in (INTERSECTION (((c4 '/\' c5) '/\' c6) '/\' c7),c8) \ {{} } by PARTIT1:def 4;
then ( c9 in INTERSECTION (((c4 '/\' c5) '/\' c6) '/\' c7),c8 & not c9 in {{} } ) by XBOOLE_0:def 4;
then consider c10, c11 being set such that
E14: ( c10 in ((c4 '/\' c5) '/\' c6) '/\' c7 & c11 in c8 & c9 = c10 /\ c11 ) by SETFAM_1:def 5;
c10 in (INTERSECTION ((c4 '/\' c5) '/\' c6),c7) \ {{} } by E14, PARTIT1:def 4;
then ( c10 in INTERSECTION ((c4 '/\' c5) '/\' c6),c7 & not c10 in {{} } ) by XBOOLE_0:def 4;
then consider c12, c13 being set such that
E15: ( c12 in (c4 '/\' c5) '/\' c6 & c13 in c7 & c10 = c12 /\ c13 ) by SETFAM_1:def 5;
c12 in (INTERSECTION (c4 '/\' c5),c6) \ {{} } by E15, PARTIT1:def 4;
then ( c12 in INTERSECTION (c4 '/\' c5),c6 & not c12 in {{} } ) by XBOOLE_0:def 4;
then consider c14, c15 being set such that
E16: ( c14 in c4 '/\' c5 & c15 in c6 & c12 = c14 /\ c15 ) by SETFAM_1:def 5;
c14 in (INTERSECTION c4,c5) \ {{} } by E16, PARTIT1:def 4;
then ( c14 in INTERSECTION c4,c5 & not c14 in {{} } ) by XBOOLE_0:def 4;
then consider c16, c17 being set such that
E17: ( c16 in c4 & c17 in c5 & c14 = c16 /\ c17 ) by SETFAM_1:def 5;
set c18 = ((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11);
E18: dom (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) = {c8,c4,c5,c6,c7} by BVFUNC14:30
.= {c8} \/ {c4,c5,c6,c7} by ENUMSET1:47
.= {c4,c5,c6,c7,c8} by ENUMSET1:50 ;
E19: (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c6 = c15 by E2, BVFUNC14:29;
E20: (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c4 = c16 by E2, BVFUNC14:29;
E21: (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c5 = c17 by E2, BVFUNC14:29;
E22: (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c7 = c13 by E2, BVFUNC14:29;
E23: (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c8 = c11 by E2, BVFUNC14:29;
E24: for b1 being set holds
( b1 in c2 \ {c3} implies (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . b1 in b1 )
proof
let c19 be set ;
assume E25: c19 in c2 \ {c3} ;
now
per cases not ( not c19 = c6 & not c19 = c4 & not c19 = c5 & not c19 = c7 & not c19 = c8 ) by E4, E10, E11, E25, ENUMSET1:def 3;
case c19 = c6 ;
hence (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c19 in c19 by E2, E16, BVFUNC14:29;
end;
case c19 = c4 ;
hence (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c19 in c19 by E2, E17, BVFUNC14:29;
end;
case c19 = c5 ;
hence (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c19 in c19 by E2, E17, BVFUNC14:29;
end;
case c19 = c7 ;
hence (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c19 in c19 by E2, E15, BVFUNC14:29;
end;
case c19 = c8 ;
hence (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c19 in c19 by E2, E14, BVFUNC14:29;
end;
end;
end;
hence (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c19 in c19 ;
end;
E25: c6 in dom (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) by E18, ENUMSET1:def 3;
then E26: (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c6 in rng (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) by FUNCT_1:def 5;
E27: c4 in dom (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) by E18, ENUMSET1:def 3;
E28: c5 in dom (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) by E18, ENUMSET1:def 3;
E29: c7 in dom (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) by E18, ENUMSET1:def 3;
E30: c8 in dom (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) by E18, ENUMSET1:def 3;
E31: rng (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) c= {((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c6),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c4),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c5),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c7),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c8)}
proof
let c19 be set ; :: uses TARSKI:def 3
assume c19 in rng (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) ;
then consider c20 being set such that
E32: ( c20 in dom (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) & c19 = (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c20 ) by FUNCT_1:def 5;
now
per cases not ( not c20 = c6 & not c20 = c4 & not c20 = c5 & not c20 = c7 & not c20 = c8 ) by E18, E32, ENUMSET1:def 3;
case c20 = c6 ;
hence c19 in {((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c6),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c4),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c5),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c7),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c8)} by E32, ENUMSET1:def 3;
end;
case c20 = c4 ;
hence c19 in {((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c6),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c4),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c5),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c7),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c8)} by E32, ENUMSET1:def 3;
end;
case c20 = c5 ;
hence c19 in {((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c6),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c4),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c5),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c7),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c8)} by E32, ENUMSET1:def 3;
end;
case c20 = c7 ;
hence c19 in {((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c6),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c4),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c5),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c7),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c8)} by E32, ENUMSET1:def 3;
end;
case c20 = c8 ;
hence c19 in {((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c6),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c4),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c5),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c7),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c8)} by E32, ENUMSET1:def 3;
end;
end;
end;
hence c19 in {((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c6),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c4),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c5),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c7),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c8)} ;
end;
{((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c6),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c4),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c5),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c7),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c8)} c= rng (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11))
proof
let c19 be set ; :: uses TARSKI:def 3
assume E32: c19 in {((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c6),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c4),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c5),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c7),((((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c8)} ;
now
per cases not ( not c19 = (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c6 & not c19 = (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c4 & not c19 = (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c5 & not c19 = (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c7 & not c19 = (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c8 ) by E32, ENUMSET1:def 3;
case c19 = (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c6 ;
hence c19 in rng (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) by E25, FUNCT_1:def 5;
end;
case c19 = (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c4 ;
hence c19 in rng (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) by E27, FUNCT_1:def 5;
end;
case c19 = (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c5 ;
hence c19 in rng (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) by E28, FUNCT_1:def 5;
end;
case c19 = (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c7 ;
hence c19 in rng (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) by E29, FUNCT_1:def 5;
end;
case c19 = (((((c4 .--> c16) +* (c5 .--> c17)) +* (c6 .--> c15)) +* (c7 .--> c13)) +* (c8 .--> c11)) . c8 ;
hence c19 in rng (((((c4 .--> c16) +* (c5