:: BVFUNC14 semantic presentation

theorem E1: :: BVFUNC14:1
for b1 being non empty set
for b2 being Element of b1
for b3, b4 being a_partition of b1 holds EqClass b2,(b3 '/\' b4) = (EqClass b2,b3) /\ (EqClass b2,b4)
proof
let c1 be non empty set ;
let c2 be Element of c1;
let c3, c4 be a_partition of c1;
E2: EqClass c2,(c3 '/\' c4) c= (EqClass c2,c3) /\ (EqClass c2,c4)
proof
let c5 be set ; :: uses TARSKI:def 3
assume E3: c5 in EqClass c2,(c3 '/\' c4) ;
E4: EqClass c2,(c3 '/\' c4) c= EqClass c2,c3 by BVFUNC11:3;
EqClass c2,(c3 '/\' c4) c= EqClass c2,c4 by BVFUNC11:3;
hence c5 in (EqClass c2,c3) /\ (EqClass c2,c4) by E3, E4, XBOOLE_0:def 3;
end;
(EqClass c2,c3) /\ (EqClass c2,c4) c= EqClass c2,(c3 '/\' c4)
proof
let c5 be set ; :: uses TARSKI:def 3
assume E3: c5 in (EqClass c2,c3) /\ (EqClass c2,c4) ;
then reconsider c6 = c5 as Element of c1 ;
E4: ( c6 in EqClass c2,c3 & c6 in EqClass c2,c4 ) by E3, XBOOLE_0:def 3;
E5: ( c6 in EqClass c6,c3 & EqClass c6,c3 in c3 ) by T_1TOPSP:def 1;
E6: ( c6 in EqClass c6,c4 & EqClass c6,c4 in c4 ) by T_1TOPSP:def 1;
E7: EqClass c6,c3 meets EqClass c2,c3 by E4, E5, XBOOLE_0:3;
E8: EqClass c6,c4 meets EqClass c2,c4 by E4, E6, XBOOLE_0:3;
E9: ( c2 in EqClass c2,c3 & EqClass c2,c3 in c3 ) by T_1TOPSP:def 1;
E10: ( c2 in EqClass c2,c4 & EqClass c2,c4 in c4 ) by T_1TOPSP:def 1;
E11: c3 '/\' c4 = (INTERSECTION c3,c4) \ {{} } by PARTIT1:def 4;
set c7 = EqClass c2,(c3 '/\' c4);
( EqClass c2,(c3 '/\' c4) in INTERSECTION c3,c4 & not EqClass c2,(c3 '/\' c4) in {{} } ) by E11, XBOOLE_0:def 4;
then consider c8, c9 being set such that
E12: ( c8 in c3 & c9 in c4 & EqClass c2,(c3 '/\' c4) = c8 /\ c9 ) by SETFAM_1:def 5;
c2 in c8 /\ c9 by E12, T_1TOPSP:def 1;
then E13: ( c2 in c8 & c2 in c9 ) by XBOOLE_0:def 3;
then c8 meets EqClass c2,c3 by E9, XBOOLE_0:3;
then E14: c8 = EqClass c2,c3 by E12, EQREL_1:def 6;
c9 meets EqClass c2,c4 by E10, E13, XBOOLE_0:3;
then E15: c9 = EqClass c2,c4 by E12, EQREL_1:def 6;
E16: c8 = EqClass c6,c3 by E7, E14, T_1TOPSP:9;
c6 in (EqClass c6,c3) /\ (EqClass c6,c4) by E5, E6, XBOOLE_0:def 3;
hence c5 in EqClass c2,(c3 '/\' c4) by E8, E12, E15, E16, T_1TOPSP:9;
end;
hence (EqClass c2,c3) /\ (EqClass c2,c4) = EqClass c2,(c3 '/\' c4) by E2, XBOOLE_0:def 10;
end;

theorem :: BVFUNC14:2
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4 being a_partition of b1 holds
( ( b2 = {b3,b4} ) implies ( not b3 <> b4 or '/\' b2 = b3 '/\' b4 ) )
proof
let c1 be non empty set ;
let c2 be Subset of (PARTITIONS c1);
let c3, c4 be a_partition of c1;
assume E2: ( c2 = {c3,c4} & c3 <> c4 ) ;
E3: c3 '/\' c4 c= '/\' c2
proof
let c5 be set ; :: uses TARSKI:def 3
assume E4: c5 in c3 '/\' c4 ;
then c5 in (INTERSECTION c3,c4) \ {{} } by PARTIT1:def 4;
then ( c5 in INTERSECTION c3,c4 & not c5 in {{} } ) by XBOOLE_0:def 4;
then consider c6, c7 being set such that
E5: ( c6 in c3 & c7 in c4 & c5 = c6 /\ c7 ) by SETFAM_1:def 5;
set c8 = c3,c4 --> c6,c7;
E6: dom (c3,c4 --> c6,c7) = {c3,c4} by FUNCT_4:65;
E7: rng (c3,c4 --> c6,c7) = {c6,c7} by E2, FUNCT_4:67;
E8: rng (c3,c4 --> c6,c7) = {c6,c7} by E2, FUNCT_4:67;
rng (c3,c4 --> c6,c7) c= bool c1
proof
let c9 be set ; :: uses TARSKI:def 3
assume E9: c9 in rng (c3,c4 --> c6,c7) ;
now
per cases ( c9 = c6 or c9 = c7 ) by E7, E9, TARSKI:def 2;
case c9 = c6 ;
hence c9 in bool c1 by E5;
end;
case c9 = c7 ;
hence c9 in bool c1 by E5;
end;
end;
end;
hence c9 in bool c1 ;
end;
then reconsider c9 = rng (c3,c4 --> c6,c7) as Subset-Family of c1 ;
E9: for b1 being set holds
( b1 in c2 implies (c3,c4 --> c6,c7) . b1 in b1 )
proof
let c10 be set ;
assume E10: c10 in c2 ;
now
per cases ( c10 = c3 or c10 = c4 ) by E2, E10, TARSKI:def 2;
case c10 = c3 ;
hence (c3,c4 --> c6,c7) . c10 in c10 by E2, E5, FUNCT_4:66;
end;
case c10 = c4 ;
hence (c3,c4 --> c6,c7) . c10 in c10 by E2, E5, FUNCT_4:66;
end;
end;
end;
hence (c3,c4 --> c6,c7) . c10 in c10 ;
end;
E10: c5 c= Intersect c9
proof
let c10 be set ; :: uses TARSKI:def 3
assume E11: c10 in c5 ;
for b1 being set holds
( b1 in c9 implies c10 in b1 )
proof
let c11 be set ;
assume E12: c11 in c9 ;
now
per cases ( c11 = c6 or c11 = c7 ) by E7, E12, TARSKI:def 2;
case c11 = c6 ;
hence c10 in c11 by E5, E11, XBOOLE_0:def 3;
end;
case c11 = c7 ;
hence c10 in c11 by E5, E11, XBOOLE_0:def 3;
end;
end;
end;
hence c10 in c11 ;
end;
then c10 in meet c9 by E7, SETFAM_1:def 1;
hence c10 in Intersect c9 by E7, SETFAM_1:def 10;
end;
Intersect c9 c= c5
proof
let c10 be set ; :: uses TARSKI:def 3
assume E11: c10 in Intersect c9 ;
E12: ( c6 in {c6,c7} & c7 in {c6,c7} ) by TARSKI:def 2;
then ( c6 in c9 & c7 in c9 ) by E2, FUNCT_4:67;
then Intersect c9 = meet c9 by SETFAM_1:def 10;
then ( c10 in c6 & c10 in c7 ) by E8, E11, E12, SETFAM_1:def 1;
hence c10 in c5 by E5, XBOOLE_0:def 3;
end;
then E11: c5 = Intersect c9 by E10, XBOOLE_0:def 10;
c5 <> {} by E4, EQREL_1:def 6;
hence c5 in '/\' c2 by E2, E6, E9, E11, BVFUNC_2:def 1;
end;
'/\' c2 c= c3 '/\' c4
proof
let c5 be set ; :: uses TARSKI:def 3
assume c5 in '/\' c2 ;
then consider c6 being Function, c7 being Subset-Family of c1 such that
E4: ( dom c6 = c2 & rng c6 = c7 & for b1 being set holds
( b1 in c2 implies c6 . b1 in b1 ) & c5 = Intersect c7 & c5 <> {} ) by BVFUNC_2:def 1;
( c3 in c2 & c4 in c2 ) by E2, TARSKI:def 2;
then E5: ( c6 . c3 in c3 & c6 . c4 in c4 ) by E4;
( c3 in dom c6 & c4 in dom c6 ) by E2, E4, TARSKI:def 2;
then E6: ( c6 . c3 in rng c6 & c6 . c4 in rng c6 ) by FUNCT_1:def 5;
E7: not c5 in {{} } by E4, TARSKI:def 1;
E8: (c6 . c3) /\ (c6 . c4) c= c5
proof
let c8 be set ; :: uses TARSKI:def 3
assume E9: c8 in (c6 . c3) /\ (c6 . c4) ;
E10: rng c6 c= {(c6 . c3),(c6 . c4)}
proof
let c9 be set ; :: uses TARSKI:def 3
assume c9 in rng c6 ;
then consider c10 being set such that
E11: ( c10 in dom c6 & c9 = c6 . c10 ) by FUNCT_1:def 5;
now
per cases ( c10 = c3 or c10 = c4 ) by E2, E4, E11, TARSKI:def 2;
case c10 = c3 ;
hence c9 in {(c6 . c3),(c6 . c4)} by E11, TARSKI:def 2;
end;
case c10 = c4 ;
hence c9 in {(c6 . c3),(c6 . c4)} by E11, TARSKI:def 2;
end;
end;
end;
hence c9 in {(c6 . c3),(c6 . c4)} ;
end;
for b1 being set holds
( b1 in rng c6 implies c8 in b1 )
proof
let c9 be set ;
assume E11: c9 in rng c6 ;
now
per cases ( c9 = c6 . c3 or c9 = c6 . c4 ) by E10, E11, TARSKI:def 2;
case c9 = c6 . c3 ;
hence c8 in c9 by E9, XBOOLE_0:def 3;
end;
case c9 = c6 . c4 ;
hence c8 in c9 by E9, XBOOLE_0:def 3;
end;
end;
end;
hence c8 in c9 ;
end;
then c8 in meet (rng c6) by E6, SETFAM_1:def 1;
hence c8 in c5 by E4, E6, SETFAM_1:def 10;
end;
c5 c= (c6 . c3) /\ (c6 . c4)
proof
let c8 be set ; :: uses TARSKI:def 3
assume c8 in c5 ;
then c8 in meet (rng c6) by E4, E6, SETFAM_1:def 10;
then ( c8 in c6 . c3 & c8 in c6 . c4 ) by E6, SETFAM_1:def 1;
hence c8 in (c6 . c3) /\ (c6 . c4) by XBOOLE_0:def 3;
end;
then (c6 . c3) /\ (c6 . c4) = c5 by E8, XBOOLE_0:def 10;
then c5 in INTERSECTION c3,c4 by E5, SETFAM_1:def 5;
then c5 in (INTERSECTION c3,c4) \ {{} } by E7, XBOOLE_0:def 4;
hence c5 in c3 '/\' c4 by PARTIT1:def 4;
end;
hence '/\' c2 = c3 '/\' c4 by E3, XBOOLE_0:def 10;
end;

E2: for b1, b2, b3, b4, b5, b6 being set holds dom (((b1 .--> b4) +* (b2 .--> b5)) +* (b3 .--> b6)) = {b1,b2,b3}
proof
let c1, c2, c3, c4, c5, c6 be set ;
E3: dom ((c1 .--> c4) +* (c2 .--> c5)) = (dom (c1 .--> c4)) \/ (dom (c2 .--> c5)) by FUNCT_4:def 1;
E4: dom (c1 .--> c4) = {c1} by CQC_LANG:5;
E5: dom (c2 .--> c5) = {c2} by CQC_LANG:5;
dom (c3 .--> c6) = {c3} by CQC_LANG:5;
hence dom (((c1 .--> c4) +* (c2 .--> c5)) +* (c3 .--> c6)) = ({c1} \/ {c2}) \/ {c3} by E3, E4, E5, FUNCT_4:def 1
.= {c1,c2} \/ {c3} by ENUMSET1:41
.= {c1,c2,c3} by ENUMSET1:43 ;

end;

E3: for b1 being Function
for b2, b3, b4, b5 being set holds
( b2 <> b3 implies ((b1 +* (b2 .--> b4)) +* (b3 .--> b5)) . b2 = b4 )
proof
let c1 be Function;
let c2, c3, c4, c5 be set ;
assume E4: c2 <> c3 ;
set c6 = (c1 +* (c2 .--> c4)) +* (c3 .--> c5);
E5: dom (c2 .--> c4) = {c2} by CQC_LANG:5;
dom (c3 .--> c5) = {c3} by CQC_LANG:5;
then not c2 in dom (c3 .--> c5) by E4, TARSKI:def 1;
then E6: ((c1 +* (c2 .--> c4)) +* (c3 .--> c5)) . c2 = (c1 +* (c2 .--> c4)) . c2 by FUNCT_4:12;
c2 in dom (c2 .--> c4) by E5, TARSKI:def 1;
hence ((c1 +* (c2 .--> c4)) +* (c3 .--> c5)) . c2 = (c2 .--> c4) . c2 by E6, FUNCT_4:14
.= c4 by CQC_LANG:6 ;

end;

E4: for b1, b2, b3, b4, b5, b6 being set holds
( ( ) implies ( not b1 <> b2 or not b3 <> b1 or (((b1 .--> b4) +* (b2 .--> b5)) +* (b3 .--> b6)) . b1 = b4 ) )
proof
let c1, c2, c3, c4, c5, c6 be set ;
assume E5: ( c1 <> c2 & c3 <> c1 ) ;
set c7 = ((c1 .--> c4) +* (c2 .--> c5)) +* (c3 .--> c6);
E6: dom (c2 .--> c5) = {c2} by CQC_LANG:5;
dom (c3 .--> c6) = {c3} by CQC_LANG:5;
then not c1 in dom (c3 .--> c6) by E5, TARSKI:def 1;
then E7: (((c1 .--> c4) +* (c2 .--> c5)) +* (c3 .--> c6)) . c1 = ((c1 .--> c4) +* (c2 .--> c5)) . c1 by FUNCT_4:12;
not c1 in dom (c2 .--> c5) by E5, E6, TARSKI:def 1;
hence (((c1 .--> c4) +* (c2 .--> c5)) +* (c3 .--> c6)) . c1 = (c1 .--> c4) . c1 by E7, FUNCT_4:12
.= c4 by CQC_LANG:6 ;

end;

E5: for b1, b2, b3, b4, b5, b6 being set
for b7 being Function holds
( b7 = ((b1 .--> b4) +* (b2 .--> b5)) +* (b3 .--> b6) implies rng b7 = {(b7 . b1),(b7 . b2),(b7 . b3)} )
proof
let c1, c2, c3, c4, c5, c6 be set ;
let c7 be Function;
assume c7 = ((c1 .--> c4) +* (c2 .--> c5)) +* (c3 .--> c6) ;
then E6: dom c7 = {c1,c2,c3} by E2;
then E7: c3 in dom c7 by ENUMSET1:def 1;
E8: c1 in dom c7 by E6, ENUMSET1:def 1;
E9: c2 in dom c7 by E6, ENUMSET1:def 1;
E10: rng c7 c= {(c7 . c1),(c7 . c2),(c7 . c3)}
proof
let c8 be set ; :: uses TARSKI:def 3
assume c8 in rng c7 ;
then consider c9 being set such that
E11: ( c9 in dom c7 & c8 = c7 . c9 ) by FUNCT_1:def 5;
now
per cases not ( not c9 = c3 & not c9 = c1 & not c9 = c2 ) by E6, E11, ENUMSET1:def 1;
case c9 = c3 ;
hence c8 in {(c7 . c1),(c7 . c2),(c7 . c3)} by E11, ENUMSET1:def 1;
end;
case c9 = c1 ;
hence c8 in {(c7 . c1),(c7 . c2),(c7 . c3)} by E11, ENUMSET1:def 1;
end;
case c9 = c2 ;
hence c8 in {(c7 . c1),(c7 . c2),(c7 . c3)} by E11, ENUMSET1:def 1;
end;
end;
end;
hence c8 in {(c7 . c1),(c7 . c2),(c7 . c3)} ;
end;
{(c7 . c1),(c7 . c2),(c7 . c3)} c= rng c7
proof
let c8 be set ; :: uses TARSKI:def 3
assume E11: c8 in {(c7 . c1),(c7 . c2),(c7 . c3)} ;
now
per cases not ( not c8 = c7 . c3 & not c8 = c7 . c1 & not c8 = c7 . c2 ) by E11, ENUMSET1:def 1;
case c8 = c7 . c3 ;
hence c8 in rng c7 by E7, FUNCT_1:def 5;
end;
case c8 = c7 . c1 ;
hence c8 in rng c7 by E8, FUNCT_1:def 5;
end;
case c8 = c7 . c2 ;
hence c8 in rng c7 by E9, FUNCT_1:def 5;
end;
end;
end;
hence c8 in rng c7 ;
end;
hence rng c7 = {(c7 . c1),(c7 . c2),(c7 . c3)} by E10, XBOOLE_0:def 10;
end;

theorem :: BVFUNC14:3
for b1 being non empty set
for b2 being Subset of (PARTITIONS b1)
for b3, b4, b5 being a_partition of b1 holds
( ( b2 = {b3,b4,b5} ) implies ( not b3 <> b4 or not b4 <> b5 or not b5 <> b3 or '/\' b2 = (b3 '/\' b4) '/\' b5 ) )
proof
let c1 be non empty set ;
let c2 be Subset of (PARTITIONS c1);
let c3, c4, c5 be a_partition of c1;
assume E6: ( c2 = {c3,c4,c5} & c3 <> c4 & c4 <> c5 & c5 <> c3 ) ;
E7: (c3 '/\' c4) '/\' c5 c= '/\' c2
proof
let c6 be set ; :: uses TARSKI:def 3
assume E8: c6 in (c3 '/\' c4) '/\' c5 ;
then c6 in (INTERSECTION (c3 '/\' c4),c5) \ {{} } by PARTIT1:def 4;
then ( c6 in INTERSECTION (c3 '/\' c4),c5 & not c6 in {{} } ) by XBOOLE_0:def 4;
then consider c7, c8 being set such that
E9: ( c7 in c3 '/\' c4 & c8 in c5 & c6 = c7 /\ c8 ) by SETFAM_1:def 5;
c7 in (INTERSECTION c3,c4) \ {{} } by E9, PARTIT1:def 4;
then ( c7 in INTERSECTION c3,c4 & not c7 in {{} } ) by XBOOLE_0:def 4;
then consider c9, c10 being set such that
E10: ( c9 in c3 & c10 in c4 & c7 = c9 /\ c10 ) by SETFAM_1:def 5;
set c11 = ((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8);
E11: dom (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) = {c3,c4,c5} by E2;
E12: (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c5 = c8 by YELLOW14:3;
E13: (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c3 = c9 by E6, E4;
E14: (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c4 = c10 by E6, E3;
E15: for b1 being set holds
( b1 in c2 implies (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . b1 in b1 )
proof
let c12 be set ;
assume E16: c12 in c2 ;
now
per cases not ( not c12 = c5 & not c12 = c3 & not c12 = c4 ) by E6, E16, ENUMSET1:def 1;
case c12 = c5 ;
hence (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c12 in c12 by E9, YELLOW14:3;
end;
case c12 = c3 ;
hence (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c12 in c12 by E6, E10, E4;
end;
case c12 = c4 ;
hence (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c12 in c12 by E6, E10, E3;
end;
end;
end;
hence (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c12 in c12 ;
end;
E16: c5 in dom (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) by E11, ENUMSET1:def 1;
E17: rng (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) = {((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c3),((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c4),((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c5)} by E5
.= {((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c5),((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c3),((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c4)} by ENUMSET1:100 ;
rng (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) c= bool c1
proof
let c12 be set ; :: uses TARSKI:def 3
assume E18: c12 in rng (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) ;
now
per cases not ( not c12 = (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c5 & not c12 = (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c3 & not c12 = (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c4 ) by E17, E18, ENUMSET1:def 1;
case c12 = (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c5 ;
hence c12 in bool c1 by E9, E12;
end;
case c12 = (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c3 ;
then c12 = c9 by E6, E4;
hence c12 in bool c1 by E10;
end;
case c12 = (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c4 ;
then c12 = c10 by E6, E3;
hence c12 in bool c1 by E10;
end;
end;
end;
hence c12 in bool c1 ;
end;
then reconsider c12 = rng (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) as Subset-Family of c1 ;
E18: rng (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) <> {} by E16, FUNCT_1:12;
E19: c6 c= Intersect c12
proof
let c13 be set ; :: uses TARSKI:def 3
assume E20: c13 in c6 ;
E21: (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c5 in {((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c5),((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c3),((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c4)} by ENUMSET1:def 1;
for b1 being set holds
( b1 in c12 implies c13 in b1 )
proof
let c14 be set ;
assume E22: c14 in c12 ;
now
per cases not ( not c14 = (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c5 & not c14 = (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c3 & not c14 = (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c4 ) by E17, E22, ENUMSET1:def 1;
case c14 = (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c5 ;
hence c13 in c14 by E9, E12, E20, XBOOLE_0:def 3;
end;
case E23: c14 = (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c3 ;
c13 in c9 /\ (c10 /\ c8) by E9, E10, E20, XBOOLE_1:16;
hence c13 in c14 by E13, E23, XBOOLE_0:def 3;
end;
case E23: c14 = (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c4 ;
c13 in c10 /\ (c9 /\ c8) by E9, E10, E20, XBOOLE_1:16;
hence c13 in c14 by E14, E23, XBOOLE_0:def 3;
end;
end;
end;
hence c13 in c14 ;
end;
then c13 in meet c12 by E17, E21, SETFAM_1:def 1;
hence c13 in Intersect c12 by E17, E21, SETFAM_1:def 10;
end;
Intersect c12 c= c6
proof
let c13 be set ; :: uses TARSKI:def 3
assume c13 in Intersect c12 ;
then E20: c13 in meet (rng (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8))) by E18, SETFAM_1:def 10;
( (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c3 in {((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c5),((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c3),((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c4)} & (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c4 in {((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c5),((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c3),((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c4)} & (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c5 in {((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c5),((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c3),((((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c4)} ) by ENUMSET1:def 1;
then E21: ( c13 in (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c3 & c13 in (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c4 & c13 in (((c3 .--> c9) +* (c4 .--> c10)) +* (c5 .--> c8)) . c5 ) by E17, E20, SETFAM_1:def 1;
then ( c13 in c9 & c13 in c10 & c13 in c8 ) by E6, E3, E4, YELLOW14:3;
then c13 in c9 /\ c10 by XBOOLE_0:def 3;
hence c13 in c6 by E9, E10, E12, E21, XBOOLE_0:def 3;
end;
then E20: c6 = Intersect c12 by E19, XBOOLE_0:def 10;
c6 <> {} by E8, EQREL_1:def 6;
hence c6 in '/\' c2 by E6, E11, E15, E20, BVFUNC_2:def 1;
end;
'/\' c2 c= (c3 '/\' c4) '/\' c5
proof
let c6 be set ; :: uses TARSKI:def 3
assume c6 in '/\' c2 ;
then consider c7 being Function, c8 being Subset-Family of c1 such that
E8: ( dom c7 = c2 & rng c7 = c8 & for b1 being set holds
( b1 in c2 implies c7 . b1 in b1 ) & c6 = Intersect c8 & c6 <> {} ) by BVFUNC_2:def 1;
( c3 in c2 & c4 in c2 & c5 in c2 ) by E6, ENUMSET1:def 1;
then E9: ( c7 . c3 in c3 & c7 . c4 in c4 & c7 . c5 in c5 ) by E8;
( c3 in dom c7 & c4 in dom c7 & c5 in dom c7 ) by E6, E8, ENUMSET1:def 1;
then E10: ( c7 . c3 in rng c7 & c7 . c4 in rng c7 & c7 . c5 in rng c7 ) by FUNCT_1:def 5;
E11: not c6 in {{} } by E8, TARSKI:def 1;
E12: ((c7 . c3) /\ (c7 . c4)) /\ (c7 . c5) c= c6
proof
let c9 be set ; :: uses TARSKI:def 3
assume E13: c9 in ((c7 . c3) /\ (c7 . c4)) /\ (c7 . c5) ;
then E14: ( c9 in (c7 . c3) /\ (c7 . c4) & c9 in c7 . c5 ) by XBOOLE_0:def 3;
E15: rng c7 c= {(c7 . c3),(c7 . c4),(c7 . c5)}
proof
let c10 be set ; :: uses TARSKI:def 3
assume c10 in rng c7 ;
then consider c11 being set such that
E16: ( c11 in dom c7 & c10 = c7 . c11 ) by FUNCT_1:def 5;
now
per cases not ( not c11 = c3 & not c11 = c4 & not c11 = c5 ) by E6, E8, E16, ENUMSET1:def 1;
case c11 = c3 ;
hence c10 in {(c7 . c3),(c7 . c4),(c7 . c5)} by E16, ENUMSET1:def 1;
end;
case c11 = c4 ;
hence c10 in {(c7 . c3),(c7 . c4),(c7 . c5)} by E16, ENUMSET1:def 1;
end;
case c11 = c5 ;
hence c10 in {(c7 . c3),(c7 . c4),(c7 . c5)} by E16, ENUMSET1:def 1;
end;
end;
end;
hence c10 in {(c7 . c3),(c7 . c4),(c7 . c5)} ;
end;
for b1 being set holds
( b1 in rng c7 implies c9 in b1 )
proof
let c10 be set ;
assume E16: c10 in rng c7 ;
now
per cases not ( not c10 = c7 . c3 & not c10 = c7 . c4 & not c10 = c7 . c5 ) by E15, E16, ENUMSET1:def 1;
case c10 = c7 . c3 ;
hence c9 in c10 by E14, XBOOLE_0:def 3;
end;
case c10 = c7 . c4 ;
hence c9 in c10 by E14, XBOOLE_0:def 3;
end;
case c10 = c7 . c5 ;
hence c9 in c10 by E13, XBOOLE_0:def 3;
end;
end;
end;
hence c9 in