Theorem mulnqf

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

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

Proof

Step	Hyp	Ref	Expression
1		nqerf	|- /Q : ( N. X. N. ) --> Q.
2		mulpqf	|- .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-mq	|- .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.