Theorem prelrrx2b

Description: Equivalent condition for being one of a pair of points in a real Euclidean space of dimension 2, determined by its coordinates. (Contributed by AV, 7-May-2023)

	Ref	Expression
Hypotheses	prelrrx2.i	⊢ 𝐼 = ( 0 ..^ 2 )
	prelrrx2.b	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
Assertion	prelrrx2b	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 0 ) = 𝐴 ∧ ( 𝑍 ‘ 1 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 0 ) = 𝑋 ∧ ( 𝑍 ‘ 1 ) = 𝑌 ) ) ) ↔ 𝑍 ∈ { ⟨“ 𝐴 𝐵 ”⟩ , ⟨“ 𝑋 𝑌 ”⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		prelrrx2.i	⊢ 𝐼 = ( 0 ..^ 2 )
2		prelrrx2.b	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
3		simpll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐴 ∈ ℝ )
4		simplr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐵 ∈ ℝ )
5	3 4	s2cld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ⟨“ 𝐴 𝐵 ”⟩ ∈ Word ℝ )
6		simprl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑋 ∈ ℝ )
7		simprr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑌 ∈ ℝ )
8	6 7	s2cld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ⟨“ 𝑋 𝑌 ”⟩ ∈ Word ℝ )
9		elpr2g	⊢ ( ( ⟨“ 𝐴 𝐵 ”⟩ ∈ Word ℝ ∧ ⟨“ 𝑋 𝑌 ”⟩ ∈ Word ℝ ) → ( 𝑍 ∈ { ⟨“ 𝐴 𝐵 ”⟩ , ⟨“ 𝑋 𝑌 ”⟩ } ↔ ( 𝑍 = ⟨“ 𝐴 𝐵 ”⟩ ∨ 𝑍 = ⟨“ 𝑋 𝑌 ”⟩ ) ) )
10	5 8 9	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑍 ∈ { ⟨“ 𝐴 𝐵 ”⟩ , ⟨“ 𝑋 𝑌 ”⟩ } ↔ ( 𝑍 = ⟨“ 𝐴 𝐵 ”⟩ ∨ 𝑍 = ⟨“ 𝑋 𝑌 ”⟩ ) ) )
11	1 2 3 4	prelrrx2bd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑍 = ⟨“ 𝐴 𝐵 ”⟩ ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑍 ‘ 0 ) = 𝐴 ∧ ( 𝑍 ‘ 1 ) = 𝐵 ) ) ) )
12	1 2 6 7	prelrrx2bd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑍 = ⟨“ 𝑋 𝑌 ”⟩ ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑍 ‘ 0 ) = 𝑋 ∧ ( 𝑍 ‘ 1 ) = 𝑌 ) ) ) )
13	11 12	orbi12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑍 = ⟨“ 𝐴 𝐵 ”⟩ ∨ 𝑍 = ⟨“ 𝑋 𝑌 ”⟩ ) ↔ ( ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑍 ‘ 0 ) = 𝐴 ∧ ( 𝑍 ‘ 1 ) = 𝐵 ) ) ∨ ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑍 ‘ 0 ) = 𝑋 ∧ ( 𝑍 ‘ 1 ) = 𝑌 ) ) ) ) )
14		andi	⊢ ( ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 0 ) = 𝐴 ∧ ( 𝑍 ‘ 1 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 0 ) = 𝑋 ∧ ( 𝑍 ‘ 1 ) = 𝑌 ) ) ) ↔ ( ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑍 ‘ 0 ) = 𝐴 ∧ ( 𝑍 ‘ 1 ) = 𝐵 ) ) ∨ ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑍 ‘ 0 ) = 𝑋 ∧ ( 𝑍 ‘ 1 ) = 𝑌 ) ) ) )
15	13 14	bitr4di	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑍 = ⟨“ 𝐴 𝐵 ”⟩ ∨ 𝑍 = ⟨“ 𝑋 𝑌 ”⟩ ) ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 0 ) = 𝐴 ∧ ( 𝑍 ‘ 1 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 0 ) = 𝑋 ∧ ( 𝑍 ‘ 1 ) = 𝑌 ) ) ) ) )
16	10 15	bitr2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑍 ∈ 𝑃 ∧ ( ( ( 𝑍 ‘ 0 ) = 𝐴 ∧ ( 𝑍 ‘ 1 ) = 𝐵 ) ∨ ( ( 𝑍 ‘ 0 ) = 𝑋 ∧ ( 𝑍 ‘ 1 ) = 𝑌 ) ) ) ↔ 𝑍 ∈ { ⟨“ 𝐴 𝐵 ”⟩ , ⟨“ 𝑋 𝑌 ”⟩ } ) )