let I be set ; :: thesis: for Z, M being ManySortedSet of I
for SF being V8() MSSubsetFamily of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c= Z1 ) holds
Z c= meet SF
let Z, M be ManySortedSet of I; :: thesis: for SF being V8() MSSubsetFamily of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c= Z1 ) holds
Z c= meet SF
let SF be V8() MSSubsetFamily of M; :: thesis: ( ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c= Z1 ) implies Z c= meet SF )
assume A1: for Z1 being ManySortedSet of I st Z1 in SF holds
Z c= Z1 ; :: thesis: Z c= meet SF
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or Z . i c= (meet SF) . i )
consider T being ManySortedSet of I such that
A2: T in SF by PBOOLE:146;
assume A3: i in I ; :: thesis: Z . i c= (meet SF) . i
then consider Q being Subset-Family of (M . i) such that
A4: Q = SF . i and
A5: (meet SF) . i = Intersect Q by Def2;
A6: for Z9 being set st Z9 in Q holds
Z . i c= Z9
proof
let Z9 be set ; :: thesis: ( Z9 in Q implies Z . i c= Z9 )
assume A7: Z9 in Q ; :: thesis: Z . i c= Z9
dom (T +* (i .--> Z9)) = I by A3, PZFMISC1:1;
then reconsider K = T +* (i .--> Z9) as ManySortedSet of I by PARTFUN1:def 4, RELAT_1:def 18;
A8: dom (i .--> Z9) = {i} by FUNCOP_1:19;
i in {i} by TARSKI:def 1;
then A9: K . i = (i .--> Z9) . i by A8, FUNCT_4:14
.= Z9 by FUNCOP_1:87 ;
K in SF
proof
let q be set ; :: according to PBOOLE:def 4 :: thesis: ( not q in I or K . q in SF . q )
assume A10: q in I ; :: thesis: K . q in SF . q
per cases ( q = i or q <> i ) ;
suppose q = i ; :: thesis: K . q in SF . q
hence K . q in SF . q by A4, A7, A9; :: thesis: verum
end;
end;
end;
then Z c= K by A1;
hence Z . i c= Z9 by A3, A9, PBOOLE:def 5; :: thesis: verum
end;
Intersect Q = meet Q by A3, A4, SETFAM_1:def 10;
hence Z . i c= (meet SF) . i by A3, A4, A5, A6, SETFAM_1:6; :: thesis: verum