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	⊢ ( 𝐴 ∈ ℝ ↔ ( ( 1st ‘ 𝐴 ) ∈ R ∧ 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , 0R ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		df-r	⊢ ℝ = ( R × { 0R } )
2	1	eleq2i	⊢ ( 𝐴 ∈ ℝ ↔ 𝐴 ∈ ( R × { 0R } ) )
3		xp1st	⊢ ( 𝐴 ∈ ( R × { 0R } ) → ( 1st ‘ 𝐴 ) ∈ R )
4		1st2nd2	⊢ ( 𝐴 ∈ ( R × { 0R } ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
5		xp2nd	⊢ ( 𝐴 ∈ ( R × { 0R } ) → ( 2nd ‘ 𝐴 ) ∈ { 0R } )
6		elsni	⊢ ( ( 2nd ‘ 𝐴 ) ∈ { 0R } → ( 2nd ‘ 𝐴 ) = 0R )
7	5 6	syl	⊢ ( 𝐴 ∈ ( R × { 0R } ) → ( 2nd ‘ 𝐴 ) = 0R )
8	7	opeq2d	⊢ ( 𝐴 ∈ ( R × { 0R } ) → ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ = ⟨ ( 1st ‘ 𝐴 ) , 0R ⟩ )
9	4 8	eqtrd	⊢ ( 𝐴 ∈ ( R × { 0R } ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , 0R ⟩ )
10	3 9	jca	⊢ ( 𝐴 ∈ ( R × { 0R } ) → ( ( 1st ‘ 𝐴 ) ∈ R ∧ 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , 0R ⟩ ) )
11		eleq1	⊢ ( 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , 0R ⟩ → ( 𝐴 ∈ ( R × { 0R } ) ↔ ⟨ ( 1st ‘ 𝐴 ) , 0R ⟩ ∈ ( R × { 0R } ) ) )
12		0r	⊢ 0R ∈ R
13	12	elexi	⊢ 0R ∈ V
14	13	snid	⊢ 0R ∈ { 0R }
15		opelxp	⊢ ( ⟨ ( 1st ‘ 𝐴 ) , 0R ⟩ ∈ ( R × { 0R } ) ↔ ( ( 1st ‘ 𝐴 ) ∈ R ∧ 0R ∈ { 0R } ) )
16	14 15	mpbiran2	⊢ ( ⟨ ( 1st ‘ 𝐴 ) , 0R ⟩ ∈ ( R × { 0R } ) ↔ ( 1st ‘ 𝐴 ) ∈ R )
17	11 16	syl6bb	⊢ ( 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , 0R ⟩ → ( 𝐴 ∈ ( R × { 0R } ) ↔ ( 1st ‘ 𝐴 ) ∈ R ) )
18	17	biimparc	⊢ ( ( ( 1st ‘ 𝐴 ) ∈ R ∧ 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , 0R ⟩ ) → 𝐴 ∈ ( R × { 0R } ) )
19	10 18	impbii	⊢ ( 𝐴 ∈ ( R × { 0R } ) ↔ ( ( 1st ‘ 𝐴 ) ∈ R ∧ 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , 0R ⟩ ) )
20	2 19	bitri	⊢ ( 𝐴 ∈ ℝ ↔ ( ( 1st ‘ 𝐴 ) ∈ R ∧ 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , 0R ⟩ ) )