Theorem brprop

Description: Binary relation for a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023)

	Ref	Expression
Hypotheses	brprop.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	brprop.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	brprop.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	brprop.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
Assertion	brprop	⊢ ( 𝜑 → ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ↔ ( ( 𝑋 = 𝐴 ∧ 𝑌 = 𝐵 ) ∨ ( 𝑋 = 𝐶 ∧ 𝑌 = 𝐷 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		brprop.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		brprop.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		brprop.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4		brprop.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
5		df-pr	⊢ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } )
6	5	breqi	⊢ ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ↔ 𝑋 ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) 𝑌 )
7		brun	⊢ ( 𝑋 ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) 𝑌 ↔ ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ } 𝑌 ∨ 𝑋 { ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ) )
8	6 7	bitri	⊢ ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ↔ ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ } 𝑌 ∨ 𝑋 { ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ) )
9		brsnop	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ } 𝑌 ↔ ( 𝑋 = 𝐴 ∧ 𝑌 = 𝐵 ) ) )
10	1 2 9	syl2anc	⊢ ( 𝜑 → ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ } 𝑌 ↔ ( 𝑋 = 𝐴 ∧ 𝑌 = 𝐵 ) ) )
11		brsnop	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) → ( 𝑋 { ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ↔ ( 𝑋 = 𝐶 ∧ 𝑌 = 𝐷 ) ) )
12	3 4 11	syl2anc	⊢ ( 𝜑 → ( 𝑋 { ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ↔ ( 𝑋 = 𝐶 ∧ 𝑌 = 𝐷 ) ) )
13	10 12	orbi12d	⊢ ( 𝜑 → ( ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ } 𝑌 ∨ 𝑋 { ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ) ↔ ( ( 𝑋 = 𝐴 ∧ 𝑌 = 𝐵 ) ∨ ( 𝑋 = 𝐶 ∧ 𝑌 = 𝐷 ) ) ) )
14	8 13	bitrid	⊢ ( 𝜑 → ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ↔ ( ( 𝑋 = 𝐴 ∧ 𝑌 = 𝐵 ) ∨ ( 𝑋 = 𝐶 ∧ 𝑌 = 𝐷 ) ) ) )