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

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	⊢ 𝑋 ∈ V
		brpprod3.2	⊢ 𝑌 ∈ V
		brpprod3.3	⊢ 𝑍 ∈ V
	Assertion	brpprod3b	⊢ ( 𝑋 pprod ( 𝑅 , 𝑆 ) ⟨ 𝑌 , 𝑍 ⟩ ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑋 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑧 𝑅 𝑌 ∧ 𝑤 𝑆 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		brpprod3.1	⊢ 𝑋 ∈ V
2		brpprod3.2	⊢ 𝑌 ∈ V
3		brpprod3.3	⊢ 𝑍 ∈ V
4		pprodcnveq	⊢ pprod ( 𝑅 , 𝑆 ) = ^◡ pprod ( ^◡ 𝑅 , ^◡ 𝑆 )
5	4	breqi	⊢ ( 𝑋 pprod ( 𝑅 , 𝑆 ) ⟨ 𝑌 , 𝑍 ⟩ ↔ 𝑋 ^◡ pprod ( ^◡ 𝑅 , ^◡ 𝑆 ) ⟨ 𝑌 , 𝑍 ⟩ )
6		opex	⊢ ⟨ 𝑌 , 𝑍 ⟩ ∈ V
7	1 6	brcnv	⊢ ( 𝑋 ^◡ pprod ( ^◡ 𝑅 , ^◡ 𝑆 ) ⟨ 𝑌 , 𝑍 ⟩ ↔ ⟨ 𝑌 , 𝑍 ⟩ pprod ( ^◡ 𝑅 , ^◡ 𝑆 ) 𝑋 )
8	2 3 1	brpprod3a	⊢ ( ⟨ 𝑌 , 𝑍 ⟩ pprod ( ^◡ 𝑅 , ^◡ 𝑆 ) 𝑋 ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑋 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑌 ^◡ 𝑅 𝑧 ∧ 𝑍 ^◡ 𝑆 𝑤 ) )
9	7 8	bitri	⊢ ( 𝑋 ^◡ pprod ( ^◡ 𝑅 , ^◡ 𝑆 ) ⟨ 𝑌 , 𝑍 ⟩ ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑋 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑌 ^◡ 𝑅 𝑧 ∧ 𝑍 ^◡ 𝑆 𝑤 ) )
10		biid	⊢ ( 𝑋 = ⟨ 𝑧 , 𝑤 ⟩ ↔ 𝑋 = ⟨ 𝑧 , 𝑤 ⟩ )
11		vex	⊢ 𝑧 ∈ V
12	2 11	brcnv	⊢ ( 𝑌 ^◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝑌 )
13		vex	⊢ 𝑤 ∈ V
14	3 13	brcnv	⊢ ( 𝑍 ^◡ 𝑆 𝑤 ↔ 𝑤 𝑆 𝑍 )
15	10 12 14	3anbi123i	⊢ ( ( 𝑋 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑌 ^◡ 𝑅 𝑧 ∧ 𝑍 ^◡ 𝑆 𝑤 ) ↔ ( 𝑋 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑧 𝑅 𝑌 ∧ 𝑤 𝑆 𝑍 ) )
16	15	2exbii	⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑋 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑌 ^◡ 𝑅 𝑧 ∧ 𝑍 ^◡ 𝑆 𝑤 ) ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑋 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑧 𝑅 𝑌 ∧ 𝑤 𝑆 𝑍 ) )
17	9 16	bitri	⊢ ( 𝑋 ^◡ pprod ( ^◡ 𝑅 , ^◡ 𝑆 ) ⟨ 𝑌 , 𝑍 ⟩ ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑋 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑧 𝑅 𝑌 ∧ 𝑤 𝑆 𝑍 ) )
18	5 17	bitri	⊢ ( 𝑋 pprod ( 𝑅 , 𝑆 ) ⟨ 𝑌 , 𝑍 ⟩ ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑋 = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑧 𝑅 𝑌 ∧ 𝑤 𝑆 𝑍 ) )