Metamath Proof Explorer


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 0RR
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 bitrdi ( 𝐴 = ⟨ ( 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 ⟩ ) )