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

Metamath Proof Explorer

Theorem iinun2

Description: Indexed intersection of union. Generalization of half of theorem "Distributive laws" in Enderton p. 30. Use intiin to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004)

Ref Expression
Assertion iinun2 ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∪ 𝐶 ) = ( 𝐵 ∪ ∩ 𝑥 ∈ 𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 r19.32v ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∨ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ) )
2 elun ⊢ ( 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶 ) )
3 2 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶 ) )
4 eliin ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ) )
5 4 elv ⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 )
6 5 orbi2i ⊢ ( ( 𝑦 ∈ 𝐵 ∨ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∨ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ) )
7 1 3 6 3bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∨ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ) )
8 eliin ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∪ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ) )
9 8 elv ⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∪ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) )
10 elun ⊢ ( 𝑦 ∈ ( 𝐵 ∪ ∩ 𝑥 ∈ 𝐴 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∨ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ) )
11 7 9 10 3bitr4i ⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∪ 𝐶 ) ↔ 𝑦 ∈ ( 𝐵 ∪ ∩ 𝑥 ∈ 𝐴 𝐶 ) )
12 11 eqriv ⊢ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∪ 𝐶 ) = ( 𝐵 ∪ ∩ 𝑥 ∈ 𝐴 𝐶 )