Metamath Proof Explorer


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 ) )