elreal2

Description: Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	elreal2	$⊢ A \in ℝ \leftrightarrow (1^{st} (A) \in 𝑹 \land A = ⟨1^{st} (A), 0_{𝑹}⟩)$

Proof

Step	Hyp	Ref	Expression
1		df-r	$⊢ ℝ = 𝑹 \times \{0_{𝑹}\}$
2	1	eleq2i	$⊢ A \in ℝ \leftrightarrow A \in (𝑹 \times \{0_{𝑹}\})$
3		xp1st	$⊢ A \in (𝑹 \times \{0_{𝑹}\}) \to 1^{st} (A) \in 𝑹$
4		1st2nd2	$⊢ A \in (𝑹 \times \{0_{𝑹}\}) \to A = ⟨1^{st} (A), 2^{nd} (A)⟩$
5		xp2nd	$⊢ A \in (𝑹 \times \{0_{𝑹}\}) \to 2^{nd} (A) \in \{0_{𝑹}\}$
6		elsni	$⊢ 2^{nd} (A) \in \{0_{𝑹}\} \to 2^{nd} (A) = 0_{𝑹}$
7	5 6	syl	$⊢ A \in (𝑹 \times \{0_{𝑹}\}) \to 2^{nd} (A) = 0_{𝑹}$
8	7	opeq2d	$⊢ A \in (𝑹 \times \{0_{𝑹}\}) \to ⟨1^{st} (A), 2^{nd} (A)⟩ = ⟨1^{st} (A), 0_{𝑹}⟩$
9	4 8	eqtrd	$⊢ A \in (𝑹 \times \{0_{𝑹}\}) \to A = ⟨1^{st} (A), 0_{𝑹}⟩$
10	3 9	jca	$⊢ A \in (𝑹 \times \{0_{𝑹}\}) \to (1^{st} (A) \in 𝑹 \land A = ⟨1^{st} (A), 0_{𝑹}⟩)$
11		eleq1	$⊢ A = ⟨1^{st} (A), 0_{𝑹}⟩ \to (A \in (𝑹 \times \{0_{𝑹}\}) \leftrightarrow ⟨1^{st} (A), 0_{𝑹}⟩ \in (𝑹 \times \{0_{𝑹}\}))$
12		0r	$⊢ 0_{𝑹} \in 𝑹$
13	12	elexi	$⊢ 0_{𝑹} \in V$
14	13	snid	$⊢ 0_{𝑹} \in \{0_{𝑹}\}$
15		opelxp	$⊢ ⟨1^{st} (A), 0_{𝑹}⟩ \in (𝑹 \times \{0_{𝑹}\}) \leftrightarrow (1^{st} (A) \in 𝑹 \land 0_{𝑹} \in \{0_{𝑹}\})$
16	14 15	mpbiran2	$⊢ ⟨1^{st} (A), 0_{𝑹}⟩ \in (𝑹 \times \{0_{𝑹}\}) \leftrightarrow 1^{st} (A) \in 𝑹$
17	11 16	bitrdi	$⊢ A = ⟨1^{st} (A), 0_{𝑹}⟩ \to (A \in (𝑹 \times \{0_{𝑹}\}) \leftrightarrow 1^{st} (A) \in 𝑹)$
18	17	biimparc	$⊢ (1^{st} (A) \in 𝑹 \land A = ⟨1^{st} (A), 0_{𝑹}⟩) \to A \in (𝑹 \times \{0_{𝑹}\})$
19	10 18	impbii	$⊢ A \in (𝑹 \times \{0_{𝑹}\}) \leftrightarrow (1^{st} (A) \in 𝑹 \land A = ⟨1^{st} (A), 0_{𝑹}⟩)$
20	2 19	bitri	$⊢ A \in ℝ \leftrightarrow (1^{st} (A) \in 𝑹 \land A = ⟨1^{st} (A), 0_{𝑹}⟩)$

Metamath Proof Explorer

Theorem elreal2

Proof