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)

	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		19.8a	|- ( <. x , y >. e. A -> E. y <. x , y >. e. A )
3		19.8a	|- ( <. x , y >. e. A -> E. x <. x , y >. e. A )
4		opelxp	|- ( <. x , y >. e. ( dom A X. ran A ) <-> ( x e. dom A /\ y e. ran A ) )
5		vex	|- x e. _V
6	5	eldm2	|- ( x e. dom A <-> E. y <. x , y >. e. A )
7		vex	|- y e. _V
8	7	elrn2	|- ( y e. ran A <-> E. x <. x , y >. e. A )
9	6 8	anbi12i	|- ( ( x e. dom A /\ y e. ran A ) <-> ( E. y <. x , y >. e. A /\ E. x <. x , y >. e. A ) )
10	4 9	bitri	|- ( <. x , y >. e. ( dom A X. ran A ) <-> ( E. y <. x , y >. e. A /\ E. x <. x , y >. e. A ) )
11	2 3 10	sylanbrc	|- ( <. x , y >. e. A -> <. x , y >. e. ( dom A X. ran A ) )
12	11	a1i	|- ( Rel A -> ( <. x , y >. e. A -> <. x , y >. e. ( dom A X. ran A ) ) )
13	1 12	relssdv	|- ( Rel A -> A C_ ( dom A X. ran A ) )