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