# Metamath Proof Explorer

## Theorem prelrrx2

Description: An unordered pair of ordered pairs with first components 1 and 2 and real numbers as second components is a point in a real Euclidean space of dimension 2. (Contributed by AV, 4-Feb-2023)

Ref Expression
Hypotheses prelrrx2.i ${⊢}{I}=\left\{1,2\right\}$
prelrrx2.b ${⊢}{P}={ℝ}^{{I}}$
Assertion prelrrx2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left\{⟨1,{A}⟩,⟨2,{B}⟩\right\}\in {P}$

### Proof

Step Hyp Ref Expression
1 prelrrx2.i ${⊢}{I}=\left\{1,2\right\}$
2 prelrrx2.b ${⊢}{P}={ℝ}^{{I}}$
3 1ex ${⊢}1\in \mathrm{V}$
4 2ex ${⊢}2\in \mathrm{V}$
5 3 4 pm3.2i ${⊢}\left(1\in \mathrm{V}\wedge 2\in \mathrm{V}\right)$
6 5 a1i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(1\in \mathrm{V}\wedge 2\in \mathrm{V}\right)$
7 id ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}\in ℝ\wedge {B}\in ℝ\right)$
8 1ne2 ${⊢}1\ne 2$
9 8 a1i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to 1\ne 2$
10 6 7 9 3jca ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left(1\in \mathrm{V}\wedge 2\in \mathrm{V}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge 1\ne 2\right)$
11 fprg ${⊢}\left(\left(1\in \mathrm{V}\wedge 2\in \mathrm{V}\right)\wedge \left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge 1\ne 2\right)\to \left\{⟨1,{A}⟩,⟨2,{B}⟩\right\}:\left\{1,2\right\}⟶\left\{{A},{B}\right\}$
12 10 11 syl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left\{⟨1,{A}⟩,⟨2,{B}⟩\right\}:\left\{1,2\right\}⟶\left\{{A},{B}\right\}$
13 prssi ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left\{{A},{B}\right\}\subseteq ℝ$
14 12 13 fssd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left\{⟨1,{A}⟩,⟨2,{B}⟩\right\}:\left\{1,2\right\}⟶ℝ$
15 reex ${⊢}ℝ\in \mathrm{V}$
16 prex ${⊢}\left\{1,2\right\}\in \mathrm{V}$
17 15 16 pm3.2i ${⊢}\left(ℝ\in \mathrm{V}\wedge \left\{1,2\right\}\in \mathrm{V}\right)$
18 elmapg ${⊢}\left(ℝ\in \mathrm{V}\wedge \left\{1,2\right\}\in \mathrm{V}\right)\to \left(\left\{⟨1,{A}⟩,⟨2,{B}⟩\right\}\in \left({ℝ}^{\left\{1,2\right\}}\right)↔\left\{⟨1,{A}⟩,⟨2,{B}⟩\right\}:\left\{1,2\right\}⟶ℝ\right)$
19 17 18 ax-mp ${⊢}\left\{⟨1,{A}⟩,⟨2,{B}⟩\right\}\in \left({ℝ}^{\left\{1,2\right\}}\right)↔\left\{⟨1,{A}⟩,⟨2,{B}⟩\right\}:\left\{1,2\right\}⟶ℝ$
20 14 19 sylibr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left\{⟨1,{A}⟩,⟨2,{B}⟩\right\}\in \left({ℝ}^{\left\{1,2\right\}}\right)$
21 1 oveq2i ${⊢}{ℝ}^{{I}}={ℝ}^{\left\{1,2\right\}}$
22 2 21 eqtri ${⊢}{P}={ℝ}^{\left\{1,2\right\}}$
23 22 eleq2i ${⊢}\left\{⟨1,{A}⟩,⟨2,{B}⟩\right\}\in {P}↔\left\{⟨1,{A}⟩,⟨2,{B}⟩\right\}\in \left({ℝ}^{\left\{1,2\right\}}\right)$
24 20 23 sylibr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left\{⟨1,{A}⟩,⟨2,{B}⟩\right\}\in {P}$