This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 , 𝐵 ) ⊆ ( ( 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 biimtrdi ⊢ ( 𝑦 = ⟨ 𝑧 , 𝑤 ⟩ → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∘ ( 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 ) )