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 ( 𝐴 , 𝐵 ) ⟨ 𝑍 , 𝑊 ⟩ ↔ ( 𝑋 𝐴 𝑍 ∧ 𝑌 𝐵 𝑊 ) )