This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem txprel

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

		Ref	Expression
	Assertion	txprel	$⊢ Rel (A \otimes B)$

Step	Hyp	Ref	Expression
1		txpss3v	$⊢ (A \otimes B) \subseteq V \times (V \times V)$
2		xpss	$⊢ V \times (V \times V) \subseteq V \times V$
3	1 2	sstri	$⊢ (A \otimes B) \subseteq V \times V$
4		df-rel	$⊢ Rel (A \otimes B) \leftrightarrow (A \otimes B) \subseteq V \times V$
5	3 4	mpbir	$⊢ Rel (A \otimes B)$