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	⊢ 𝐼 = { 1 , 2 }
	prelrrx2.b	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
Assertion	prelrrx2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∈ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		prelrrx2.i	⊢ 𝐼 = { 1 , 2 }
2		prelrrx2.b	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
3		1ex	⊢ 1 ∈ V
4		2ex	⊢ 2 ∈ V
5	3 4	pm3.2i	⊢ ( 1 ∈ V ∧ 2 ∈ V )
6	5	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1 ∈ V ∧ 2 ∈ V ) )
7		id	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
8		1ne2	⊢ 1 ≠ 2
9	8	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 1 ≠ 2 )
10	6 7 9	3jca	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 1 ≠ 2 ) )
11		fprg	⊢ ( ( ( 1 ∈ V ∧ 2 ∈ V ) ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 1 ≠ 2 ) → { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : { 1 , 2 } ⟶ { 𝐴 , 𝐵 } )
12	10 11	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : { 1 , 2 } ⟶ { 𝐴 , 𝐵 } )
13		prssi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → { 𝐴 , 𝐵 } ⊆ ℝ )
14	12 13	fssd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : { 1 , 2 } ⟶ ℝ )
15		reex	⊢ ℝ ∈ V
16		prex	⊢ { 1 , 2 } ∈ V
17	15 16	pm3.2i	⊢ ( ℝ ∈ V ∧ { 1 , 2 } ∈ V )
18		elmapg	⊢ ( ( ℝ ∈ V ∧ { 1 , 2 } ∈ V ) → ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∈ ( ℝ ↑m { 1 , 2 } ) ↔ { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : { 1 , 2 } ⟶ ℝ ) )
19	17 18	ax-mp	⊢ ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∈ ( ℝ ↑m { 1 , 2 } ) ↔ { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : { 1 , 2 } ⟶ ℝ )
20	14 19	sylibr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∈ ( ℝ ↑m { 1 , 2 } ) )
21	1	oveq2i	⊢ ( ℝ ↑m 𝐼 ) = ( ℝ ↑m { 1 , 2 } )
22	2 21	eqtri	⊢ 𝑃 = ( ℝ ↑m { 1 , 2 } )
23	22	eleq2i	⊢ ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∈ 𝑃 ↔ { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∈ ( ℝ ↑m { 1 , 2 } ) )
24	20 23	sylibr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∈ 𝑃 )