Step |
Hyp |
Ref |
Expression |
1 |
|
nqerf |
|- /Q : ( N. X. N. ) --> Q. |
2 |
|
addpqf |
|- +pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. ) |
3 |
|
fco |
|- ( ( /Q : ( N. X. N. ) --> Q. /\ +pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. ) ) -> ( /Q o. +pQ ) : ( ( N. X. N. ) X. ( N. X. N. ) ) --> Q. ) |
4 |
1 2 3
|
mp2an |
|- ( /Q o. +pQ ) : ( ( N. X. N. ) X. ( N. X. N. ) ) --> Q. |
5 |
|
elpqn |
|- ( x e. Q. -> x e. ( N. X. N. ) ) |
6 |
5
|
ssriv |
|- Q. C_ ( N. X. N. ) |
7 |
|
xpss12 |
|- ( ( Q. C_ ( N. X. N. ) /\ Q. C_ ( N. X. N. ) ) -> ( Q. X. Q. ) C_ ( ( N. X. N. ) X. ( N. X. N. ) ) ) |
8 |
6 6 7
|
mp2an |
|- ( Q. X. Q. ) C_ ( ( N. X. N. ) X. ( N. X. N. ) ) |
9 |
|
fssres |
|- ( ( ( /Q o. +pQ ) : ( ( N. X. N. ) X. ( N. X. N. ) ) --> Q. /\ ( Q. X. Q. ) C_ ( ( N. X. N. ) X. ( N. X. N. ) ) ) -> ( ( /Q o. +pQ ) |` ( Q. X. Q. ) ) : ( Q. X. Q. ) --> Q. ) |
10 |
4 8 9
|
mp2an |
|- ( ( /Q o. +pQ ) |` ( Q. X. Q. ) ) : ( Q. X. Q. ) --> Q. |
11 |
|
df-plq |
|- +Q = ( ( /Q o. +pQ ) |` ( Q. X. Q. ) ) |
12 |
11
|
feq1i |
|- ( +Q : ( Q. X. Q. ) --> Q. <-> ( ( /Q o. +pQ ) |` ( Q. X. Q. ) ) : ( Q. X. Q. ) --> Q. ) |
13 |
10 12
|
mpbir |
|- +Q : ( Q. X. Q. ) --> Q. |