Theorem 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 \left(1^{st}\left(A\right)\in 𝑹\wedge A=⟨1^{st}\left(A\right),0_{𝑹}⟩\right)$$

Proof

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