This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ B C ⊆ ⋂ y ∈ B ⋃ x ∈ A C

Proof

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