Theorem relssdmrn 6286

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.

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (Rel 𝐴 → Rel 𝐴)
2		vex 3458	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3458	. . . . 5 ⊢ 𝑦 ∈ V
4	2, 3	opeldm 5895	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → 𝑥 ∈ dom 𝐴)
5	2, 3	opelrn 5931	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → 𝑦 ∈ ran 𝐴)
6	4, 5	opelxpd 5694	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ (dom 𝐴 × ran 𝐴))
7	6	a1i 11	. 2 ⊢ (Rel 𝐴 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ (dom 𝐴 × ran 𝐴)))
8	1, 7	relssdv 5769	1 ⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ⊆ wss 3900  ⟨cop 4838   × cxp 5653  dom cdm 5655  ran crn 5656  Rel wrel 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-rel 5662  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  resssxp  6287  cnvssrndm  6288  cossxp  6289  relrelss  6290  relfld  6292  fssxp  6756  oprabss  7548  cnvexg  7957  resfunexgALT  7981  cofunexg  7982  fnexALT  7984  funexw  7985  erssxp  8766  ttrclexg  9748  wunco  10842  trclublem  15174  trclubi  15175  trclub  15177  reltrclfv  15196  imasless  17738  sylow2a  19860  gsum2d  20213  znleval  21887  tsmsxp  24501  relfi  33265  fcnvgreu  33335  elrgspnsubrunlem2  33876  relssinxpdmrn  39472  trclubNEW  44809  trrelsuperreldg  44858  trrelsuperrel2dg  44861  relwf  46150  hfrel  46213  ishfstruct  46224