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

Metamath Proof Explorer

Theorem dmrnssfld

Description: The domain and range of a class are included in its double union. (Contributed by NM, 13-May-2008)

Ref Expression
Assertion dmrnssfld ( dom 𝐴 ∪ ran 𝐴 ) ⊆ ∪ ∪ 𝐴

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 1 eldm2 ⊢ ( 𝑥 ∈ dom 𝐴 ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
3 1 prid1 ⊢ 𝑥 ∈ { 𝑥 , 𝑦 }
4 vex ⊢ 𝑦 ∈ V
5 1 4 uniop ⊢ ∪ ⟨ 𝑥 , 𝑦 ⟩ = { 𝑥 , 𝑦 }
6 1 4 uniopel ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ∪ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝐴 )
7 5 6 eqeltrrid ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → { 𝑥 , 𝑦 } ∈ ∪ 𝐴 )
8 elssuni ⊢ ( { 𝑥 , 𝑦 } ∈ ∪ 𝐴 → { 𝑥 , 𝑦 } ⊆ ∪ ∪ 𝐴 )
9 7 8 syl ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → { 𝑥 , 𝑦 } ⊆ ∪ ∪ 𝐴 )
10 9 sseld ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ( 𝑥 ∈ { 𝑥 , 𝑦 } → 𝑥 ∈ ∪ ∪ 𝐴 ) )
11 3 10 mpi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑥 ∈ ∪ ∪ 𝐴 )
12 11 exlimiv ⊢ ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑥 ∈ ∪ ∪ 𝐴 )
13 2 12 sylbi ⊢ ( 𝑥 ∈ dom 𝐴 → 𝑥 ∈ ∪ ∪ 𝐴 )
14 13 ssriv ⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
15 4 elrn2 ⊢ ( 𝑦 ∈ ran 𝐴 ↔ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
16 4 prid2 ⊢ 𝑦 ∈ { 𝑥 , 𝑦 }
17 9 sseld ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ( 𝑦 ∈ { 𝑥 , 𝑦 } → 𝑦 ∈ ∪ ∪ 𝐴 ) )
18 16 17 mpi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑦 ∈ ∪ ∪ 𝐴 )
19 18 exlimiv ⊢ ( ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑦 ∈ ∪ ∪ 𝐴 )
20 15 19 sylbi ⊢ ( 𝑦 ∈ ran 𝐴 → 𝑦 ∈ ∪ ∪ 𝐴 )
21 20 ssriv ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
22 14 21 unssi ⊢ ( dom 𝐴 ∪ ran 𝐴 ) ⊆ ∪ ∪ 𝐴