Metamath Proof Explorer

Theorem nqerf

Description: Corollary of nqereu : the function /Q is actually a function. (Contributed by Mario Carneiro, 6-May-2013) (New usage is discouraged.)

Ref Expression
Assertion nqerf 
|- /Q : ( N. X. N. ) --> Q.

Proof

Step Hyp Ref Expression
1 df-erq 
 |-  /Q = ( ~Q i^i ( ( N. X. N. ) X. Q. ) )
2 inss2 
 |-  ( ~Q i^i ( ( N. X. N. ) X. Q. ) ) C_ ( ( N. X. N. ) X. Q. )
3 1 2 eqsstri 
 |-  /Q C_ ( ( N. X. N. ) X. Q. )
4 xpss 
 |-  ( ( N. X. N. ) X. Q. ) C_ ( _V X. _V )
5 3 4 sstri 
 |-  /Q C_ ( _V X. _V )
6 df-rel 
 |-  ( Rel /Q <-> /Q C_ ( _V X. _V ) )
7 5 6 mpbir 
 |-  Rel /Q
8 nqereu 
 |-  ( x e. ( N. X. N. ) -> E! y e. Q. y ~Q x )
9 df-reu 
 |-  ( E! y e. Q. y ~Q x <-> E! y ( y e. Q. /\ y ~Q x ) )
10 eumo 
 |-  ( E! y ( y e. Q. /\ y ~Q x ) -> E* y ( y e. Q. /\ y ~Q x ) )
11 9 10 sylbi 
 |-  ( E! y e. Q. y ~Q x -> E* y ( y e. Q. /\ y ~Q x ) )
12 8 11 syl 
 |-  ( x e. ( N. X. N. ) -> E* y ( y e. Q. /\ y ~Q x ) )
13 moanimv 
 |-  ( E* y ( x e. ( N. X. N. ) /\ ( y e. Q. /\ y ~Q x ) ) <-> ( x e. ( N. X. N. ) -> E* y ( y e. Q. /\ y ~Q x ) ) )
14 12 13 mpbir 
 |-  E* y ( x e. ( N. X. N. ) /\ ( y e. Q. /\ y ~Q x ) )
15 3 brel 
 |-  ( x /Q y -> ( x e. ( N. X. N. ) /\ y e. Q. ) )
16 15 simpld 
 |-  ( x /Q y -> x e. ( N. X. N. ) )
17 15 simprd 
 |-  ( x /Q y -> y e. Q. )
18 enqer 
 |-  ~Q Er ( N. X. N. )
19 18 a1i 
 |-  ( x /Q y -> ~Q Er ( N. X. N. ) )
20 inss1 
 |-  ( ~Q i^i ( ( N. X. N. ) X. Q. ) ) C_ ~Q
21 1 20 eqsstri 
 |-  /Q C_ ~Q
22 21 ssbri 
 |-  ( x /Q y -> x ~Q y )
23 19 22 ersym 
 |-  ( x /Q y -> y ~Q x )
24 16 17 23 jca32 
 |-  ( x /Q y -> ( x e. ( N. X. N. ) /\ ( y e. Q. /\ y ~Q x ) ) )
25 24 moimi 
 |-  ( E* y ( x e. ( N. X. N. ) /\ ( y e. Q. /\ y ~Q x ) ) -> E* y x /Q y )
26 14 25 ax-mp 
 |-  E* y x /Q y
27 26 ax-gen 
 |-  A. x E* y x /Q y
28 dffun6 
 |-  ( Fun /Q <-> ( Rel /Q /\ A. x E* y x /Q y ) )
29 7 27 28 mpbir2an 
 |-  Fun /Q
30 dmss 
 |-  ( /Q C_ ( ( N. X. N. ) X. Q. ) -> dom /Q C_ dom ( ( N. X. N. ) X. Q. ) )
31 3 30 ax-mp 
 |-  dom /Q C_ dom ( ( N. X. N. ) X. Q. )
32 1nq 
 |-  1Q e. Q.
33 ne0i 
 |-  ( 1Q e. Q. -> Q. =/= (/) )
34 dmxp 
 |-  ( Q. =/= (/) -> dom ( ( N. X. N. ) X. Q. ) = ( N. X. N. ) )
35 32 33 34 mp2b 
 |-  dom ( ( N. X. N. ) X. Q. ) = ( N. X. N. )
36 31 35 sseqtri 
 |-  dom /Q C_ ( N. X. N. )
37 reurex 
 |-  ( E! y e. Q. y ~Q x -> E. y e. Q. y ~Q x )
38 simpll 
 |-  ( ( ( x e. ( N. X. N. ) /\ y e. Q. ) /\ y ~Q x ) -> x e. ( N. X. N. ) )
39 simplr 
 |-  ( ( ( x e. ( N. X. N. ) /\ y e. Q. ) /\ y ~Q x ) -> y e. Q. )
40 18 a1i 
 |-  ( ( ( x e. ( N. X. N. ) /\ y e. Q. ) /\ y ~Q x ) -> ~Q Er ( N. X. N. ) )
41 simpr 
 |-  ( ( ( x e. ( N. X. N. ) /\ y e. Q. ) /\ y ~Q x ) -> y ~Q x )
42 40 41 ersym 
 |-  ( ( ( x e. ( N. X. N. ) /\ y e. Q. ) /\ y ~Q x ) -> x ~Q y )
43 1 breqi 
 |-  ( x /Q y <-> x ( ~Q i^i ( ( N. X. N. ) X. Q. ) ) y )
44 brinxp2 
 |-  ( x ( ~Q i^i ( ( N. X. N. ) X. Q. ) ) y <-> ( ( x e. ( N. X. N. ) /\ y e. Q. ) /\ x ~Q y ) )
45 43 44 bitri 
 |-  ( x /Q y <-> ( ( x e. ( N. X. N. ) /\ y e. Q. ) /\ x ~Q y ) )
46 38 39 42 45 syl21anbrc 
 |-  ( ( ( x e. ( N. X. N. ) /\ y e. Q. ) /\ y ~Q x ) -> x /Q y )
47 46 ex 
 |-  ( ( x e. ( N. X. N. ) /\ y e. Q. ) -> ( y ~Q x -> x /Q y ) )
48 47 reximdva 
 |-  ( x e. ( N. X. N. ) -> ( E. y e. Q. y ~Q x -> E. y e. Q. x /Q y ) )
49 rexex 
 |-  ( E. y e. Q. x /Q y -> E. y x /Q y )
50 37 48 49 syl56 
 |-  ( x e. ( N. X. N. ) -> ( E! y e. Q. y ~Q x -> E. y x /Q y ) )
51 8 50 mpd 
 |-  ( x e. ( N. X. N. ) -> E. y x /Q y )
52 vex 
 |-  x e. _V
53 52 eldm 
 |-  ( x e. dom /Q <-> E. y x /Q y )
54 51 53 sylibr 
 |-  ( x e. ( N. X. N. ) -> x e. dom /Q )
55 54 ssriv 
 |-  ( N. X. N. ) C_ dom /Q
56 36 55 eqssi 
 |-  dom /Q = ( N. X. N. )
57 df-fn 
 |-  ( /Q Fn ( N. X. N. ) <-> ( Fun /Q /\ dom /Q = ( N. X. N. ) ) )
58 29 56 57 mpbir2an 
 |-  /Q Fn ( N. X. N. )
59 3 rnssi 
 |-  ran /Q C_ ran ( ( N. X. N. ) X. Q. )
60 rnxpss 
 |-  ran ( ( N. X. N. ) X. Q. ) C_ Q.
61 59 60 sstri 
 |-  ran /Q C_ Q.
62 df-f 
 |-  ( /Q : ( N. X. N. ) --> Q. <-> ( /Q Fn ( N. X. N. ) /\ ran /Q C_ Q. ) )
63 58 61 62 mpbir2an 
 |-  /Q : ( N. X. N. ) --> Q.