Metamath Proof Explorer

Theorem iuniin

Description: Law combining indexed union with indexed intersection. Eq. 14 in KuratowskiMostowski p. 109. This theorem also appears as the last example at http://en.wikipedia.org/wiki/Union%5F%28set%5Ftheory%29 . (Contributed by NM, 17-Aug-2004) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion iuniin ⊢⋃x∈A⋂y∈BC⊆⋂y∈B⋃x∈AC

Proof

Step Hyp Ref Expression
1 r19.12 ⊢∃x∈A∀y∈Bz∈C→∀y∈B∃x∈Az∈C
2 eliin ⊢z∈V→z∈⋂y∈BC↔∀y∈Bz∈C
3 2 elv ⊢z∈⋂y∈BC↔∀y∈Bz∈C
4 3 rexbii ⊢∃x∈Az∈⋂y∈BC↔∃x∈A∀y∈Bz∈C
5 eliun ⊢z∈⋃x∈AC↔∃x∈Az∈C
6 5 ralbii ⊢∀y∈Bz∈⋃x∈AC↔∀y∈B∃x∈Az∈C
7 1 4 6 3imtr4i ⊢∃x∈Az∈⋂y∈BC→∀y∈Bz∈⋃x∈AC
8 eliun ⊢z∈⋃x∈A⋂y∈BC↔∃x∈Az∈⋂y∈BC
9 eliin ⊢z∈V→z∈⋂y∈B⋃x∈AC↔∀y∈Bz∈⋃x∈AC
10 9 elv ⊢z∈⋂y∈B⋃x∈AC↔∀y∈Bz∈⋃x∈AC
11 7 8 10 3imtr4i ⊢z∈⋃x∈A⋂y∈BC→z∈⋂y∈B⋃x∈AC
12 11 ssriv ⊢⋃x∈A⋂y∈BC⊆⋂y∈B⋃x∈AC