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 |X. B ) C_ ( _V X. ( _V X. _V ) )

Proof

Step	Hyp	Ref	Expression
1		df-xrn	|- ( A |X. B ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) )
2		inss1	|- ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) ) C_ ( `' ( 1st |` ( _V X. _V ) ) o. A )
3		relco	|- Rel ( `' ( 1st |` ( _V X. _V ) ) o. A )
4		vex	|- z e. _V
5		vex	|- y e. _V
6	4 5	brcnv	|- ( z `' ( 1st |` ( _V X. _V ) ) y <-> y ( 1st |` ( _V X. _V ) ) z )
7	4	brresi	|- ( y ( 1st |` ( _V X. _V ) ) z <-> ( y e. ( _V X. _V ) /\ y 1st z ) )
8	7	simplbi	|- ( y ( 1st |` ( _V X. _V ) ) z -> y e. ( _V X. _V ) )
9	6 8	sylbi	|- ( z `' ( 1st |` ( _V X. _V ) ) y -> y e. ( _V X. _V ) )
10	9	adantl	|- ( ( x A z /\ z `' ( 1st |` ( _V X. _V ) ) y ) -> y e. ( _V X. _V ) )
11	10	exlimiv	|- ( E. z ( x A z /\ z `' ( 1st |` ( _V X. _V ) ) y ) -> y e. ( _V X. _V ) )
12		vex	|- x e. _V
13	12 5	opelco	|- ( <. x , y >. e. ( `' ( 1st |` ( _V X. _V ) ) o. A ) <-> E. z ( x A z /\ z `' ( 1st |` ( _V X. _V ) ) y ) )
14		opelxp	|- ( <. x , y >. e. ( _V X. ( _V X. _V ) ) <-> ( x e. _V /\ y e. ( _V X. _V ) ) )
15	12 14	mpbiran	|- ( <. x , y >. e. ( _V X. ( _V X. _V ) ) <-> y e. ( _V X. _V ) )
16	11 13 15	3imtr4i	|- ( <. x , y >. e. ( `' ( 1st |` ( _V X. _V ) ) o. A ) -> <. x , y >. e. ( _V X. ( _V X. _V ) ) )
17	3 16	relssi	|- ( `' ( 1st |` ( _V X. _V ) ) o. A ) C_ ( _V X. ( _V X. _V ) )
18	2 17	sstri	|- ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) ) C_ ( _V X. ( _V X. _V ) )
19	1 18	eqsstri	|- ( A |X. B ) C_ ( _V X. ( _V X. _V ) )