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 ( 𝐴 , 𝐵 ) ⊆ ( ( V × V ) × ( V × V ) )

Proof

Step	Hyp	Ref	Expression
1		df-pprod	⊢ pprod ( 𝐴 , 𝐵 ) = ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) )
2		txprel	⊢ Rel ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) )
3		txpss3v	⊢ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) ⊆ ( V × ( V × V ) )
4	3	sseli	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V × ( V × V ) ) )
5		opelxp2	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V × ( V × V ) ) → 𝑦 ∈ ( V × V ) )
6	4 5	syl	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) → 𝑦 ∈ ( V × V ) )
7		elvv	⊢ ( 𝑦 ∈ ( V × V ) ↔ ∃ 𝑧 ∃ 𝑤 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ )
8		opeq2	⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , ⟨ 𝑧 , 𝑤 ⟩ ⟩ )
9	8	eleq1d	⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) ↔ ⟨ 𝑥 , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∈ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) ) )
10		df-br	⊢ ( 𝑥 ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) ⟨ 𝑧 , 𝑤 ⟩ ↔ ⟨ 𝑥 , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∈ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) )
11		vex	⊢ 𝑥 ∈ V
12		vex	⊢ 𝑧 ∈ V
13		vex	⊢ 𝑤 ∈ V
14	11 12 13	brtxp	⊢ ( 𝑥 ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) ⟨ 𝑧 , 𝑤 ⟩ ↔ ( 𝑥 ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) 𝑧 ∧ 𝑥 ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) 𝑤 ) )
15	11 12	brco	⊢ ( 𝑥 ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) 𝑧 ↔ ∃ 𝑦 ( 𝑥 ( 1st ↾ ( V × V ) ) 𝑦 ∧ 𝑦 𝐴 𝑧 ) )
16		vex	⊢ 𝑦 ∈ V
17	16	brresi	⊢ ( 𝑥 ( 1st ↾ ( V × V ) ) 𝑦 ↔ ( 𝑥 ∈ ( V × V ) ∧ 𝑥 1st 𝑦 ) )
18	17	simplbi	⊢ ( 𝑥 ( 1st ↾ ( V × V ) ) 𝑦 → 𝑥 ∈ ( V × V ) )
19	18	adantr	⊢ ( ( 𝑥 ( 1st ↾ ( V × V ) ) 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 ∈ ( V × V ) )
20	19	exlimiv	⊢ ( ∃ 𝑦 ( 𝑥 ( 1st ↾ ( V × V ) ) 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 ∈ ( V × V ) )
21	15 20	sylbi	⊢ ( 𝑥 ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) 𝑧 → 𝑥 ∈ ( V × V ) )
22	21	adantr	⊢ ( ( 𝑥 ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) 𝑧 ∧ 𝑥 ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) 𝑤 ) → 𝑥 ∈ ( V × V ) )
23	14 22	sylbi	⊢ ( 𝑥 ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) ⟨ 𝑧 , 𝑤 ⟩ → 𝑥 ∈ ( V × V ) )
24	10 23	sylbir	⊢ ( ⟨ 𝑥 , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∈ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) → 𝑥 ∈ ( V × V ) )
25	9 24	syl6bi	⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) → 𝑥 ∈ ( V × V ) ) )
26	25	exlimivv	⊢ ( ∃ 𝑧 ∃ 𝑤 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) → 𝑥 ∈ ( V × V ) ) )
27	7 26	sylbi	⊢ ( 𝑦 ∈ ( V × V ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) → 𝑥 ∈ ( V × V ) ) )
28	6 27	mpcom	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) → 𝑥 ∈ ( V × V ) )
29	28 6	opelxpd	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( V × V ) × ( V × V ) ) )
30	2 29	relssi	⊢ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) ⊆ ( ( V × V ) × ( V × V ) )
31	1 30	eqsstri	⊢ pprod ( 𝐴 , 𝐵 ) ⊆ ( ( V × V ) × ( V × V ) )