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 ) ) |
| 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 ) ) |