Theorem dmrecnq

Description: Domain of reciprocal on positive fractions. (Contributed by NM, 6-Mar-1996) (Revised by Mario Carneiro, 10-Jul-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	dmrecnq	|- dom *Q = Q.

Proof

Step	Hyp	Ref	Expression
1		df-rq	|- *Q = ( `' .Q " { 1Q } )
2		cnvimass	|- ( `' .Q " { 1Q } ) C_ dom .Q
3	1 2	eqsstri	|- *Q C_ dom .Q
4		mulnqf	|- .Q : ( Q. X. Q. ) --> Q.
5	4	fdmi	|- dom .Q = ( Q. X. Q. )
6	3 5	sseqtri	|- *Q C_ ( Q. X. Q. )
7		dmss	|- ( *Q C_ ( Q. X. Q. ) -> dom *Q C_ dom ( Q. X. Q. ) )
8	6 7	ax-mp	|- dom *Q C_ dom ( Q. X. Q. )
9		dmxpid	|- dom ( Q. X. Q. ) = Q.
10	8 9	sseqtri	|- dom *Q C_ Q.
11		recclnq	|- ( x e. Q. -> ( *Q ` x ) e. Q. )
12		opelxpi	|- ( ( x e. Q. /\ ( *Q ` x ) e. Q. ) -> <. x , ( *Q ` x ) >. e. ( Q. X. Q. ) )
13	11 12	mpdan	|- ( x e. Q. -> <. x , ( *Q ` x ) >. e. ( Q. X. Q. ) )
14		df-ov	|- ( x .Q ( *Q ` x ) ) = ( .Q ` <. x , ( *Q ` x ) >. )
15		recidnq	|- ( x e. Q. -> ( x .Q ( *Q ` x ) ) = 1Q )
16	14 15	eqtr3id	|- ( x e. Q. -> ( .Q ` <. x , ( *Q ` x ) >. ) = 1Q )
17		ffn	|- ( .Q : ( Q. X. Q. ) --> Q. -> .Q Fn ( Q. X. Q. ) )
18		fniniseg	|- ( .Q Fn ( Q. X. Q. ) -> ( <. x , ( *Q ` x ) >. e. ( `' .Q " { 1Q } ) <-> ( <. x , ( *Q ` x ) >. e. ( Q. X. Q. ) /\ ( .Q ` <. x , ( *Q ` x ) >. ) = 1Q ) ) )
19	4 17 18	mp2b	|- ( <. x , ( *Q ` x ) >. e. ( `' .Q " { 1Q } ) <-> ( <. x , ( *Q ` x ) >. e. ( Q. X. Q. ) /\ ( .Q ` <. x , ( *Q ` x ) >. ) = 1Q ) )
20	13 16 19	sylanbrc	|- ( x e. Q. -> <. x , ( *Q ` x ) >. e. ( `' .Q " { 1Q } ) )
21	20 1	eleqtrrdi	|- ( x e. Q. -> <. x , ( *Q ` x ) >. e. *Q )
22		df-br	|- ( x *Q ( *Q ` x ) <-> <. x , ( *Q ` x ) >. e. *Q )
23	21 22	sylibr	|- ( x e. Q. -> x *Q ( *Q ` x ) )
24		vex	|- x e. _V
25		fvex	|- ( *Q ` x ) e. _V
26	24 25	breldm	|- ( x *Q ( *Q ` x ) -> x e. dom *Q )
27	23 26	syl	|- ( x e. Q. -> x e. dom *Q )
28	27	ssriv	|- Q. C_ dom *Q
29	10 28	eqssi	|- dom *Q = Q.