Metamath Proof Explorer

Theorem brpprod3b

Description: Condition for parallel product when the first argument is not an ordered pair. (Contributed by Scott Fenton, 3-May-2014)

Ref Expression
Hypotheses brpprod3.1 ⊢ X ∈ V
brpprod3.2 ⊢ Y ∈ V
brpprod3.3 ⊢ Z ∈ V
Assertion brpprod3b ⊢ X pprod R S Y Z ↔ ∃ z ∃ w X = z w ∧ z R Y ∧ w S Z

Proof

Step Hyp Ref Expression
1 brpprod3.1 ⊢ X ∈ V
2 brpprod3.2 ⊢ Y ∈ V
3 brpprod3.3 ⊢ Z ∈ V
4 pprodcnveq ⊢ pprod R S = pprod R -1 S -1 -1
5 4 breqi ⊢ X pprod R S Y Z ↔ X pprod R -1 S -1 -1 Y Z
6 opex ⊢ Y Z ∈ V
7 1 6 brcnv ⊢ X pprod R -1 S -1 -1 Y Z ↔ Y Z pprod R -1 S -1 X
8 2 3 1 brpprod3a ⊢ Y Z pprod R -1 S -1 X ↔ ∃ z ∃ w X = z w ∧ Y R -1 z ∧ Z S -1 w
9 7 8 bitri ⊢ X pprod R -1 S -1 -1 Y Z ↔ ∃ z ∃ w X = z w ∧ Y R -1 z ∧ Z S -1 w
10 biid ⊢ X = z w ↔ X = z w
11 vex ⊢ z ∈ V
12 2 11 brcnv ⊢ Y R -1 z ↔ z R Y
13 vex ⊢ w ∈ V
14 3 13 brcnv ⊢ Z S -1 w ↔ w S Z
15 10 12 14 3anbi123i ⊢ X = z w ∧ Y R -1 z ∧ Z S -1 w ↔ X = z w ∧ z R Y ∧ w S Z
16 15 2exbii ⊢ ∃ z ∃ w X = z w ∧ Y R -1 z ∧ Z S -1 w ↔ ∃ z ∃ w X = z w ∧ z R Y ∧ w S Z
17 9 16 bitri ⊢ X pprod R -1 S -1 -1 Y Z ↔ ∃ z ∃ w X = z w ∧ z R Y ∧ w S Z
18 5 17 bitri ⊢ X pprod R S Y Z ↔ ∃ z ∃ w X = z w ∧ z R Y ∧ w S Z