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

Theorem relssdmrn 6288
Description: A relation is included in the Cartesian product of its domain and range. Exercise 4.12(t) of [Mendelson] p. 235. (Contributed by NM, 3-Aug-1994.) (Proof shortened by SN, 23-Dec-2024.)
Assertion
Ref Expression
relssdmrn (Rel 𝐴𝐴 ⊆ (dom 𝐴 × ran 𝐴))

Proof of Theorem relssdmrn
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 22 . 2 (Rel 𝐴 → Rel 𝐴)
2 vex 3484 . . . . 5 𝑥 ∈ V
3 vex 3484 . . . . 5 𝑦 ∈ V
42, 3opeldm 5918 . . . 4 (⟨𝑥, 𝑦⟩ ∈ 𝐴𝑥 ∈ dom 𝐴)
52, 3opelrn 5954 . . . 4 (⟨𝑥, 𝑦⟩ ∈ 𝐴𝑦 ∈ ran 𝐴)
64, 5opelxpd 5724 . . 3 (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ (dom 𝐴 × ran 𝐴))
76a1i 11 . 2 (Rel 𝐴 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ (dom 𝐴 × ran 𝐴)))
81, 7relssdv 5798 1 (Rel 𝐴𝐴 ⊆ (dom 𝐴 × ran 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  wss 3951  cop 4632   × cxp 5683  dom cdm 5685  ran crn 5686  Rel wrel 5690
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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-cnv 5693  df-dm 5695  df-rn 5696
This theorem is referenced by:  resssxp  6290  cnvssrndm  6291  cossxp  6292  relrelss  6293  relfld  6295  fssxp  6763  oprabss  7541  cnvexg  7946  resfunexgALT  7972  cofunexg  7973  fnexALT  7975  funexw  7976  erssxp  8768  ttrclexg  9763  wunco  10773  trclublem  15034  trclubi  15035  trclub  15037  reltrclfv  15056  imasless  17585  sylow2a  19637  gsum2d  19990  znleval  21573  tsmsxp  24163  relfi  32615  fcnvgreu  32683  elrgspnsubrunlem2  33252  relssinxpdmrn  38350  trclubNEW  43632  trrelsuperreldg  43681  trrelsuperrel2dg  43684  relwf  44984
  Copyright terms: Public domain W3C validator