Theorem prelrrx2

Description: A doubleton word of real numbers is a point in a real Euclidean space of dimension 2. (Contributed by AV, 4-Feb-2023)

	Ref	Expression
Hypotheses	prelrrx2.i	⊢ 𝐼 = ( 0 ..^ 2 )
	prelrrx2.b	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
Assertion	prelrrx2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ⟨“ 𝐴 𝐵 ”⟩ ∈ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		prelrrx2.i	⊢ 𝐼 = ( 0 ..^ 2 )
2		prelrrx2.b	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
3		reex	⊢ ℝ ∈ V
4	3	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ℝ ∈ V )
5		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
6		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
7	4 5 6	s2mapd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ⟨“ 𝐴 𝐵 ”⟩ ∈ ( ℝ ↑m ( 0 ..^ 2 ) ) )
8	1	oveq2i	⊢ ( ℝ ↑m 𝐼 ) = ( ℝ ↑m ( 0 ..^ 2 ) )
9	2 8	eqtri	⊢ 𝑃 = ( ℝ ↑m ( 0 ..^ 2 ) )
10	7 9	eleqtrrdi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ⟨“ 𝐴 𝐵 ”⟩ ∈ 𝑃 )