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 = \{1, 2\}$
	prelrrx2.b	$⊢ P = ℝ^{I}$
Assertion	prelrrx2	$⊢ (A \in ℝ \land B \in ℝ) \to \{⟨1, A⟩, ⟨2, B⟩\} \in P$

Proof

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

Metamath Proof Explorer

Theorem prelrrx2

Proof