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

Theorem relssdmrn 5377
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 1793 . . . 4  |-  ( <.
x ,  y >.  e.  A  ->  E. y <. x ,  y >.  e.  A )
3 19.8a 1793 . . . 4  |-  ( <.
x ,  y >.  e.  A  ->  E. x <. x ,  y >.  e.  A )
4 opelxp 4888 . . . . 5  |-  ( <.
x ,  y >.  e.  ( dom  A  X.  ran  A )  <->  ( x  e.  dom  A  /\  y  e.  ran  A ) )
5 vex 2994 . . . . . . 7  |-  x  e. 
_V
65eldm2 5057 . . . . . 6  |-  ( x  e.  dom  A  <->  E. y <. x ,  y >.  e.  A )
7 vex 2994 . . . . . . 7  |-  y  e. 
_V
87elrn2 5098 . . . . . 6  |-  ( y  e.  ran  A  <->  E. x <. x ,  y >.  e.  A )
96, 8anbi12i 697 . . . . 5  |-  ( ( x  e.  dom  A  /\  y  e.  ran  A )  <->  ( E. y <. x ,  y >.  e.  A  /\  E. x <. x ,  y >.  e.  A ) )
104, 9bitri 249 . . . 4  |-  ( <.
x ,  y >.  e.  ( dom  A  X.  ran  A )  <->  ( E. y <. x ,  y
>.  e.  A  /\  E. x <. x ,  y
>.  e.  A ) )
112, 3, 10sylanbrc 664 . . 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 4951 1  |-  ( Rel 
A  ->  A  C_  ( dom  A  X.  ran  A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   E.wex 1586    e. wcel 1756    C_ wss 3347   <.cop 3902    X. cxp 4857   dom cdm 4859   ran crn 4860   Rel wrel 4864
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4432  ax-nul 4440  ax-pr 4550
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2739  df-rex 2740  df-rab 2743  df-v 2993  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-nul 3657  df-if 3811  df-sn 3897  df-pr 3899  df-op 3903  df-br 4312  df-opab 4370  df-xp 4865  df-rel 4866  df-cnv 4867  df-dm 4869  df-rn 4870
This theorem is referenced by:  cnvssrndm  5378  cossxp  5379  relrelss  5380  relfld  5382  fssxp  5589  oprabss  6195  cnvexg  6543  resfunexgALT  6559  cofunexg  6560  fnexALT  6562  erssxp  7143  wunco  8919  imasless  14497  sylow2a  16137  gsum2d  16482  gsum2dOLD  16483  znleval  18006  tsmsxp  19748  relfi  25959  fcnvgreu  26010
  Copyright terms: Public domain W3C validator