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

Metamath Proof Explorer

Theorem nqerrel

Description: Any member of ( N. X. N. ) relates to the representative of its equivalence class. (Contributed by Mario Carneiro, 6-May-2013) (New usage is discouraged.)

Ref Expression
Assertion nqerrel 
|- ( A e. ( N. X. N. ) -> A ~Q ( /Q ` A ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( /Q ` A ) = ( /Q ` A )
2 nqerf 
 |-  /Q : ( N. X. N. ) --> Q.
3 ffn 
 |-  ( /Q : ( N. X. N. ) --> Q. -> /Q Fn ( N. X. N. ) )
4 2 3 ax-mp 
 |-  /Q Fn ( N. X. N. )
5 fnbrfvb 
 |-  ( ( /Q Fn ( N. X. N. ) /\ A e. ( N. X. N. ) ) -> ( ( /Q ` A ) = ( /Q ` A ) <-> A /Q ( /Q ` A ) ) )
6 4 5 mpan 
 |-  ( A e. ( N. X. N. ) -> ( ( /Q ` A ) = ( /Q ` A ) <-> A /Q ( /Q ` A ) ) )
7 1 6 mpbii 
 |-  ( A e. ( N. X. N. ) -> A /Q ( /Q ` A ) )
8 df-erq 
 |-  /Q = ( ~Q i^i ( ( N. X. N. ) X. Q. ) )
9 inss1 
 |-  ( ~Q i^i ( ( N. X. N. ) X. Q. ) ) C_ ~Q
10 8 9 eqsstri 
 |-  /Q C_ ~Q
11 10 ssbri 
 |-  ( A /Q ( /Q ` A ) -> A ~Q ( /Q ` A ) )
12 7 11 syl 
 |-  ( A e. ( N. X. N. ) -> A ~Q ( /Q ` A ) )