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 V × V × V × V

Proof

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