Theorem xrnrel

Description: A range Cartesian product is a relation. This is Scott Fenton's txprel with a different symbol, see https://github.com/metamath/set.mm/issues/2469 . (Contributed by Scott Fenton, 31-Mar-2012)

	Ref	Expression
Assertion	xrnrel	$$⊢\mathrm{Rel}A⋉B$$

Proof

Step	Hyp	Ref	Expression
1		xrnss3v	$$⊢A⋉B\subseteq \mathrm{V}\times \left(\mathrm{V}\times \mathrm{V}\right)$$
2		xpss	$$⊢\mathrm{V}\times \left(\mathrm{V}\times \mathrm{V}\right)\subseteq \mathrm{V}\times \mathrm{V}$$
3	1 2	sstri	$$⊢A⋉B\subseteq \mathrm{V}\times \mathrm{V}$$
4		df-rel	$$⊢\mathrm{Rel}A⋉B\leftrightarrow A⋉B\subseteq \mathrm{V}\times \mathrm{V}$$
5	3 4	mpbir	$$⊢\mathrm{Rel}A⋉B$$