let I be set ; :: thesis: for M being ManySortedSet of I
for SF, SG, SH being MSSubsetFamily of M st SH = SF (\/) SG holds
meet SH = (meet SF) (/\) (meet SG)
let M be ManySortedSet of I; :: thesis: for SF, SG, SH being MSSubsetFamily of M st SH = SF (\/) SG holds
meet SH = (meet SF) (/\) (meet SG)
let SF, SG, SH be MSSubsetFamily of M; :: thesis: ( SH = SF (\/) SG implies meet SH = (meet SF) (/\) (meet SG) )
assume A1: SH = SF (\/) SG ; :: thesis: meet SH = (meet SF) (/\) (meet SG)
now :: thesis: for i being object st i in I holds
(meet SH) . i = ((meet SF) (/\) (meet SG)) . i
let i be object ; :: thesis: ( i in I implies (meet SH) . i = ((meet SF) (/\) (meet SG)) . i )
assume A2: i in I ; :: thesis: (meet SH) . i = ((meet SF) (/\) (meet SG)) . i
then consider Qf being Subset-Family of (M . i) such that
A3: Qf = SF . i and
A4: (meet SF) . i = Intersect Qf by Def1;
consider Qh being Subset-Family of (M . i) such that
A5: Qh = SH . i and
A6: (meet SH) . i = Intersect Qh by A2, Def1;
consider Qg being Subset-Family of (M . i) such that
A7: Qg = SG . i and
A8: (meet SG) . i = Intersect Qg by A2, Def1;
A9: Qh = Qf \/ Qg by A1, A2, A3, A7, A5, PBOOLE:def 4;
now :: thesis: ( ( Qf <> {} & Qg <> {} & (meet SH) . i = ((meet SF) (/\) (meet SG)) . i ) or ( Qf <> {} & Qg = {} & (meet SH) . i = ((meet SF) (/\) (meet SG)) . i ) or ( Qf = {} & Qg <> {} & (meet SH) . i = ((meet SF) (/\) (meet SG)) . i ) or ( Qf = {} & Qg = {} & (meet SH) . i = ((meet SF) (/\) (meet SG)) . i ) )
per cases ( ( Qf <> {} & Qg <> {} ) or ( Qf <> {} & Qg = {} ) or ( Qf = {} & Qg <> {} ) or ( Qf = {} & Qg = {} ) ) ;
case A10: ( Qf <> {} & Qg <> {} ) ; :: thesis: (meet SH) . i = ((meet SF) (/\) (meet SG)) . i
hence (meet SH) . i = meet Qh by A6, A9, SETFAM_1:def 9
.= (meet Qf) /\ (meet Qg) by A9, A10, SETFAM_1:9
.= ((meet SF) . i) /\ (meet Qg) by A4, A10, SETFAM_1:def 9
.= ((meet SF) . i) /\ ((meet SG) . i) by A8, A10, SETFAM_1:def 9
.= ((meet SF) (/\) (meet SG)) . i by A2, PBOOLE:def 5 ;
:: thesis: verum
end;
case A11: ( Qf <> {} & Qg = {} ) ; :: thesis: (meet SH) . i = ((meet SF) (/\) (meet SG)) . i
hence (meet SH) . i = ((meet SF) . i) /\ (M . i) by A4, A6, A9, XBOOLE_1:28
.= ((meet SF) . i) /\ ((meet SG) . i) by A8, A11, SETFAM_1:def 9
.= ((meet SF) (/\) (meet SG)) . i by A2, PBOOLE:def 5 ;
:: thesis: verum
end;
case A12: ( Qf = {} & Qg <> {} ) ; :: thesis: (meet SH) . i = ((meet SF) (/\) (meet SG)) . i
hence (meet SH) . i = (M . i) /\ ((meet SG) . i) by A8, A6, A9, XBOOLE_1:28
.= ((meet SF) . i) /\ ((meet SG) . i) by A4, A12, SETFAM_1:def 9
.= ((meet SF) (/\) (meet SG)) . i by A2, PBOOLE:def 5 ;
:: thesis: verum
end;
case ( Qf = {} & Qg = {} ) ; :: thesis: (meet SH) . i = ((meet SF) (/\) (meet SG)) . i
hence (meet SH) . i = (Intersect Qf) /\ (Intersect Qg) by A6, A9
.= ((meet SF) (/\) (meet SG)) . i by A2, A4, A8, PBOOLE:def 5 ;
:: thesis: verum
end;
end;
end;
hence (meet SH) . i = ((meet SF) (/\) (meet SG)) . i ; :: thesis: verum
end;
hence meet SH = (meet SF) (/\) (meet SG) ; :: thesis: verum