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

Theorem relssdmrn 5318
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.)
Assertion
Ref Expression
relssdmrn  |-  ( Rel 
A  ->  A  C_  ( dom  A  X.  ran  A
) )

Proof of Theorem relssdmrn
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 22 . 2  |-  ( Rel 
A  ->  Rel  A )
2 19.8a 1912 . . . 4  |-  ( <.
x ,  y >.  e.  A  ->  E. y <. x ,  y >.  e.  A )
3 19.8a 1912 . . . 4  |-  ( <.
x ,  y >.  e.  A  ->  E. x <. x ,  y >.  e.  A )
4 opelxp 4826 . . . . 5  |-  ( <.
x ,  y >.  e.  ( dom  A  X.  ran  A )  <->  ( x  e.  dom  A  /\  y  e.  ran  A ) )
5 vex 3025 . . . . . . 7  |-  x  e. 
_V
65eldm2 4995 . . . . . 6  |-  ( x  e.  dom  A  <->  E. y <. x ,  y >.  e.  A )
7 vex 3025 . . . . . . 7  |-  y  e. 
_V
87elrn2 5036 . . . . . 6  |-  ( y  e.  ran  A  <->  E. x <. x ,  y >.  e.  A )
96, 8anbi12i 701 . . . . 5  |-  ( ( x  e.  dom  A  /\  y  e.  ran  A )  <->  ( E. y <. x ,  y >.  e.  A  /\  E. x <. x ,  y >.  e.  A ) )
104, 9bitri 252 . . . 4  |-  ( <.
x ,  y >.  e.  ( dom  A  X.  ran  A )  <->  ( E. y <. x ,  y
>.  e.  A  /\  E. x <. x ,  y
>.  e.  A ) )
112, 3, 10sylanbrc 668 . . 3  |-  ( <.
x ,  y >.  e.  A  ->  <. x ,  y >.  e.  ( dom  A  X.  ran  A ) )
1211a1i 11 . 2  |-  ( Rel 
A  ->  ( <. x ,  y >.  e.  A  -> 
<. x ,  y >.  e.  ( dom  A  X.  ran  A ) ) )
131, 12relssdv 4889 1  |-  ( Rel 
A  ->  A  C_  ( dom  A  X.  ran  A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370   E.wex 1657    e. wcel 1872    C_ wss 3379   <.cop 3947    X. cxp 4794   dom cdm 4796   ran crn 4797   Rel wrel 4801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-br 4367  df-opab 4426  df-xp 4802  df-rel 4803  df-cnv 4804  df-dm 4806  df-rn 4807
This theorem is referenced by:  cnvssrndm  5319  cossxp  5320  relrelss  5321  relfld  5323  fssxp  5701  oprabss  6340  cnvexg  6697  resfunexgALT  6714  cofunexg  6715  fnexALT  6717  erssxp  7341  wunco  9109  trclublem  13003  trclubi  13004  trclub  13006  reltrclfv  13025  imasless  15389  sylow2a  17214  gsum2d  17547  znleval  19067  tsmsxp  21111  relfi  28159  idssxp  28173  fcnvgreu  28221  rtrclex  36137  trclubNEW  36139  rtrclexi  36141  trrelsuperreldg  36173  trrelsuperrel2dg  36176  rp-imass  36279  idhe  36296
  Copyright terms: Public domain W3C validator