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

Metamath Proof Explorer

Theorem nqerid

Description: Corollary of nqereu : the function /Q acts as the identity on members of Q. . (Contributed by Mario Carneiro, 6-May-2013) (New usage is discouraged.)

Ref Expression
Assertion nqerid 
|- ( A e. Q. -> ( /Q ` A ) = A )

Proof

Step Hyp Ref Expression
1 nqerf 
 |-  /Q : ( N. X. N. ) --> Q.
2 ffun 
 |-  ( /Q : ( N. X. N. ) --> Q. -> Fun /Q )
3 1 2 ax-mp 
 |-  Fun /Q
4 elpqn 
 |-  ( A e. Q. -> A e. ( N. X. N. ) )
5 id 
 |-  ( A e. Q. -> A e. Q. )
6 enqer 
 |-  ~Q Er ( N. X. N. )
7 6 a1i 
 |-  ( A e. Q. -> ~Q Er ( N. X. N. ) )
8 7 4 erref 
 |-  ( A e. Q. -> A ~Q A )
9 df-erq 
 |-  /Q = ( ~Q i^i ( ( N. X. N. ) X. Q. ) )
10 9 breqi 
 |-  ( A /Q A <-> A ( ~Q i^i ( ( N. X. N. ) X. Q. ) ) A )
11 brinxp2 
 |-  ( A ( ~Q i^i ( ( N. X. N. ) X. Q. ) ) A <-> ( ( A e. ( N. X. N. ) /\ A e. Q. ) /\ A ~Q A ) )
12 10 11 bitri 
 |-  ( A /Q A <-> ( ( A e. ( N. X. N. ) /\ A e. Q. ) /\ A ~Q A ) )
13 4 5 8 12 syl21anbrc 
 |-  ( A e. Q. -> A /Q A )
14 funbrfv 
 |-  ( Fun /Q -> ( A /Q A -> ( /Q ` A ) = A ) )
15 3 13 14 mpsyl 
 |-  ( A e. Q. -> ( /Q ` A ) = A )