Theorem nqereu 9218

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.)

Assertion

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

Distinct variable group:   x, A

Proof of Theorem nqereu

Dummy variables a b y c d m z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp2 4931	. . 3 |- ( A e. ( N. X. N. ) <-> E. a e. N. E. b e. N. A = <. a , b >. )
2		pion 9168	. . . . . . . . 9 |- ( b e. N. -> b e. On )
3		suceloni 6547	. . . . . . . . 9 |- ( b e. On -> suc b e. On )
4	2, 3	syl 16	. . . . . . . 8 |- ( b e. N. -> suc b e. On )
5		vex 3037	. . . . . . . . 9 |- b e. _V
6	5	sucid 4871	. . . . . . . 8 |- b e. suc b
7		eleq2 2455	. . . . . . . . 9 |- ( y = suc b -> ( b e. y <-> b e. suc b ) )
8	7	rspcev 3135	. . . . . . . 8 |- ( ( suc b e. On /\ b e. suc b ) -> E. y e. On b e. y )
9	4, 6, 8	sylancl 660	. . . . . . 7 |- ( b e. N. -> E. y e. On b e. y )
10	9	adantl 464	. . . . . 6 |- ( ( a e. N. /\ b e. N. ) -> E. y e. On b e. y )
11		elequ2 1831	. . . . . . . . . . . . . 14 |- ( y = m -> ( b e. y <-> b e. m ) )
12	11	imbi1d 315	. . . . . . . . . . . . 13 |- ( 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 2826	. . . . . . . . . . . 12 |- ( 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 4131	. . . . . . . . . . . . . . . . . . 19 |- ( c = a -> <. c , d >. = <. a , d >. )
15	14	breq2d 4379	. . . . . . . . . . . . . . . . . 18 |- ( c = a -> ( x ~Q <. c , d >. <-> x ~Q <. a , d >. ) )
16	15	rexbidv 2893	. . . . . . . . . . . . . . . . 17 |- ( c = a -> ( E. x e. Q. x ~Q <. c , d >. <-> E. x e. Q. x ~Q <. a , d >. ) )
17	16	imbi2d 314	. . . . . . . . . . . . . . . 16 |- ( 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 1829	. . . . . . . . . . . . . . . . 17 |- ( d = b -> ( d e. m <-> b e. m ) )
19		opeq2 4132	. . . . . . . . . . . . . . . . . . 19 |- ( d = b -> <. a , d >. = <. a , b >. )
20	19	breq2d 4379	. . . . . . . . . . . . . . . . . 18 |- ( d = b -> ( x ~Q <. a , d >. <-> x ~Q <. a , b >. ) )
21	20	rexbidv 2893	. . . . . . . . . . . . . . . . 17 |- ( d = b -> ( E. x e. Q. x ~Q <. a , d >. <-> E. x e. Q. x ~Q <. a , b >. ) )
22	18, 21	imbi12d 318	. . . . . . . . . . . . . . . 16 |- ( 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	cbvral2v 3017	. . . . . . . . . . . . . . 15 |- ( 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 2813	. . . . . . . . . . . . . 14 |- ( 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 2830	. . . . . . . . . . . . . . . . . . 19 |- ( E. z e. ( N. X. N. ) -. ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) <-> -. A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) )
26		pm4.63 419	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) <-> ( <. a , b >. ~Q z /\ ( 2nd ` z ) <N b ) )
27		xp2nd 6730	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( z e. ( N. X. N. ) -> ( 2nd ` z ) e. N. )
28		ltpiord 9176	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 2nd ` z ) e. N. /\ b e. N. ) -> ( ( 2nd ` z ) <N b <-> ( 2nd ` z ) e. b ) )
29	28	ancoms 451	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( b e. N. /\ ( 2nd ` z ) e. N. ) -> ( ( 2nd ` z ) <N b <-> ( 2nd ` z ) e. b ) )
30	27, 29	sylan2 472	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( b e. N. /\ z e. ( N. X. N. ) ) -> ( ( 2nd ` z ) <N b <-> ( 2nd ` z ) e. b ) )
31	30	adantll 711	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( a e. N. /\ b e. N. ) /\ z e. ( N. X. N. ) ) -> ( ( 2nd ` z ) <N b <-> ( 2nd ` z ) e. b ) )
32	31	anbi2d 701	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( a e. N. /\ b e. N. ) /\ z e. ( N. X. N. ) ) -> ( ( <. a , b >. ~Q z /\ ( 2nd ` z ) <N b ) <-> ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) ) )
33	26, 32	syl5bb 257	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( a e. N. /\ b e. N. ) /\ z e. ( N. X. N. ) ) -> ( -. ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) <-> ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) ) )
34	33	rexbidva 2890	. . . . . . . . . . . . . . . . . . 19 |- ( ( a e. N. /\ b e. N. ) -> ( E. z e. ( N. X. N. ) -. ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) <-> E. z e. ( N. X. N. ) ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) ) )
35	25, 34	syl5bbr 259	. . . . . . . . . . . . . . . . . 18 |- ( ( a e. N. /\ b e. N. ) -> ( -. A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) <-> E. z e. ( N. X. N. ) ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) ) )
36		xp1st 6729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( z e. ( N. X. N. ) -> ( 1st ` z ) e. N. )
37		elequ2 1831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( m = b -> ( d e. m <-> d e. b ) )
38	37	imbi1d 315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( 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 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( 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 3132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( 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 4131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( c = ( 1st ` z ) -> <. c , d >. = <. ( 1st ` z ) , d >. )
42	41	breq2d 4379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( c = ( 1st ` z ) -> ( x ~Q <. c , d >. <-> x ~Q <. ( 1st ` z ) , d >. ) )
43	42	rexbidv 2893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( c = ( 1st ` z ) -> ( E. x e. Q. x ~Q <. c , d >. <-> E. x e. Q. x ~Q <. ( 1st ` z ) , d >. ) )
44	43	imbi2d 314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( 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 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( 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 3132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( 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 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( d = ( 2nd ` z ) -> ( d e. b <-> ( 2nd ` z ) e. b ) )
48		opeq2 4132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( d = ( 2nd ` z ) -> <. ( 1st ` z ) , d >. = <. ( 1st ` z ) , ( 2nd ` z ) >. )
49	48	breq2d 4379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( d = ( 2nd ` z ) -> ( x ~Q <. ( 1st ` z ) , d >. <-> x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
50	49	rexbidv 2893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( 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 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( 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 3132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( 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 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( 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 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( 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 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( 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 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( 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 42	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( 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 1188	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( 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 6736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( z e. ( N. X. N. ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
60	59	breq2d 4379	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z e. ( N. X. N. ) -> ( x ~Q z <-> x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
61	60	rexbidv 2893	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( 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 1016	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( 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 232	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 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 9210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ~Q Er ( N. X. N. )
65	64	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( <. a , b >. ~Q z /\ x ~Q z ) -> ~Q Er ( N. X. N. ) )
66		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( <. a , b >. ~Q z /\ x ~Q z ) -> x ~Q z )
67		simpl 455	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( <. a , b >. ~Q z /\ x ~Q z ) -> <. a , b >. ~Q z )
68	65, 66, 67	ertr4d 7248	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( <. a , b >. ~Q z /\ x ~Q z ) -> x ~Q <. a , b >. )
69	68	ex 432	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( <. a , b >. ~Q z -> ( x ~Q z -> x ~Q <. a , b >. ) )
70	69	reximdv 2856	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( <. a , b >. ~Q z -> ( E. x e. Q. x ~Q z -> E. x e. Q. x ~Q <. a , b >. ) )
71	63, 70	syl5com 30	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 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 1196	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 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	com23 78	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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	impd 429	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 >. ) )
75	74	rexlimdva 2874	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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	ex 432	. . . . . . . . . . . . . . . . . . 19 |- ( 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 >. ) ) )
77	76	com3r 79	. . . . . . . . . . . . . . . . . 18 |- ( 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 >. ) ) )
78	35, 77	syl6bi 228	. . . . . . . . . . . . . . . . 17 |- ( ( a e. N. /\ b e. N. ) -> ( -. A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N 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 >. ) ) ) )
79	78	com13 80	. . . . . . . . . . . . . . . 16 |- ( 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 ) <N b ) -> ( ( a e. N. /\ b e. N. ) -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) ) )
80		mulcompi 9185	. . . . . . . . . . . . . . . . . . . 20 |- ( a .N b ) = ( b .N a )
81		enqbreq 9208	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( a e. N. /\ b e. N. ) /\ ( a e. N. /\ b e. N. ) ) -> ( <. a , b >. ~Q <. a , b >. <-> ( a .N b ) = ( b .N a ) ) )
82	81	anidms 643	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. N. /\ b e. N. ) -> ( <. a , b >. ~Q <. a , b >. <-> ( a .N b ) = ( b .N a ) ) )
83	80, 82	mpbiri 233	. . . . . . . . . . . . . . . . . . 19 |- ( ( a e. N. /\ b e. N. ) -> <. a , b >. ~Q <. a , b >. )
84		opelxpi 4945	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. N. /\ b e. N. ) -> <. a , b >. e. ( N. X. N. ) )
85		breq1 4370	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = <. a , b >. -> ( y ~Q z <-> <. a , b >. ~Q z ) )
86		vex 3037	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- a e. _V
87	86, 5	op2ndd 6710	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y = <. a , b >. -> ( 2nd ` y ) = b )
88	87	breq2d 4379	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = <. a , b >. -> ( ( 2nd ` z ) <N ( 2nd ` y ) <-> ( 2nd ` z ) <N b ) )
89	88	notbid 292	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = <. a , b >. -> ( -. ( 2nd ` z ) <N ( 2nd ` y ) <-> -. ( 2nd ` z ) <N b ) )
90	85, 89	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y = <. a , b >. -> ( ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) <-> ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) ) )
91	90	ralbidv 2821	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = <. a , b >. -> ( A. z e. ( N. X. N. ) ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) <-> A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) ) )
92		df-nq 9201	. . . . . . . . . . . . . . . . . . . . . 22 |- Q. = { y e. ( N. X. N. ) | A. z e. ( N. X. N. ) ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) }
93	91, 92	elrab2 3184	. . . . . . . . . . . . . . . . . . . . 21 |- ( <. a , b >. e. Q. <-> ( <. a , b >. e. ( N. X. N. ) /\ A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) ) )
94	93	simplbi2 623	. . . . . . . . . . . . . . . . . . . 20 |- ( <. a , b >. e. ( N. X. N. ) -> ( A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) -> <. a , b >. e. Q. ) )
95	84, 94	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( a e. N. /\ b e. N. ) -> ( A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) -> <. a , b >. e. Q. ) )
96		breq1 4370	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = <. a , b >. -> ( x ~Q <. a , b >. <-> <. a , b >. ~Q <. a , b >. ) )
97	96	rspcev 3135	. . . . . . . . . . . . . . . . . . . 20 |- ( ( <. a , b >. e. Q. /\ <. a , b >. ~Q <. a , b >. ) -> E. x e. Q. x ~Q <. a , b >. )
98	97	expcom 433	. . . . . . . . . . . . . . . . . . 19 |- ( <. a , b >. ~Q <. a , b >. -> ( <. a , b >. e. Q. -> E. x e. Q. x ~Q <. a , b >. ) )
99	83, 95, 98	sylsyld 56	. . . . . . . . . . . . . . . . . 18 |- ( ( a e. N. /\ b e. N. ) -> ( A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) -> E. x e. Q. x ~Q <. a , b >. ) )
100	99	com12 31	. . . . . . . . . . . . . . . . 17 |- ( A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) -> ( ( a e. N. /\ b e. N. ) -> E. x e. Q. x ~Q <. a , b >. ) )
101	100	a1dd 46	. . . . . . . . . . . . . . . 16 |- ( A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) -> ( ( a e. N. /\ b e. N. ) -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
102	79, 101	pm2.61d2 160	. . . . . . . . . . . . . . 15 |- ( 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 >. ) ) )
103	102	ralrimivv 2802	. . . . . . . . . . . . . 14 |- ( 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 >. ) )
104	24, 103	sylbir 213	. . . . . . . . . . . . 13 |- ( 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	104	a1i 11	. . . . . . . . . . . 12 |- ( 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 >. ) ) )
106	13, 105	tfis2 6590	. . . . . . . . . . 11 |- ( y e. On -> A. a e. N. A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) )
107		rsp 2748	. . . . . . . . . . 11 |- ( 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 >. ) ) )
108	106, 107	syl 16	. . . . . . . . . 10 |- ( y e. On -> ( a e. N. -> A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
109		rsp 2748	. . . . . . . . . 10 |- ( 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 >. ) ) )
110	108, 109	syl6 33	. . . . . . . . 9 |- ( y e. On -> ( a e. N. -> ( b e. N. -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) ) )
111	110	impd 429	. . . . . . . 8 |- ( y e. On -> ( ( a e. N. /\ b e. N. ) -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
112	111	com12 31	. . . . . . 7 |- ( ( a e. N. /\ b e. N. ) -> ( y e. On -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
113	112	rexlimdv 2872	. . . . . 6 |- ( ( a e. N. /\ b e. N. ) -> ( E. y e. On b e. y -> E. x e. Q. x ~Q <. a , b >. ) )
114	10, 113	mpd 15	. . . . 5 |- ( ( a e. N. /\ b e. N. ) -> E. x e. Q. x ~Q <. a , b >. )
115		breq2 4371	. . . . . 6 |- ( A = <. a , b >. -> ( x ~Q A <-> x ~Q <. a , b >. ) )
116	115	rexbidv 2893	. . . . 5 |- ( A = <. a , b >. -> ( E. x e. Q. x ~Q A <-> E. x e. Q. x ~Q <. a , b >. ) )
117	114, 116	syl5ibrcom 222	. . . 4 |- ( ( a e. N. /\ b e. N. ) -> ( A = <. a , b >. -> E. x e. Q. x ~Q A ) )
118	117	rexlimivv 2879	. . 3 |- ( E. a e. N. E. b e. N. A = <. a , b >. -> E. x e. Q. x ~Q A )
119	1, 118	sylbi 195	. 2 |- ( A e. ( N. X. N. ) -> E. x e. Q. x ~Q A )
120		breq2 4371	. . . . . 6 |- ( a = A -> ( x ~Q a <-> x ~Q A ) )
121		breq2 4371	. . . . . 6 |- ( a = A -> ( y ~Q a <-> y ~Q A ) )
122	120, 121	anbi12d 708	. . . . 5 |- ( a = A -> ( ( x ~Q a /\ y ~Q a ) <-> ( x ~Q A /\ y ~Q A ) ) )
123	122	imbi1d 315	. . . 4 |- ( a = A -> ( ( ( x ~Q a /\ y ~Q a ) -> x = y ) <-> ( ( x ~Q A /\ y ~Q A ) -> x = y ) ) )
124	123	2ralbidv 2826	. . 3 |- ( 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 ) ) )
125	64	a1i 11	. . . . . 6 |- ( ( x ~Q a /\ y ~Q a ) -> ~Q Er ( N. X. N. ) )
126		simpl 455	. . . . . 6 |- ( ( x ~Q a /\ y ~Q a ) -> x ~Q a )
127		simpr 459	. . . . . 6 |- ( ( x ~Q a /\ y ~Q a ) -> y ~Q a )
128	125, 126, 127	ertr4d 7248	. . . . 5 |- ( ( x ~Q a /\ y ~Q a ) -> x ~Q y )
129		mulcompi 9185	. . . . . . . . . . 11 |- ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` x ) )
130		elpqn 9214	. . . . . . . . . . . . . . 15 |- ( y e. Q. -> y e. ( N. X. N. ) )
131		breq1 4370	. . . . . . . . . . . . . . . . . . 19 |- ( y = x -> ( y ~Q z <-> x ~Q z ) )
132		fveq2 5774	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = x -> ( 2nd ` y ) = ( 2nd ` x ) )
133	132	breq2d 4379	. . . . . . . . . . . . . . . . . . . 20 |- ( y = x -> ( ( 2nd ` z ) <N ( 2nd ` y ) <-> ( 2nd ` z ) <N ( 2nd ` x ) ) )
134	133	notbid 292	. . . . . . . . . . . . . . . . . . 19 |- ( y = x -> ( -. ( 2nd ` z ) <N ( 2nd ` y ) <-> -. ( 2nd ` z ) <N ( 2nd ` x ) ) )
135	131, 134	imbi12d 318	. . . . . . . . . . . . . . . . . 18 |- ( y = x -> ( ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) <-> ( x ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` x ) ) ) )
136	135	ralbidv 2821	. . . . . . . . . . . . . . . . 17 |- ( y = x -> ( A. z e. ( N. X. N. ) ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) <-> A. z e. ( N. X. N. ) ( x ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` x ) ) ) )
137	136, 92	elrab2 3184	. . . . . . . . . . . . . . . 16 |- ( x e. Q. <-> ( x e. ( N. X. N. ) /\ A. z e. ( N. X. N. ) ( x ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` x ) ) ) )
138	137	simprbi 462	. . . . . . . . . . . . . . 15 |- ( x e. Q. -> A. z e. ( N. X. N. ) ( x ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` x ) ) )
139		breq2 4371	. . . . . . . . . . . . . . . . 17 |- ( z = y -> ( x ~Q z <-> x ~Q y ) )
140		fveq2 5774	. . . . . . . . . . . . . . . . . . 19 |- ( z = y -> ( 2nd ` z ) = ( 2nd ` y ) )
141	140	breq1d 4377	. . . . . . . . . . . . . . . . . 18 |- ( z = y -> ( ( 2nd ` z ) <N ( 2nd ` x ) <-> ( 2nd ` y ) <N ( 2nd ` x ) ) )
142	141	notbid 292	. . . . . . . . . . . . . . . . 17 |- ( z = y -> ( -. ( 2nd ` z ) <N ( 2nd ` x ) <-> -. ( 2nd ` y ) <N ( 2nd ` x ) ) )
143	139, 142	imbi12d 318	. . . . . . . . . . . . . . . 16 |- ( z = y -> ( ( x ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` x ) ) <-> ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) ) ) )
144	143	rspcva 3133	. . . . . . . . . . . . . . 15 |- ( ( y e. ( N. X. N. ) /\ A. z e. ( N. X. N. ) ( x ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` x ) ) ) -> ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) ) )
145	130, 138, 144	syl2anr 476	. . . . . . . . . . . . . 14 |- ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) ) )
146	145	imp 427	. . . . . . . . . . . . 13 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> -. ( 2nd ` y ) <N ( 2nd ` x ) )
147	64	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( x ~Q y -> ~Q Er ( N. X. N. ) )
148		id 22	. . . . . . . . . . . . . . . . . 18 |- ( x ~Q y -> x ~Q y )
149	147, 148	ersym 7241	. . . . . . . . . . . . . . . . 17 |- ( x ~Q y -> y ~Q x )
150		elpqn 9214	. . . . . . . . . . . . . . . . . 18 |- ( x e. Q. -> x e. ( N. X. N. ) )
151	92	rabeq2i 3031	. . . . . . . . . . . . . . . . . . 19 |- ( y e. Q. <-> ( y e. ( N. X. N. ) /\ A. z e. ( N. X. N. ) ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) ) )
152	151	simprbi 462	. . . . . . . . . . . . . . . . . 18 |- ( y e. Q. -> A. z e. ( N. X. N. ) ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) )
153		breq2 4371	. . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( y ~Q z <-> y ~Q x ) )
154		fveq2 5774	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z = x -> ( 2nd ` z ) = ( 2nd ` x ) )
155	154	breq1d 4377	. . . . . . . . . . . . . . . . . . . . 21 |- ( z = x -> ( ( 2nd ` z ) <N ( 2nd ` y ) <-> ( 2nd ` x ) <N ( 2nd ` y ) ) )
156	155	notbid 292	. . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( -. ( 2nd ` z ) <N ( 2nd ` y ) <-> -. ( 2nd ` x ) <N ( 2nd ` y ) ) )
157	153, 156	imbi12d 318	. . . . . . . . . . . . . . . . . . 19 |- ( z = x -> ( ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) <-> ( y ~Q x -> -. ( 2nd ` x ) <N ( 2nd ` y ) ) ) )
158	157	rspcva 3133	. . . . . . . . . . . . . . . . . 18 |- ( ( x e. ( N. X. N. ) /\ A. z e. ( N. X. N. ) ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) ) -> ( y ~Q x -> -. ( 2nd ` x ) <N ( 2nd ` y ) ) )
159	150, 152, 158	syl2an 475	. . . . . . . . . . . . . . . . 17 |- ( ( x e. Q. /\ y e. Q. ) -> ( y ~Q x -> -. ( 2nd ` x ) <N ( 2nd ` y ) ) )
160	149, 159	syl5 32	. . . . . . . . . . . . . . . 16 |- ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y -> -. ( 2nd ` x ) <N ( 2nd ` y ) ) )
161	160	imp 427	. . . . . . . . . . . . . . 15 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> -. ( 2nd ` x ) <N ( 2nd ` y ) )
162		xp2nd 6730	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( N. X. N. ) -> ( 2nd ` x ) e. N. )
163	150, 162	syl 16	. . . . . . . . . . . . . . . . 17 |- ( x e. Q. -> ( 2nd ` x ) e. N. )
164	163	ad2antrr 723	. . . . . . . . . . . . . . . 16 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 2nd ` x ) e. N. )
165		xp2nd 6730	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( N. X. N. ) -> ( 2nd ` y ) e. N. )
166	130, 165	syl 16	. . . . . . . . . . . . . . . . 17 |- ( y e. Q. -> ( 2nd ` y ) e. N. )
167	166	ad2antlr 724	. . . . . . . . . . . . . . . 16 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 2nd ` y ) e. N. )
168		ltsopi 9177	. . . . . . . . . . . . . . . . . . 19 |- <N Or N.
169		sotric 4740	. . . . . . . . . . . . . . . . . . 19 |- ( ( <N Or N. /\ ( ( 2nd ` x ) e. N. /\ ( 2nd ` y ) e. N. ) ) -> ( ( 2nd ` x ) <N ( 2nd ` y ) <-> -. ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) ) )
170	168, 169	mpan 668	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 2nd ` x ) e. N. /\ ( 2nd ` y ) e. N. ) -> ( ( 2nd ` x ) <N ( 2nd ` y ) <-> -. ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) ) )
171	170	notbid 292	. . . . . . . . . . . . . . . . 17 |- ( ( ( 2nd ` x ) e. N. /\ ( 2nd ` y ) e. N. ) -> ( -. ( 2nd ` x ) <N ( 2nd ` y ) <-> -. -. ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) ) )
172		notnot 289	. . . . . . . . . . . . . . . . 17 |- ( ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) <-> -. -. ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) )
173	171, 172	syl6bbr 263	. . . . . . . . . . . . . . . 16 |- ( ( ( 2nd ` x ) e. N. /\ ( 2nd ` y ) e. N. ) -> ( -. ( 2nd ` x ) <N ( 2nd ` y ) <-> ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) ) )
174	164, 167, 173	syl2anc 659	. . . . . . . . . . . . . . 15 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( -. ( 2nd ` x ) <N ( 2nd ` y ) <-> ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) ) )
175	161, 174	mpbid 210	. . . . . . . . . . . . . 14 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) )
176	175	ord 375	. . . . . . . . . . . . 13 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( -. ( 2nd ` x ) = ( 2nd ` y ) -> ( 2nd ` y ) <N ( 2nd ` x ) ) )
177	146, 176	mt3d 125	. . . . . . . . . . . 12 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 2nd ` x ) = ( 2nd ` y ) )
178	177	oveq2d 6212	. . . . . . . . . . 11 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 1st ` x ) .N ( 2nd ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` y ) ) )
179	129, 178	syl5eq 2435	. . . . . . . . . 10 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` y ) ) )
180		1st2nd2 6736	. . . . . . . . . . . . . 14 |- ( x e. ( N. X. N. ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
181		1st2nd2 6736	. . . . . . . . . . . . . 14 |- ( y e. ( N. X. N. ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
182	180, 181	breqan12d 4382	. . . . . . . . . . . . 13 |- ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( x ~Q y <-> <. ( 1st ` x ) , ( 2nd ` x ) >. ~Q <. ( 1st ` y ) , ( 2nd ` y ) >. ) )
183		xp1st 6729	. . . . . . . . . . . . . . 15 |- ( x e. ( N. X. N. ) -> ( 1st ` x ) e. N. )
184	183, 162	jca 530	. . . . . . . . . . . . . 14 |- ( x e. ( N. X. N. ) -> ( ( 1st ` x ) e. N. /\ ( 2nd ` x ) e. N. ) )
185		xp1st 6729	. . . . . . . . . . . . . . 15 |- ( y e. ( N. X. N. ) -> ( 1st ` y ) e. N. )
186	185, 165	jca 530	. . . . . . . . . . . . . 14 |- ( y e. ( N. X. N. ) -> ( ( 1st ` y ) e. N. /\ ( 2nd ` y ) e. N. ) )
187		enqbreq 9208	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) ) ) )
188	184, 186, 187	syl2an 475	. . . . . . . . . . . . 13 |- ( ( 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 ) ) ) )
189	182, 188	bitrd 253	. . . . . . . . . . . 12 |- ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( x ~Q y <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) ) )
190	150, 130, 189	syl2an 475	. . . . . . . . . . 11 |- ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) ) )
191	190	biimpa 482	. . . . . . . . . 10 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) )
192	179, 191	eqtrd 2423	. . . . . . . . 9 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) )
193	150	ad2antrr 723	. . . . . . . . . 10 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> x e. ( N. X. N. ) )
194		mulcanpi 9189	. . . . . . . . . . 11 |- ( ( ( 2nd ` x ) e. N. /\ ( 1st ` x ) e. N. ) -> ( ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) <-> ( 1st ` x ) = ( 1st ` y ) ) )
195	162, 183, 194	syl2anc 659	. . . . . . . . . 10 |- ( x e. ( N. X. N. ) -> ( ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) <-> ( 1st ` x ) = ( 1st ` y ) ) )
196	193, 195	syl 16	. . . . . . . . 9 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) <-> ( 1st ` x ) = ( 1st ` y ) ) )
197	192, 196	mpbid 210	. . . . . . . 8 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 1st ` x ) = ( 1st ` y ) )
198	197, 177	opeq12d 4139	. . . . . . 7 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. = <. ( 1st ` y ) , ( 2nd ` y ) >. )
199	193, 180	syl 16	. . . . . . 7 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
200	130	ad2antlr 724	. . . . . . . 8 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> y e. ( N. X. N. ) )
201	200, 181	syl 16	. . . . . . 7 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
202	198, 199, 201	3eqtr4d 2433	. . . . . 6 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> x = y )
203	202	ex 432	. . . . 5 |- ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y -> x = y ) )
204	128, 203	syl5 32	. . . 4 |- ( ( x e. Q. /\ y e. Q. ) -> ( ( x ~Q a /\ y ~Q a ) -> x = y ) )
205	204	rgen2a 2809	. . 3 |- A. x e. Q. A. y e. Q. ( ( x ~Q a /\ y ~Q a ) -> x = y )
206	124, 205	vtoclg 3092	. 2 |- ( A e. ( N. X. N. ) -> A. x e. Q. A. y e. Q. ( ( x ~Q A /\ y ~Q A ) -> x = y ) )
207		breq1 4370	. . 3 |- ( x = y -> ( x ~Q A <-> y ~Q A ) )
208	207	reu4 3218	. 2 |- ( 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 ) ) )
209	119, 206, 208	sylanbrc 662	1 |- ( A e. ( N. X. N. ) -> E! x e. Q. x ~Q A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 366   /\ wa 367   /\ w3a 971   = wceq 1399   e. wcel 1826   A.wral 2732   E.wrex 2733   E!wreu 2734   <.cop 3950   class class class wbr 4367   Or wor 4713   Oncon0 4792   suc csuc 4794   X. cxp 4911   ` cfv 5496  (class class class)co 6196   1stc1st 6697   2ndc2nd 6698   Er wer 7226   N.cnpi 9133   .N cmi 9135   <N clti 9136   ~Q ceq 9140   Q.cnq 9141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-reu 2739  df-rmo 2740  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-iun 4245  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-om 6600  df-1st 6699  df-2nd 6700  df-recs 6960  df-rdg 6994  df-oadd 7052  df-omul 7053  df-er 7229  df-ni 9161  df-mi 9163  df-lti 9164  df-enq 9200  df-nq 9201

This theorem is referenced by:  nqerf  9219  enqeq  9223