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 𝐴 ) ⊆ ∪ ∪ 𝐴