This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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.