MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmrnssfld Structured version   Visualization version   GIF version

Theorem dmrnssfld 5983
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.
StepHypRef Expression
1 vex 3483 . . . . 5 𝑥 ∈ V
21eldm2 5911 . . . 4 (𝑥 ∈ dom 𝐴 ↔ ∃𝑦𝑥, 𝑦⟩ ∈ 𝐴)
31prid1 4761 . . . . . 6 𝑥 ∈ {𝑥, 𝑦}
4 vex 3483 . . . . . . . . . 10 𝑦 ∈ V
51, 4uniop 5519 . . . . . . . . 9 𝑥, 𝑦⟩ = {𝑥, 𝑦}
61, 4uniopel 5520 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥, 𝑦⟩ ∈ 𝐴)
75, 6eqeltrrid 2845 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ 𝐴 → {𝑥, 𝑦} ∈ 𝐴)
8 elssuni 4936 . . . . . . . 8 ({𝑥, 𝑦} ∈ 𝐴 → {𝑥, 𝑦} ⊆ 𝐴)
97, 8syl 17 . . . . . . 7 (⟨𝑥, 𝑦⟩ ∈ 𝐴 → {𝑥, 𝑦} ⊆ 𝐴)
109sseld 3981 . . . . . 6 (⟨𝑥, 𝑦⟩ ∈ 𝐴 → (𝑥 ∈ {𝑥, 𝑦} → 𝑥 𝐴))
113, 10mpi 20 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥 𝐴)
1211exlimiv 1929 . . . 4 (∃𝑦𝑥, 𝑦⟩ ∈ 𝐴𝑥 𝐴)
132, 12sylbi 217 . . 3 (𝑥 ∈ dom 𝐴𝑥 𝐴)
1413ssriv 3986 . 2 dom 𝐴 𝐴
154elrn2 5902 . . . 4 (𝑦 ∈ ran 𝐴 ↔ ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴)
164prid2 4762 . . . . . 6 𝑦 ∈ {𝑥, 𝑦}
179sseld 3981 . . . . . 6 (⟨𝑥, 𝑦⟩ ∈ 𝐴 → (𝑦 ∈ {𝑥, 𝑦} → 𝑦 𝐴))
1816, 17mpi 20 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ 𝐴𝑦 𝐴)
1918exlimiv 1929 . . . 4 (∃𝑥𝑥, 𝑦⟩ ∈ 𝐴𝑦 𝐴)
2015, 19sylbi 217 . . 3 (𝑦 ∈ ran 𝐴𝑦 𝐴)
2120ssriv 3986 . 2 ran 𝐴 𝐴
2214, 21unssi 4190 1 (dom 𝐴 ∪ ran 𝐴) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wex 1778  wcel 2107  cun 3948  wss 3950  {cpr 4627  cop 4631   cuni 4906  dom cdm 5684  ran crn 5685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-cnv 5692  df-dm 5694  df-rn 5695
This theorem is referenced by:  relfld  6294  relcoi2  6296  dmexg  7924  rnexg  7925  wundm  10769  wunrn  10770  relexpdm  15083  relexprn  15087  relexpfld  15089  psdmrn  18619  dirdm  18646  dirge  18649  tailf  36377  filnetlem3  36382  dmwf  44987  rnwf  44988
  Copyright terms: Public domain W3C validator