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