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