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

Proof

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

Metamath Proof Explorer

Theorem elreal2

Proof