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) \subseteq (V \times V) \times (V \times V)$

Proof

Step	Hyp	Ref	Expression
1		df-pprod	$⊢ pprod (A, B) = ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)})))$
2		txprel	$⊢ Rel ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)})))$
3		txpss3v	$⊢ ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) \subseteq V \times (V \times V)$
4	3	sseli	$⊢ ⟨x, y⟩ \in ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) \to ⟨x, y⟩ \in (V \times (V \times V))$
5		opelxp2	$⊢ ⟨x, y⟩ \in (V \times (V \times V)) \to y \in (V \times V)$
6	4 5	syl	$⊢ ⟨x, y⟩ \in ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) \to y \in (V \times V)$
7		elvv	$⊢ y \in (V \times V) \leftrightarrow \exists z \exists w y = ⟨z, w⟩$
8		opeq2	$⊢ y = ⟨z, w⟩ \to ⟨x, y⟩ = ⟨x, ⟨z, w⟩⟩$
9	8	eleq1d	$⊢ y = ⟨z, w⟩ \to (⟨x, y⟩ \in ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) \leftrightarrow ⟨x, ⟨z, w⟩⟩ \in ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))))$
10		df-br	$⊢ x ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) ⟨z, w⟩ \leftrightarrow ⟨x, ⟨z, w⟩⟩ \in ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)})))$
11		vex	$⊢ x \in V$
12		vex	$⊢ z \in V$
13		vex	$⊢ w \in V$
14	11 12 13	brtxp	$⊢ x ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) ⟨z, w⟩ \leftrightarrow (x (A \circ ({1^{st} ↾}_{(V \times V)})) z \land x (B \circ ({2^{nd} ↾}_{(V \times V)})) w)$
15	11 12	brco	$⊢ x (A \circ ({1^{st} ↾}_{(V \times V)})) z \leftrightarrow \exists y (x ({1^{st} ↾}_{(V \times V)}) y \land y A z)$
16		vex	$⊢ y \in V$
17	16	brresi	$⊢ x ({1^{st} ↾}_{(V \times V)}) y \leftrightarrow (x \in (V \times V) \land x 1^{st} y)$
18	17	simplbi	$⊢ x ({1^{st} ↾}_{(V \times V)}) y \to x \in (V \times V)$
19	18	adantr	$⊢ (x ({1^{st} ↾}_{(V \times V)}) y \land y A z) \to x \in (V \times V)$
20	19	exlimiv	$⊢ \exists y (x ({1^{st} ↾}_{(V \times V)}) y \land y A z) \to x \in (V \times V)$
21	15 20	sylbi	$⊢ x (A \circ ({1^{st} ↾}_{(V \times V)})) z \to x \in (V \times V)$
22	21	adantr	$⊢ (x (A \circ ({1^{st} ↾}_{(V \times V)})) z \land x (B \circ ({2^{nd} ↾}_{(V \times V)})) w) \to x \in (V \times V)$
23	14 22	sylbi	$⊢ x ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) ⟨z, w⟩ \to x \in (V \times V)$
24	10 23	sylbir	$⊢ ⟨x, ⟨z, w⟩⟩ \in ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) \to x \in (V \times V)$
25	9 24	syl6bi	$⊢ y = ⟨z, w⟩ \to (⟨x, y⟩ \in ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) \to x \in (V \times V))$
26	25	exlimivv	$⊢ \exists z \exists w y = ⟨z, w⟩ \to (⟨x, y⟩ \in ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) \to x \in (V \times V))$
27	7 26	sylbi	$⊢ y \in (V \times V) \to (⟨x, y⟩ \in ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) \to x \in (V \times V))$
28	6 27	mpcom	$⊢ ⟨x, y⟩ \in ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) \to x \in (V \times V)$
29	28 6	opelxpd	$⊢ ⟨x, y⟩ \in ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) \to ⟨x, y⟩ \in ((V \times V) \times (V \times V))$
30	2 29	relssi	$⊢ ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) \subseteq (V \times V) \times (V \times V)$
31	1 30	eqsstri	$⊢ pprod (A, B) \subseteq (V \times V) \times (V \times V)$

Metamath Proof Explorer

Theorem pprodss4v

Proof