Metamath Proof Explorer

Theorem pprodss4v

Description: The parallel product is a subclass of ( (V X. V ) X. (V X. V ) ) . (Contributed by Scott Fenton, 11-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion pprodss4v 
|- pprod ( A , B ) C_ ( ( _V X. _V ) X. ( _V X. _V ) )

Proof

Step Hyp Ref Expression
1 df-pprod 
 |-  pprod ( A , B ) = ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) )
2 txprel 
 |-  Rel ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) )
3 txpss3v 
 |-  ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) C_ ( _V X. ( _V X. _V ) )
4 3 sseli 
 |-  ( <. x , y >. e. ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) -> <. x , y >. e. ( _V X. ( _V X. _V ) ) )
5 opelxp2 
 |-  ( <. x , y >. e. ( _V X. ( _V X. _V ) ) -> y e. ( _V X. _V ) )
6 4 5 syl 
 |-  ( <. x , y >. e. ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) -> y e. ( _V X. _V ) )
7 elvv 
 |-  ( y e. ( _V X. _V ) <-> E. z E. w y = <. z , w >. )
8 opeq2 
 |-  ( y = <. z , w >. -> <. x , y >. = <. x , <. z , w >. >. )
9 8 eleq1d 
 |-  ( y = <. z , w >. -> ( <. x , y >. e. ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) <-> <. x , <. z , w >. >. e. ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) ) )
10 df-br 
 |-  ( x ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) <. z , w >. <-> <. x , <. z , w >. >. e. ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) )
11 vex 
 |-  x e. _V
12 vex 
 |-  z e. _V
13 vex 
 |-  w e. _V
14 11 12 13 brtxp 
 |-  ( x ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) <. z , w >. <-> ( x ( A o. ( 1st |` ( _V X. _V ) ) ) z /\ x ( B o. ( 2nd |` ( _V X. _V ) ) ) w ) )
15 11 12 brco 
 |-  ( x ( A o. ( 1st |` ( _V X. _V ) ) ) z <-> E. y ( x ( 1st |` ( _V X. _V ) ) y /\ y A z ) )
16 vex 
 |-  y e. _V
17 16 brresi 
 |-  ( x ( 1st |` ( _V X. _V ) ) y <-> ( x e. ( _V X. _V ) /\ x 1st y ) )
18 17 simplbi 
 |-  ( x ( 1st |` ( _V X. _V ) ) y -> x e. ( _V X. _V ) )
19 18 adantr 
 |-  ( ( x ( 1st |` ( _V X. _V ) ) y /\ y A z ) -> x e. ( _V X. _V ) )
20 19 exlimiv 
 |-  ( E. y ( x ( 1st |` ( _V X. _V ) ) y /\ y A z ) -> x e. ( _V X. _V ) )
21 15 20 sylbi 
 |-  ( x ( A o. ( 1st |` ( _V X. _V ) ) ) z -> x e. ( _V X. _V ) )
22 21 adantr 
 |-  ( ( x ( A o. ( 1st |` ( _V X. _V ) ) ) z /\ x ( B o. ( 2nd |` ( _V X. _V ) ) ) w ) -> x e. ( _V X. _V ) )
23 14 22 sylbi 
 |-  ( x ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) <. z , w >. -> x e. ( _V X. _V ) )
24 10 23 sylbir 
 |-  ( <. x , <. z , w >. >. e. ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) -> x e. ( _V X. _V ) )
25 9 24 syl6bi 
 |-  ( y = <. z , w >. -> ( <. x , y >. e. ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) -> x e. ( _V X. _V ) ) )
26 25 exlimivv 
 |-  ( E. z E. w y = <. z , w >. -> ( <. x , y >. e. ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) -> x e. ( _V X. _V ) ) )
27 7 26 sylbi 
 |-  ( y e. ( _V X. _V ) -> ( <. x , y >. e. ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) -> x e. ( _V X. _V ) ) )
28 6 27 mpcom 
 |-  ( <. x , y >. e. ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) -> x e. ( _V X. _V ) )
29 28 6 opelxpd 
 |-  ( <. x , y >. e. ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) -> <. x , y >. e. ( ( _V X. _V ) X. ( _V X. _V ) ) )
30 2 29 relssi 
 |-  ( ( A o. ( 1st |` ( _V X. _V ) ) ) (x) ( B o. ( 2nd |` ( _V X. _V ) ) ) ) C_ ( ( _V X. _V ) X. ( _V X. _V ) )
31 1 30 eqsstri 
 |-  pprod ( A , B ) C_ ( ( _V X. _V ) X. ( _V X. _V ) )