Metamath Proof Explorer

Theorem txpss3v

Description: A tail Cartesian product is a subset of the class of ordered triples. (Contributed by Scott Fenton, 31-Mar-2012)

		Ref	Expression
	Assertion	txpss3v	$⊢ (A \otimes B) \subseteq V \times (V \times V)$

Proof

Step	Hyp	Ref	Expression
1		df-txp	$⊢ (A \otimes B) = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B)$
2		inss1	$⊢ ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B) \subseteq {({1^{st} ↾}_{(V \times V)})}^{-1} \circ A$
3		relco	$⊢ Rel ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A)$
4		vex	$⊢ z \in V$
5		vex	$⊢ y \in V$
6	4 5	brcnv	$⊢ z {({1^{st} ↾}_{(V \times V)})}^{-1} y \leftrightarrow y ({1^{st} ↾}_{(V \times V)}) z$
7	4	brresi	$⊢ y ({1^{st} ↾}_{(V \times V)}) z \leftrightarrow (y \in (V \times V) \land y 1^{st} z)$
8	7	simplbi	$⊢ y ({1^{st} ↾}_{(V \times V)}) z \to y \in (V \times V)$
9	6 8	sylbi	$⊢ z {({1^{st} ↾}_{(V \times V)})}^{-1} y \to y \in (V \times V)$
10	9	adantl	$⊢ (x A z \land z {({1^{st} ↾}_{(V \times V)})}^{-1} y) \to y \in (V \times V)$
11	10	exlimiv	$⊢ \exists z (x A z \land z {({1^{st} ↾}_{(V \times V)})}^{-1} y) \to y \in (V \times V)$
12		vex	$⊢ x \in V$
13	12 5	opelco	$⊢ ⟨x, y⟩ \in ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) \leftrightarrow \exists z (x A z \land z {({1^{st} ↾}_{(V \times V)})}^{-1} y)$
14		opelxp	$⊢ ⟨x, y⟩ \in (V \times (V \times V)) \leftrightarrow (x \in V \land y \in (V \times V))$
15	12 14	mpbiran	$⊢ ⟨x, y⟩ \in (V \times (V \times V)) \leftrightarrow y \in (V \times V)$
16	11 13 15	3imtr4i	$⊢ ⟨x, y⟩ \in ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) \to ⟨x, y⟩ \in (V \times (V \times V))$
17	3 16	relssi	$⊢ {({1^{st} ↾}_{(V \times V)})}^{-1} \circ A \subseteq V \times (V \times V)$
18	2 17	sstri	$⊢ ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B) \subseteq V \times (V \times V)$
19	1 18	eqsstri	$⊢ (A \otimes B) \subseteq V \times (V \times V)$