Theorem txprel

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

	Ref	Expression
Assertion	txprel	⊢ Rel ( 𝐴 ⊗ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		txpss3v	⊢ ( 𝐴 ⊗ 𝐵 ) ⊆ ( V × ( V × V ) )
2		xpss	⊢ ( V × ( V × V ) ) ⊆ ( V × V )
3	1 2	sstri	⊢ ( 𝐴 ⊗ 𝐵 ) ⊆ ( V × V )
4		df-rel	⊢ ( Rel ( 𝐴 ⊗ 𝐵 ) ↔ ( 𝐴 ⊗ 𝐵 ) ⊆ ( V × V ) )
5	3 4	mpbir	⊢ Rel ( 𝐴 ⊗ 𝐵 )