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 ⊢ X ∈ V
brpprod3.2 ⊢ Y ∈ V
brpprod3.3 ⊢ Z ∈ V
Assertion brpprod3a ⊢ X Y pprod R S Z ↔ ∃ z ∃ w Z = z w ∧ X R z ∧ Y S w

Proof

Step Hyp Ref Expression
1 brpprod3.1 ⊢ X ∈ V
2 brpprod3.2 ⊢ Y ∈ V
3 brpprod3.3 ⊢ Z ∈ V
4 pprodss4v ⊢ pprod R S ⊆ V × V × V × V
5 4 brel ⊢ X Y pprod R S Z → X Y ∈ V × V ∧ Z ∈ V × V
6 5 simprd ⊢ X Y pprod R S Z → Z ∈ V × V
7 elvv ⊢ Z ∈ V × V ↔ ∃ z ∃ w Z = z w
8 6 7 sylib ⊢ X Y pprod R S Z → ∃ z ∃ w Z = z w
9 8 pm4.71ri ⊢ X Y pprod R S Z ↔ ∃ z ∃ w Z = z w ∧ X Y pprod R S Z
10 19.41vv ⊢ ∃ z ∃ w Z = z w ∧ X Y pprod R S Z ↔ ∃ z ∃ w Z = z w ∧ X Y pprod R S Z
11 9 10 bitr4i ⊢ X Y pprod R S Z ↔ ∃ z ∃ w Z = z w ∧ X Y pprod R S Z
12 breq2 ⊢ Z = z w → X Y pprod R S Z ↔ X Y pprod R S z w
13 12 pm5.32i ⊢ Z = z w ∧ X Y pprod R S Z ↔ Z = z w ∧ X Y pprod R S z w
14 13 2exbii ⊢ ∃ z ∃ w Z = z w ∧ X Y pprod R S Z ↔ ∃ z ∃ w Z = z w ∧ X Y pprod R S z w
15 vex ⊢ z ∈ V
16 vex ⊢ w ∈ V
17 1 2 15 16 brpprod ⊢ X Y pprod R S z w ↔ X R z ∧ Y S w
18 17 anbi2i ⊢ Z = z w ∧ X Y pprod R S z w ↔ Z = z w ∧ X R z ∧ Y S w
19 3anass ⊢ Z = z w ∧ X R z ∧ Y S w ↔ Z = z w ∧ X R z ∧ Y S w
20 18 19 bitr4i ⊢ Z = z w ∧ X Y pprod R S z w ↔ Z = z w ∧ X R z ∧ Y S w
21 20 2exbii ⊢ ∃ z ∃ w Z = z w ∧ X Y pprod R S z w ↔ ∃ z ∃ w Z = z w ∧ X R z ∧ Y S w
22 11 14 21 3bitri ⊢ X Y pprod R S Z ↔ ∃ z ∃ w Z = z w ∧ X R z ∧ Y S w