Metamath Proof Explorer


Theorem relssdmrn

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)

Ref Expression
Assertion relssdmrn
|- ( Rel A -> A C_ ( dom A X. ran A ) )

Proof

Step Hyp Ref Expression
1 id
 |-  ( Rel A -> Rel A )
2 vex
 |-  x e. _V
3 vex
 |-  y e. _V
4 2 3 opeldm
 |-  ( <. x , y >. e. A -> x e. dom A )
5 2 3 opelrn
 |-  ( <. x , y >. e. A -> y e. ran A )
6 4 5 opelxpd
 |-  ( <. x , y >. e. A -> <. x , y >. e. ( dom A X. ran A ) )
7 6 a1i
 |-  ( Rel A -> ( <. x , y >. e. A -> <. x , y >. e. ( dom A X. ran A ) ) )
8 1 7 relssdv
 |-  ( Rel A -> A C_ ( dom A X. ran A ) )