Step |
Hyp |
Ref |
Expression |
1 |
|
1pr |
|- 1P e. P. |
2 |
|
addclpr |
|- ( ( 1P e. P. /\ 1P e. P. ) -> ( 1P +P. 1P ) e. P. ) |
3 |
1 1 2
|
mp2an |
|- ( 1P +P. 1P ) e. P. |
4 |
|
opelxpi |
|- ( ( ( 1P +P. 1P ) e. P. /\ 1P e. P. ) -> <. ( 1P +P. 1P ) , 1P >. e. ( P. X. P. ) ) |
5 |
3 1 4
|
mp2an |
|- <. ( 1P +P. 1P ) , 1P >. e. ( P. X. P. ) |
6 |
|
enrex |
|- ~R e. _V |
7 |
6
|
ecelqsi |
|- ( <. ( 1P +P. 1P ) , 1P >. e. ( P. X. P. ) -> [ <. ( 1P +P. 1P ) , 1P >. ] ~R e. ( ( P. X. P. ) /. ~R ) ) |
8 |
5 7
|
ax-mp |
|- [ <. ( 1P +P. 1P ) , 1P >. ] ~R e. ( ( P. X. P. ) /. ~R ) |
9 |
|
df-1r |
|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R |
10 |
|
df-nr |
|- R. = ( ( P. X. P. ) /. ~R ) |
11 |
8 9 10
|
3eltr4i |
|- 1R e. R. |