Metamath Proof Explorer

Theorem addnqf

Description: Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995) (Revised by Mario Carneiro, 10-Jul-2014) (New usage is discouraged.)

Ref Expression
Assertion addnqf 
|- +Q : ( Q. X. Q. ) --> Q.

Proof

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.