This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 >. ) )