As for the statement: Mario above is right, so, if I get it right this time, one can prove |- ( ( X e. V /\ A C_ U. X ) -> U. ( X |`t A ) = A ) and |- ( ( X e. V /\ A e. W ) -> U. ( X |`t A ) = ( ( U. X ) i^i A ) )
As for the name: why not call |` the "elementwise intersection" and write in the comment: "if x is a family of sets, then ( x |` y ) is the family obtained from x where each member of x is intersected by y." Benoît > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/132df271-2319-466b-8198-f5590699041dn%40googlegroups.com.
