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

Metamath Proof Explorer

Theorem brpprod3a

Description: Condition for parallel product when the last argument is not an ordered pair. (Contributed by Scott Fenton, 11-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses brpprod3.1 ⊢ 𝑋 ∈ V
brpprod3.2 ⊢ 𝑌 ∈ V
brpprod3.3 ⊢ 𝑍 ∈ V
Assertion brpprod3a ( ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) 𝑍 ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑋 𝑅 𝑧 ∧ 𝑌 𝑆 𝑤 ) )

Proof

Step Hyp Ref Expression
1 brpprod3.1 ⊢ 𝑋 ∈ V
2 brpprod3.2 ⊢ 𝑌 ∈ V
3 brpprod3.3 ⊢ 𝑍 ∈ V
4 pprodss4v ⊢ pprod ( 𝑅 , 𝑆 ) ⊆ ( ( V × V ) × ( V × V ) )
5 4 brel ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) 𝑍 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( V × V ) ∧ 𝑍 ∈ ( V × V ) ) )
6 5 simprd ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) 𝑍 → 𝑍 ∈ ( V × V ) )
7 elvv ⊢ ( 𝑍 ∈ ( V × V ) ↔ ∃ 𝑧 ∃ 𝑤 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ )
8 6 7 sylib ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) 𝑍 → ∃ 𝑧 ∃ 𝑤 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ )
9 8 pm4.71ri ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) 𝑍 ↔ ( ∃ 𝑧 ∃ 𝑤 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) 𝑍 ) )
10 19.41vv ⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) 𝑍 ) ↔ ( ∃ 𝑧 ∃ 𝑤 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) 𝑍 ) )
11 9 10 bitr4i ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) 𝑍 ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) 𝑍 ) )
12 breq2 ⊢ ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ → ( ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) 𝑍 ↔ ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
13 12 pm5.32i ⊢ ( ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) 𝑍 ) ↔ ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
14 13 2exbii ⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) 𝑍 ) ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
15 vex ⊢ 𝑧 ∈ V
16 vex ⊢ 𝑤 ∈ V
17 1 2 15 16 brpprod ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) ⟨ 𝑧 , 𝑤 ⟩ ↔ ( 𝑋 𝑅 𝑧 ∧ 𝑌 𝑆 𝑤 ) )
18 17 anbi2i ⊢ ( ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ( 𝑋 𝑅 𝑧 ∧ 𝑌 𝑆 𝑤 ) ) )
19 3anass ⊢ ( ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑋 𝑅 𝑧 ∧ 𝑌 𝑆 𝑤 ) ↔ ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ( 𝑋 𝑅 𝑧 ∧ 𝑌 𝑆 𝑤 ) ) )
20 18 19 bitr4i ⊢ ( ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑋 𝑅 𝑧 ∧ 𝑌 𝑆 𝑤 ) )
21 20 2exbii ⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑋 𝑅 𝑧 ∧ 𝑌 𝑆 𝑤 ) )
22 11 14 21 3bitri ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ pprod ( 𝑅 , 𝑆 ) 𝑍 ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑍 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑋 𝑅 𝑧 ∧ 𝑌 𝑆 𝑤 ) )