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

Metamath Proof Explorer

Theorem brpprod

Description: Characterize a quaternary relation over a tail Cartesian product. Together with pprodss4v , this completely defines membership in a parallel product. (Contributed by Scott Fenton, 11-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses brpprod.1 ⊢ 𝑋 ∈ V
brpprod.2 ⊢ 𝑌 ∈ V
brpprod.3 ⊢ 𝑍 ∈ V
brpprod.4 ⊢ 𝑊 ∈ V
Assertion brpprod ( ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝐴 , 𝐵 ) ⟨ 𝑍 , 𝑊 ⟩ ↔ ( 𝑋 𝐴 𝑍 ∧ 𝑌 𝐵 𝑊 ) )

Proof

Step Hyp Ref Expression
1 brpprod.1 ⊢ 𝑋 ∈ V
2 brpprod.2 ⊢ 𝑌 ∈ V
3 brpprod.3 ⊢ 𝑍 ∈ V
4 brpprod.4 ⊢ 𝑊 ∈ V
5 df-pprod ⊢ pprod ( 𝐴 , 𝐵 ) = ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) )
6 5 breqi ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝐴 , 𝐵 ) ⟨ 𝑍 , 𝑊 ⟩ ↔ ⟨ 𝑋 , 𝑌 ⟩ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) ⟨ 𝑍 , 𝑊 ⟩ )
7 opex ⊢ ⟨ 𝑋 , 𝑌 ⟩ ∈ V
8 7 3 4 brtxp ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ( ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) ⊗ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ↔ ( ⟨ 𝑋 , 𝑌 ⟩ ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) 𝑍 ∧ ⟨ 𝑋 , 𝑌 ⟩ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) 𝑊 ) )
9 7 3 brco ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) 𝑍 ↔ ∃ 𝑥 ( ⟨ 𝑋 , 𝑌 ⟩ ( 1st ↾ ( V × V ) ) 𝑥 ∧ 𝑥 𝐴 𝑍 ) )
10 1 2 opelvv ⊢ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( V × V )
11 vex ⊢ 𝑥 ∈ V
12 11 brresi ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ( 1st ↾ ( V × V ) ) 𝑥 ↔ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( V × V ) ∧ ⟨ 𝑋 , 𝑌 ⟩ 1st 𝑥 ) )
13 10 12 mpbiran ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ( 1st ↾ ( V × V ) ) 𝑥 ↔ ⟨ 𝑋 , 𝑌 ⟩ 1st 𝑥 )
14 1 2 br1steq ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ 1st 𝑥 ↔ 𝑥 = 𝑋 )
15 13 14 bitri ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ( 1st ↾ ( V × V ) ) 𝑥 ↔ 𝑥 = 𝑋 )
16 15 anbi1i ⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 1st ↾ ( V × V ) ) 𝑥 ∧ 𝑥 𝐴 𝑍 ) ↔ ( 𝑥 = 𝑋 ∧ 𝑥 𝐴 𝑍 ) )
17 16 exbii ⊢ ( ∃ 𝑥 ( ⟨ 𝑋 , 𝑌 ⟩ ( 1st ↾ ( V × V ) ) 𝑥 ∧ 𝑥 𝐴 𝑍 ) ↔ ∃ 𝑥 ( 𝑥 = 𝑋 ∧ 𝑥 𝐴 𝑍 ) )
18 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐴 𝑍 ↔ 𝑋 𝐴 𝑍 ) )
19 1 18 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = 𝑋 ∧ 𝑥 𝐴 𝑍 ) ↔ 𝑋 𝐴 𝑍 )
20 9 17 19 3bitri ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) 𝑍 ↔ 𝑋 𝐴 𝑍 )
21 7 4 brco ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) 𝑊 ↔ ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ↾ ( V × V ) ) 𝑦 ∧ 𝑦 𝐵 𝑊 ) )
22 vex ⊢ 𝑦 ∈ V
23 22 brresi ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ↾ ( V × V ) ) 𝑦 ↔ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( V × V ) ∧ ⟨ 𝑋 , 𝑌 ⟩ 2nd 𝑦 ) )
24 10 23 mpbiran ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ↾ ( V × V ) ) 𝑦 ↔ ⟨ 𝑋 , 𝑌 ⟩ 2nd 𝑦 )
25 1 2 br2ndeq ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ 2nd 𝑦 ↔ 𝑦 = 𝑌 )
26 24 25 bitri ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ↾ ( V × V ) ) 𝑦 ↔ 𝑦 = 𝑌 )
27 26 anbi1i ⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ↾ ( V × V ) ) 𝑦 ∧ 𝑦 𝐵 𝑊 ) ↔ ( 𝑦 = 𝑌 ∧ 𝑦 𝐵 𝑊 ) )
28 27 exbii ⊢ ( ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ↾ ( V × V ) ) 𝑦 ∧ 𝑦 𝐵 𝑊 ) ↔ ∃ 𝑦 ( 𝑦 = 𝑌 ∧ 𝑦 𝐵 𝑊 ) )
29 breq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 𝐵 𝑊 ↔ 𝑌 𝐵 𝑊 ) )
30 2 29 ceqsexv ⊢ ( ∃ 𝑦 ( 𝑦 = 𝑌 ∧ 𝑦 𝐵 𝑊 ) ↔ 𝑌 𝐵 𝑊 )
31 21 28 30 3bitri ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) 𝑊 ↔ 𝑌 𝐵 𝑊 )
32 20 31 anbi12i ⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 𝐴 ∘ ( 1st ↾ ( V × V ) ) ) 𝑍 ∧ ⟨ 𝑋 , 𝑌 ⟩ ( 𝐵 ∘ ( 2nd ↾ ( V × V ) ) ) 𝑊 ) ↔ ( 𝑋 𝐴 𝑍 ∧ 𝑌 𝐵 𝑊 ) )
33 6 8 32 3bitri ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝐴 , 𝐵 ) ⟨ 𝑍 , 𝑊 ⟩ ↔ ( 𝑋 𝐴 𝑍 ∧ 𝑌 𝐵 𝑊 ) )