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

Metamath Proof Explorer

Theorem dmuni

Description: The domain of a union. Part of Exercise 8 of Enderton p. 41. (Contributed by NM, 3-Feb-2004)

Ref Expression
Assertion dmuni dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥

Proof

Step Hyp Ref Expression
1 excom ⊢ ( ∃ 𝑧 ∃ 𝑥 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) ↔ ∃ 𝑥 ∃ 𝑧 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) )
2 ancom ⊢ ( ( ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑥 ) )
3 19.41v ⊢ ( ∃ 𝑧 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) ↔ ( ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) )
4 vex ⊢ 𝑦 ∈ V
5 4 eldm2 ⊢ ( 𝑦 ∈ dom 𝑥 ↔ ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑥 )
6 5 anbi2i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝑥 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑥 ) )
7 2 3 6 3bitr4i ⊢ ( ∃ 𝑧 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝑥 ) )
8 7 exbii ⊢ ( ∃ 𝑥 ∃ 𝑧 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝑥 ) )
9 1 8 bitri ⊢ ( ∃ 𝑧 ∃ 𝑥 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝑥 ) )
10 eluni ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝐴 ↔ ∃ 𝑥 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) )
11 10 exbii ⊢ ( ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝐴 ↔ ∃ 𝑧 ∃ 𝑥 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) )
12 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝑥 ) )
13 9 11 12 3bitr4i ⊢ ( ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥 )
14 4 eldm2 ⊢ ( 𝑦 ∈ dom ∪ 𝐴 ↔ ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝐴 )
15 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 dom 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥 )
16 13 14 15 3bitr4i ⊢ ( 𝑦 ∈ dom ∪ 𝐴 ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 dom 𝑥 )
17 16 eqriv ⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥