Theorem txprel

Description: A tail Cartesian product is a relationship. (Contributed by Scott Fenton, 31-Mar-2012)

	Ref	Expression
Assertion	txprel	$$⊢\mathrm{Rel}\left(A\otimes B\right)$$

Proof

Step	Hyp	Ref	Expression
1		txpss3v	$$⊢\left(A\otimes B\right)\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	$$⊢\left(A\otimes B\right)\subseteq \mathrm{V}\times \mathrm{V}$$
4		df-rel	$$⊢\mathrm{Rel}\left(A\otimes B\right)\leftrightarrow \left(A\otimes B\right)\subseteq \mathrm{V}\times \mathrm{V}$$
5	3 4	mpbir	$$⊢\mathrm{Rel}\left(A\otimes B\right)$$