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 ∪ 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 ⊆ ∩ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶

Proof

Step Hyp Ref Expression
1 r19.12 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐶 )
2 eliin ⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ∩ 𝑦 ∈ 𝐵 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 ) )
3 2 elv ⊢ ( 𝑧 ∈ ∩ 𝑦 ∈ 𝐵 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 )
4 3 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ∩ 𝑦 ∈ 𝐵 𝐶 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 )
5 eliun ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐶 )
6 5 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐵 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐶 )
7 1 4 6 3imtr4i ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ∩ 𝑦 ∈ 𝐵 𝐶 → ∀ 𝑦 ∈ 𝐵 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 )
8 eliun ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ∩ 𝑦 ∈ 𝐵 𝐶 )
9 eliin ⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ∩ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ) )
10 9 elv ⊢ ( 𝑧 ∈ ∩ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 )
11 7 8 10 3imtr4i ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 → 𝑧 ∈ ∩ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶 )
12 11 ssriv ⊢ ∪ 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 ⊆ ∩ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶