Theorem dmrnssfld 5958

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

Assertion

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

Proof of Theorem dmrnssfld

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

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

Syntax hints:  ∃wex 1779   ∈ wcel 2109   ∪ cun 3929   ⊆ wss 3931  {cpr 4608  ⟨cop 4612  ∪ cuni 4888  dom cdm 5659  ran crn 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is referenced by:  relfld  6269  relcoi2  6271  dmexg  7902  rnexg  7903  wundm  10747  wunrn  10748  relexpdm  15067  relexprn  15071  relexpfld  15073  psdmrn  18588  dirdm  18615  dirge  18618  tailf  36398  filnetlem3  36403  dmwf  44957  rnwf  44958