Metamath Proof Explorer

Theorem nqereu

Description: There is a unique element of Q. equivalent to each element of N. X. N. . (Contributed by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion nqereu 
|- ( A e. ( N. X. N. ) -> E! x e. Q. x ~Q A )

Proof

Step Hyp Ref Expression
1 elxp2 
 |-  ( A e. ( N. X. N. ) <-> E. a e. N. E. b e. N. A = <. a , b >. )
2 pion 
 |-  ( b e. N. -> b e. On )
3 onsuc 
 |-  ( b e. On -> suc b e. On )
4 2 3 syl 
 |-  ( b e. N. -> suc b e. On )
5 vex 
 |-  b e. _V
6 5 sucid 
 |-  b e. suc b
7 eleq2 
 |-  ( y = suc b -> ( b e. y <-> b e. suc b ) )
8 7 rspcev 
 |-  ( ( suc b e. On /\ b e. suc b ) -> E. y e. On b e. y )
9 4 6 8 sylancl 
 |-  ( b e. N. -> E. y e. On b e. y )
10 9 adantl 
 |-  ( ( a e. N. /\ b e. N. ) -> E. y e. On b e. y )
11 elequ2 
 |-  ( y = m -> ( b e. y <-> b e. m ) )
12 11 imbi1d 
 |-  ( y = m -> ( ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) <-> ( b e. m -> E. x e. Q. x ~Q <. a , b >. ) ) )
13 12 2ralbidv 
 |-  ( y = m -> ( A. a e. N. A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) <-> A. a e. N. A. b e. N. ( b e. m -> E. x e. Q. x ~Q <. a , b >. ) ) )
14 opeq1 
 |-  ( c = a -> <. c , d >. = <. a , d >. )
15 14 breq2d 
 |-  ( c = a -> ( x ~Q <. c , d >. <-> x ~Q <. a , d >. ) )
16 15 rexbidv 
 |-  ( c = a -> ( E. x e. Q. x ~Q <. c , d >. <-> E. x e. Q. x ~Q <. a , d >. ) )
17 16 imbi2d 
 |-  ( c = a -> ( ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) <-> ( d e. m -> E. x e. Q. x ~Q <. a , d >. ) ) )
18 elequ1 
 |-  ( d = b -> ( d e. m <-> b e. m ) )
19 opeq2 
 |-  ( d = b -> <. a , d >. = <. a , b >. )
20 19 breq2d 
 |-  ( d = b -> ( x ~Q <. a , d >. <-> x ~Q <. a , b >. ) )
21 20 rexbidv 
 |-  ( d = b -> ( E. x e. Q. x ~Q <. a , d >. <-> E. x e. Q. x ~Q <. a , b >. ) )
22 18 21 imbi12d 
 |-  ( d = b -> ( ( d e. m -> E. x e. Q. x ~Q <. a , d >. ) <-> ( b e. m -> E. x e. Q. x ~Q <. a , b >. ) ) )
23 17 22 cbvral2vw 
 |-  ( A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) <-> A. a e. N. A. b e. N. ( b e. m -> E. x e. Q. x ~Q <. a , b >. ) )
24 23 ralbii 
 |-  ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) <-> A. m e. y A. a e. N. A. b e. N. ( b e. m -> E. x e. Q. x ~Q <. a , b >. ) )
25 rexnal 
 |-  ( E. z e. ( N. X. N. ) -. ( <. a , b >. ~Q z -> -. ( 2nd ` z )  -. A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z )
26 pm4.63 
 |-  ( -. ( <. a , b >. ~Q z -> -. ( 2nd ` z )  ( <. a , b >. ~Q z /\ ( 2nd ` z )
27 xp2nd 
 |-  ( z e. ( N. X. N. ) -> ( 2nd ` z ) e. N. )
28 ltpiord 
 |-  ( ( ( 2nd ` z ) e. N. /\ b e. N. ) -> ( ( 2nd ` z )  ( 2nd ` z ) e. b ) )
29 28 ancoms 
 |-  ( ( b e. N. /\ ( 2nd ` z ) e. N. ) -> ( ( 2nd ` z )  ( 2nd ` z ) e. b ) )
30 27 29 sylan2 
 |-  ( ( b e. N. /\ z e. ( N. X. N. ) ) -> ( ( 2nd ` z )  ( 2nd ` z ) e. b ) )
31 30 adantll 
 |-  ( ( ( a e. N. /\ b e. N. ) /\ z e. ( N. X. N. ) ) -> ( ( 2nd ` z )  ( 2nd ` z ) e. b ) )
32 31 anbi2d 
 |-  ( ( ( a e. N. /\ b e. N. ) /\ z e. ( N. X. N. ) ) -> ( ( <. a , b >. ~Q z /\ ( 2nd ` z )  ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) ) )
33 26 32 bitrid 
 |-  ( ( ( a e. N. /\ b e. N. ) /\ z e. ( N. X. N. ) ) -> ( -. ( <. a , b >. ~Q z -> -. ( 2nd ` z )  ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) ) )
34 33 rexbidva 
 |-  ( ( a e. N. /\ b e. N. ) -> ( E. z e. ( N. X. N. ) -. ( <. a , b >. ~Q z -> -. ( 2nd ` z )  E. z e. ( N. X. N. ) ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) ) )
35 25 34 bitr3id 
 |-  ( ( a e. N. /\ b e. N. ) -> ( -. A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z )  E. z e. ( N. X. N. ) ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) ) )
36 xp1st 
 |-  ( z e. ( N. X. N. ) -> ( 1st ` z ) e. N. )
37 elequ2 
 |-  ( m = b -> ( d e. m <-> d e. b ) )
38 37 imbi1d 
 |-  ( m = b -> ( ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) <-> ( d e. b -> E. x e. Q. x ~Q <. c , d >. ) ) )
39 38 2ralbidv 
 |-  ( m = b -> ( A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) <-> A. c e. N. A. d e. N. ( d e. b -> E. x e. Q. x ~Q <. c , d >. ) ) )
40 39 rspccv 
 |-  ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) -> ( b e. y -> A. c e. N. A. d e. N. ( d e. b -> E. x e. Q. x ~Q <. c , d >. ) ) )
41 opeq1 
 |-  ( c = ( 1st ` z ) -> <. c , d >. = <. ( 1st ` z ) , d >. )
42 41 breq2d 
 |-  ( c = ( 1st ` z ) -> ( x ~Q <. c , d >. <-> x ~Q <. ( 1st ` z ) , d >. ) )
43 42 rexbidv 
 |-  ( c = ( 1st ` z ) -> ( E. x e. Q. x ~Q <. c , d >. <-> E. x e. Q. x ~Q <. ( 1st ` z ) , d >. ) )
44 43 imbi2d 
 |-  ( c = ( 1st ` z ) -> ( ( d e. b -> E. x e. Q. x ~Q <. c , d >. ) <-> ( d e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , d >. ) ) )
45 44 ralbidv 
 |-  ( c = ( 1st ` z ) -> ( A. d e. N. ( d e. b -> E. x e. Q. x ~Q <. c , d >. ) <-> A. d e. N. ( d e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , d >. ) ) )
46 45 rspccv 
 |-  ( A. c e. N. A. d e. N. ( d e. b -> E. x e. Q. x ~Q <. c , d >. ) -> ( ( 1st ` z ) e. N. -> A. d e. N. ( d e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , d >. ) ) )
47 eleq1 
 |-  ( d = ( 2nd ` z ) -> ( d e. b <-> ( 2nd ` z ) e. b ) )
48 opeq2 
 |-  ( d = ( 2nd ` z ) -> <. ( 1st ` z ) , d >. = <. ( 1st ` z ) , ( 2nd ` z ) >. )
49 48 breq2d 
 |-  ( d = ( 2nd ` z ) -> ( x ~Q <. ( 1st ` z ) , d >. <-> x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
50 49 rexbidv 
 |-  ( d = ( 2nd ` z ) -> ( E. x e. Q. x ~Q <. ( 1st ` z ) , d >. <-> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
51 47 50 imbi12d 
 |-  ( d = ( 2nd ` z ) -> ( ( d e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , d >. ) <-> ( ( 2nd ` z ) e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) )
52 51 rspccv 
 |-  ( A. d e. N. ( d e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , d >. ) -> ( ( 2nd ` z ) e. N. -> ( ( 2nd ` z ) e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) )
53 46 52 syl6 
 |-  ( A. c e. N. A. d e. N. ( d e. b -> E. x e. Q. x ~Q <. c , d >. ) -> ( ( 1st ` z ) e. N. -> ( ( 2nd ` z ) e. N. -> ( ( 2nd ` z ) e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) ) )
54 40 53 syl6 
 |-  ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) -> ( b e. y -> ( ( 1st ` z ) e. N. -> ( ( 2nd ` z ) e. N. -> ( ( 2nd ` z ) e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) ) ) )
55 54 imp 
 |-  ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) -> ( ( 1st ` z ) e. N. -> ( ( 2nd ` z ) e. N. -> ( ( 2nd ` z ) e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) ) )
56 36 55 syl5 
 |-  ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) -> ( z e. ( N. X. N. ) -> ( ( 2nd ` z ) e. N. -> ( ( 2nd ` z ) e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) ) )
57 27 56 mpdi 
 |-  ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) -> ( z e. ( N. X. N. ) -> ( ( 2nd ` z ) e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) )
58 57 3imp 
 |-  ( ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) /\ z e. ( N. X. N. ) /\ ( 2nd ` z ) e. b ) -> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. )
59 1st2nd2 
 |-  ( z e. ( N. X. N. ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
60 59 breq2d 
 |-  ( z e. ( N. X. N. ) -> ( x ~Q z <-> x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
61 60 rexbidv 
 |-  ( z e. ( N. X. N. ) -> ( E. x e. Q. x ~Q z <-> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
62 61 3ad2ant2 
 |-  ( ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) /\ z e. ( N. X. N. ) /\ ( 2nd ` z ) e. b ) -> ( E. x e. Q. x ~Q z <-> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
63 58 62 mpbird 
 |-  ( ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) /\ z e. ( N. X. N. ) /\ ( 2nd ` z ) e. b ) -> E. x e. Q. x ~Q z )
64 enqer 
 |-  ~Q Er ( N. X. N. )
65 64 a1i 
 |-  ( ( <. a , b >. ~Q z /\ x ~Q z ) -> ~Q Er ( N. X. N. ) )
66 simpr 
 |-  ( ( <. a , b >. ~Q z /\ x ~Q z ) -> x ~Q z )
67 simpl 
 |-  ( ( <. a , b >. ~Q z /\ x ~Q z ) -> <. a , b >. ~Q z )
68 65 66 67 ertr4d 
 |-  ( ( <. a , b >. ~Q z /\ x ~Q z ) -> x ~Q <. a , b >. )
69 68 ex 
 |-  ( <. a , b >. ~Q z -> ( x ~Q z -> x ~Q <. a , b >. ) )
70 69 reximdv 
 |-  ( <. a , b >. ~Q z -> ( E. x e. Q. x ~Q z -> E. x e. Q. x ~Q <. a , b >. ) )
71 63 70 syl5com 
 |-  ( ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) /\ z e. ( N. X. N. ) /\ ( 2nd ` z ) e. b ) -> ( <. a , b >. ~Q z -> E. x e. Q. x ~Q <. a , b >. ) )
72 71 3expia 
 |-  ( ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) /\ z e. ( N. X. N. ) ) -> ( ( 2nd ` z ) e. b -> ( <. a , b >. ~Q z -> E. x e. Q. x ~Q <. a , b >. ) ) )
73 72 impcomd 
 |-  ( ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) /\ z e. ( N. X. N. ) ) -> ( ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) -> E. x e. Q. x ~Q <. a , b >. ) )
74 73 rexlimdva 
 |-  ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) -> ( E. z e. ( N. X. N. ) ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) -> E. x e. Q. x ~Q <. a , b >. ) )
75 74 ex 
 |-  ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) -> ( b e. y -> ( E. z e. ( N. X. N. ) ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) -> E. x e. Q. x ~Q <. a , b >. ) ) )
76 75 com3r 
 |-  ( E. z e. ( N. X. N. ) ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) -> ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
77 35 76 biimtrdi 
 |-  ( ( a e. N. /\ b e. N. ) -> ( -. A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z )  ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) ) )
78 77 com13 
 |-  ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) -> ( -. A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z )  ( ( a e. N. /\ b e. N. ) -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) ) )
79 mulcompi 
 |-  ( a .N b ) = ( b .N a )
80 enqbreq 
 |-  ( ( ( a e. N. /\ b e. N. ) /\ ( a e. N. /\ b e. N. ) ) -> ( <. a , b >. ~Q <. a , b >. <-> ( a .N b ) = ( b .N a ) ) )
81 80 anidms 
 |-  ( ( a e. N. /\ b e. N. ) -> ( <. a , b >. ~Q <. a , b >. <-> ( a .N b ) = ( b .N a ) ) )
82 79 81 mpbiri 
 |-  ( ( a e. N. /\ b e. N. ) -> <. a , b >. ~Q <. a , b >. )
83 opelxpi 
 |-  ( ( a e. N. /\ b e. N. ) -> <. a , b >. e. ( N. X. N. ) )
84 breq1 
 |-  ( y = <. a , b >. -> ( y ~Q z <-> <. a , b >. ~Q z ) )
85 vex 
 |-  a e. _V
86 85 5 op2ndd 
 |-  ( y = <. a , b >. -> ( 2nd ` y ) = b )
87 86 breq2d 
 |-  ( y = <. a , b >. -> ( ( 2nd ` z )  ( 2nd ` z )
88 87 notbid 
 |-  ( y = <. a , b >. -> ( -. ( 2nd ` z )  -. ( 2nd ` z )
89 84 88 imbi12d 
 |-  ( y = <. a , b >. -> ( ( y ~Q z -> -. ( 2nd ` z )  ( <. a , b >. ~Q z -> -. ( 2nd ` z )
90 89 ralbidv 
 |-  ( y = <. a , b >. -> ( A. z e. ( N. X. N. ) ( y ~Q z -> -. ( 2nd ` z )  A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z )
91 df-nq 
 |-  Q. = { y e. ( N. X. N. ) | A. z e. ( N. X. N. ) ( y ~Q z -> -. ( 2nd ` z )
92 90 91 elrab2 
 |-  ( <. a , b >. e. Q. <-> ( <. a , b >. e. ( N. X. N. ) /\ A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z )
93 92 simplbi2 
 |-  ( <. a , b >. e. ( N. X. N. ) -> ( A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z )  <. a , b >. e. Q. ) )
94 83 93 syl 
 |-  ( ( a e. N. /\ b e. N. ) -> ( A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z )  <. a , b >. e. Q. ) )
95 breq1 
 |-  ( x = <. a , b >. -> ( x ~Q <. a , b >. <-> <. a , b >. ~Q <. a , b >. ) )
96 95 rspcev 
 |-  ( ( <. a , b >. e. Q. /\ <. a , b >. ~Q <. a , b >. ) -> E. x e. Q. x ~Q <. a , b >. )
97 96 expcom 
 |-  ( <. a , b >. ~Q <. a , b >. -> ( <. a , b >. e. Q. -> E. x e. Q. x ~Q <. a , b >. ) )
98 82 94 97 sylsyld 
 |-  ( ( a e. N. /\ b e. N. ) -> ( A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z )  E. x e. Q. x ~Q <. a , b >. ) )
99 98 com12 
 |-  ( A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z )  ( ( a e. N. /\ b e. N. ) -> E. x e. Q. x ~Q <. a , b >. ) )
100 99 a1dd 
 |-  ( A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z )  ( ( a e. N. /\ b e. N. ) -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
101 78 100 pm2.61d2 
 |-  ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) -> ( ( a e. N. /\ b e. N. ) -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
102 101 ralrimivv 
 |-  ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) -> A. a e. N. A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) )
103 24 102 sylbir 
 |-  ( A. m e. y A. a e. N. A. b e. N. ( b e. m -> E. x e. Q. x ~Q <. a , b >. ) -> A. a e. N. A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) )
104 103 a1i 
 |-  ( y e. On -> ( A. m e. y A. a e. N. A. b e. N. ( b e. m -> E. x e. Q. x ~Q <. a , b >. ) -> A. a e. N. A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
105 13 104 tfis2 
 |-  ( y e. On -> A. a e. N. A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) )
106 rsp 
 |-  ( A. a e. N. A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) -> ( a e. N. -> A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
107 105 106 syl 
 |-  ( y e. On -> ( a e. N. -> A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
108 rsp 
 |-  ( A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) -> ( b e. N. -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
109 107 108 syl6 
 |-  ( y e. On -> ( a e. N. -> ( b e. N. -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) ) )
110 109 impd 
 |-  ( y e. On -> ( ( a e. N. /\ b e. N. ) -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
111 110 com12 
 |-  ( ( a e. N. /\ b e. N. ) -> ( y e. On -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
112 111 rexlimdv 
 |-  ( ( a e. N. /\ b e. N. ) -> ( E. y e. On b e. y -> E. x e. Q. x ~Q <. a , b >. ) )
113 10 112 mpd 
 |-  ( ( a e. N. /\ b e. N. ) -> E. x e. Q. x ~Q <. a , b >. )
114 breq2 
 |-  ( A = <. a , b >. -> ( x ~Q A <-> x ~Q <. a , b >. ) )
115 114 rexbidv 
 |-  ( A = <. a , b >. -> ( E. x e. Q. x ~Q A <-> E. x e. Q. x ~Q <. a , b >. ) )
116 113 115 syl5ibrcom 
 |-  ( ( a e. N. /\ b e. N. ) -> ( A = <. a , b >. -> E. x e. Q. x ~Q A ) )
117 116 rexlimivv 
 |-  ( E. a e. N. E. b e. N. A = <. a , b >. -> E. x e. Q. x ~Q A )
118 1 117 sylbi 
 |-  ( A e. ( N. X. N. ) -> E. x e. Q. x ~Q A )
119 breq2 
 |-  ( a = A -> ( x ~Q a <-> x ~Q A ) )
120 breq2 
 |-  ( a = A -> ( y ~Q a <-> y ~Q A ) )
121 119 120 anbi12d 
 |-  ( a = A -> ( ( x ~Q a /\ y ~Q a ) <-> ( x ~Q A /\ y ~Q A ) ) )
122 121 imbi1d 
 |-  ( a = A -> ( ( ( x ~Q a /\ y ~Q a ) -> x = y ) <-> ( ( x ~Q A /\ y ~Q A ) -> x = y ) ) )
123 122 2ralbidv 
 |-  ( a = A -> ( A. x e. Q. A. y e. Q. ( ( x ~Q a /\ y ~Q a ) -> x = y ) <-> A. x e. Q. A. y e. Q. ( ( x ~Q A /\ y ~Q A ) -> x = y ) ) )
124 64 a1i 
 |-  ( ( x ~Q a /\ y ~Q a ) -> ~Q Er ( N. X. N. ) )
125 simpl 
 |-  ( ( x ~Q a /\ y ~Q a ) -> x ~Q a )
126 simpr 
 |-  ( ( x ~Q a /\ y ~Q a ) -> y ~Q a )
127 124 125 126 ertr4d 
 |-  ( ( x ~Q a /\ y ~Q a ) -> x ~Q y )
128 mulcompi 
 |-  ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` x ) )
129 elpqn 
 |-  ( y e. Q. -> y e. ( N. X. N. ) )
130 breq1 
 |-  ( y = x -> ( y ~Q z <-> x ~Q z ) )
131 fveq2 
 |-  ( y = x -> ( 2nd ` y ) = ( 2nd ` x ) )
132 131 breq2d 
 |-  ( y = x -> ( ( 2nd ` z )  ( 2nd ` z )
133 132 notbid 
 |-  ( y = x -> ( -. ( 2nd ` z )  -. ( 2nd ` z )
134 130 133 imbi12d 
 |-  ( y = x -> ( ( y ~Q z -> -. ( 2nd ` z )  ( x ~Q z -> -. ( 2nd ` z )
135 134 ralbidv 
 |-  ( y = x -> ( A. z e. ( N. X. N. ) ( y ~Q z -> -. ( 2nd ` z )  A. z e. ( N. X. N. ) ( x ~Q z -> -. ( 2nd ` z )
136 135 91 elrab2 
 |-  ( x e. Q. <-> ( x e. ( N. X. N. ) /\ A. z e. ( N. X. N. ) ( x ~Q z -> -. ( 2nd ` z )
137 136 simprbi 
 |-  ( x e. Q. -> A. z e. ( N. X. N. ) ( x ~Q z -> -. ( 2nd ` z )
138 breq2 
 |-  ( z = y -> ( x ~Q z <-> x ~Q y ) )
139 fveq2 
 |-  ( z = y -> ( 2nd ` z ) = ( 2nd ` y ) )
140 139 breq1d 
 |-  ( z = y -> ( ( 2nd ` z )  ( 2nd ` y )
141 140 notbid 
 |-  ( z = y -> ( -. ( 2nd ` z )  -. ( 2nd ` y )
142 138 141 imbi12d 
 |-  ( z = y -> ( ( x ~Q z -> -. ( 2nd ` z )  ( x ~Q y -> -. ( 2nd ` y )
143 142 rspcva 
 |-  ( ( y e. ( N. X. N. ) /\ A. z e. ( N. X. N. ) ( x ~Q z -> -. ( 2nd ` z )  ( x ~Q y -> -. ( 2nd ` y )
144 129 137 143 syl2anr 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y -> -. ( 2nd ` y )
145 144 imp 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> -. ( 2nd ` y )
146 elpqn 
 |-  ( x e. Q. -> x e. ( N. X. N. ) )
147 91 reqabi 
 |-  ( y e. Q. <-> ( y e. ( N. X. N. ) /\ A. z e. ( N. X. N. ) ( y ~Q z -> -. ( 2nd ` z )
148 147 simprbi 
 |-  ( y e. Q. -> A. z e. ( N. X. N. ) ( y ~Q z -> -. ( 2nd ` z )
149 breq2 
 |-  ( z = x -> ( y ~Q z <-> y ~Q x ) )
150 fveq2 
 |-  ( z = x -> ( 2nd ` z ) = ( 2nd ` x ) )
151 150 breq1d 
 |-  ( z = x -> ( ( 2nd ` z )  ( 2nd ` x )
152 151 notbid 
 |-  ( z = x -> ( -. ( 2nd ` z )  -. ( 2nd ` x )
153 149 152 imbi12d 
 |-  ( z = x -> ( ( y ~Q z -> -. ( 2nd ` z )  ( y ~Q x -> -. ( 2nd ` x )
154 153 rspcva 
 |-  ( ( x e. ( N. X. N. ) /\ A. z e. ( N. X. N. ) ( y ~Q z -> -. ( 2nd ` z )  ( y ~Q x -> -. ( 2nd ` x )
155 146 148 154 syl2an 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( y ~Q x -> -. ( 2nd ` x )
156 64 a1i 
 |-  ( x ~Q y -> ~Q Er ( N. X. N. ) )
157 id 
 |-  ( x ~Q y -> x ~Q y )
158 156 157 ersym 
 |-  ( x ~Q y -> y ~Q x )
159 155 158 impel 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> -. ( 2nd ` x )
160 xp2nd 
 |-  ( x e. ( N. X. N. ) -> ( 2nd ` x ) e. N. )
161 146 160 syl 
 |-  ( x e. Q. -> ( 2nd ` x ) e. N. )
162 161 ad2antrr 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 2nd ` x ) e. N. )
163 xp2nd 
 |-  ( y e. ( N. X. N. ) -> ( 2nd ` y ) e. N. )
164 129 163 syl 
 |-  ( y e. Q. -> ( 2nd ` y ) e. N. )
165 164 ad2antlr 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 2nd ` y ) e. N. )
166 ltsopi 
 |-
167 sotric 
 |-  ( (  ( ( 2nd ` x )  -. ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y )
168 166 167 mpan 
 |-  ( ( ( 2nd ` x ) e. N. /\ ( 2nd ` y ) e. N. ) -> ( ( 2nd ` x )  -. ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y )
169 168 notbid 
 |-  ( ( ( 2nd ` x ) e. N. /\ ( 2nd ` y ) e. N. ) -> ( -. ( 2nd ` x )  -. -. ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y )
170 notnotb 
 |-  ( ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y )  -. -. ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y )
171 169 170 bitr4di 
 |-  ( ( ( 2nd ` x ) e. N. /\ ( 2nd ` y ) e. N. ) -> ( -. ( 2nd ` x )  ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y )
172 162 165 171 syl2anc 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( -. ( 2nd ` x )  ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y )
173 159 172 mpbid 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y )
174 173 ord 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( -. ( 2nd ` x ) = ( 2nd ` y ) -> ( 2nd ` y )
175 145 174 mt3d 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 2nd ` x ) = ( 2nd ` y ) )
176 175 oveq2d 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 1st ` x ) .N ( 2nd ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` y ) ) )
177 128 176 eqtrid 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` y ) ) )
178 1st2nd2 
 |-  ( x e. ( N. X. N. ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
179 1st2nd2 
 |-  ( y e. ( N. X. N. ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
180 178 179 breqan12d 
 |-  ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( x ~Q y <-> <. ( 1st ` x ) , ( 2nd ` x ) >. ~Q <. ( 1st ` y ) , ( 2nd ` y ) >. ) )
181 xp1st 
 |-  ( x e. ( N. X. N. ) -> ( 1st ` x ) e. N. )
182 181 160 jca 
 |-  ( x e. ( N. X. N. ) -> ( ( 1st ` x ) e. N. /\ ( 2nd ` x ) e. N. ) )
183 xp1st 
 |-  ( y e. ( N. X. N. ) -> ( 1st ` y ) e. N. )
184 183 163 jca 
 |-  ( y e. ( N. X. N. ) -> ( ( 1st ` y ) e. N. /\ ( 2nd ` y ) e. N. ) )
185 enqbreq 
 |-  ( ( ( ( 1st ` x ) e. N. /\ ( 2nd ` x ) e. N. ) /\ ( ( 1st ` y ) e. N. /\ ( 2nd ` y ) e. N. ) ) -> ( <. ( 1st ` x ) , ( 2nd ` x ) >. ~Q <. ( 1st ` y ) , ( 2nd ` y ) >. <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) ) )
186 182 184 185 syl2an 
 |-  ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( <. ( 1st ` x ) , ( 2nd ` x ) >. ~Q <. ( 1st ` y ) , ( 2nd ` y ) >. <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) ) )
187 180 186 bitrd 
 |-  ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( x ~Q y <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) ) )
188 146 129 187 syl2an 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) ) )
189 188 biimpa 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) )
190 177 189 eqtrd 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) )
191 146 ad2antrr 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> x e. ( N. X. N. ) )
192 mulcanpi 
 |-  ( ( ( 2nd ` x ) e. N. /\ ( 1st ` x ) e. N. ) -> ( ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) <-> ( 1st ` x ) = ( 1st ` y ) ) )
193 160 181 192 syl2anc 
 |-  ( x e. ( N. X. N. ) -> ( ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) <-> ( 1st ` x ) = ( 1st ` y ) ) )
194 191 193 syl 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) <-> ( 1st ` x ) = ( 1st ` y ) ) )
195 190 194 mpbid 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 1st ` x ) = ( 1st ` y ) )
196 195 175 opeq12d 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. = <. ( 1st ` y ) , ( 2nd ` y ) >. )
197 191 178 syl 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
198 129 ad2antlr 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> y e. ( N. X. N. ) )
199 198 179 syl 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
200 196 197 199 3eqtr4d 
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> x = y )
201 200 ex 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y -> x = y ) )
202 127 201 syl5 
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( ( x ~Q a /\ y ~Q a ) -> x = y ) )
203 202 rgen2 
 |-  A. x e. Q. A. y e. Q. ( ( x ~Q a /\ y ~Q a ) -> x = y )
204 123 203 vtoclg 
 |-  ( A e. ( N. X. N. ) -> A. x e. Q. A. y e. Q. ( ( x ~Q A /\ y ~Q A ) -> x = y ) )
205 breq1 
 |-  ( x = y -> ( x ~Q A <-> y ~Q A ) )
206 205 reu4 
 |-  ( E! x e. Q. x ~Q A <-> ( E. x e. Q. x ~Q A /\ A. x e. Q. A. y e. Q. ( ( x ~Q A /\ y ~Q A ) -> x = y ) ) )
207 118 204 206 sylanbrc 
 |-  ( A e. ( N. X. N. ) -> E! x e. Q. x ~Q A )