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
|- ( A e. RR <-> ( ( 1st ` A ) e. R. /\ A = <. ( 1st ` A ) , 0R >. ) )

Proof

Step Hyp Ref Expression
1 df-r
 |-  RR = ( R. X. { 0R } )
2 1 eleq2i
 |-  ( A e. RR <-> A e. ( R. X. { 0R } ) )
3 xp1st
 |-  ( A e. ( R. X. { 0R } ) -> ( 1st ` A ) e. R. )
4 1st2nd2
 |-  ( A e. ( R. X. { 0R } ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
5 xp2nd
 |-  ( A e. ( R. X. { 0R } ) -> ( 2nd ` A ) e. { 0R } )
6 elsni
 |-  ( ( 2nd ` A ) e. { 0R } -> ( 2nd ` A ) = 0R )
7 5 6 syl
 |-  ( A e. ( R. X. { 0R } ) -> ( 2nd ` A ) = 0R )
8 7 opeq2d
 |-  ( A e. ( R. X. { 0R } ) -> <. ( 1st ` A ) , ( 2nd ` A ) >. = <. ( 1st ` A ) , 0R >. )
9 4 8 eqtrd
 |-  ( A e. ( R. X. { 0R } ) -> A = <. ( 1st ` A ) , 0R >. )
10 3 9 jca
 |-  ( A e. ( R. X. { 0R } ) -> ( ( 1st ` A ) e. R. /\ A = <. ( 1st ` A ) , 0R >. ) )
11 eleq1
 |-  ( A = <. ( 1st ` A ) , 0R >. -> ( A e. ( R. X. { 0R } ) <-> <. ( 1st ` A ) , 0R >. e. ( R. X. { 0R } ) ) )
12 0r
 |-  0R e. R.
13 12 elexi
 |-  0R e. _V
14 13 snid
 |-  0R e. { 0R }
15 opelxp
 |-  ( <. ( 1st ` A ) , 0R >. e. ( R. X. { 0R } ) <-> ( ( 1st ` A ) e. R. /\ 0R e. { 0R } ) )
16 14 15 mpbiran2
 |-  ( <. ( 1st ` A ) , 0R >. e. ( R. X. { 0R } ) <-> ( 1st ` A ) e. R. )
17 11 16 bitrdi
 |-  ( A = <. ( 1st ` A ) , 0R >. -> ( A e. ( R. X. { 0R } ) <-> ( 1st ` A ) e. R. ) )
18 17 biimparc
 |-  ( ( ( 1st ` A ) e. R. /\ A = <. ( 1st ` A ) , 0R >. ) -> A e. ( R. X. { 0R } ) )
19 10 18 impbii
 |-  ( A e. ( R. X. { 0R } ) <-> ( ( 1st ` A ) e. R. /\ A = <. ( 1st ` A ) , 0R >. ) )
20 2 19 bitri
 |-  ( A e. RR <-> ( ( 1st ` A ) e. R. /\ A = <. ( 1st ` A ) , 0R >. ) )