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

Proof

Step Hyp Ref Expression
1 df-txp 
 |-  ( 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 ) )