Theorem xrnss3v

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

	Ref	Expression
Assertion	xrnss3v	$$⊢A⋉B\subseteq \mathrm{V}\times \left(\mathrm{V}\times \mathrm{V}\right)$$

Proof

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