Theorem nqereu 9353

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 4872	. . 3 |- ( A e. ( N. X. N. ) <-> E. a e. N. E. b e. N. A = <. a , b >. )
2		pion 9303	. . . . . . . . 9 |- ( b e. N. -> b e. On )
3		suceloni 6654	. . . . . . . . 9 |- ( b e. On -> suc b e. On )
4	2, 3	syl 17	. . . . . . . 8 |- ( b e. N. -> suc b e. On )
5		vex 3090	. . . . . . . . 9 |- b e. _V
6	5	sucid 5521	. . . . . . . 8 |- b e. suc b
7		eleq2 2502	. . . . . . . . 9 |- ( y = suc b -> ( b e. y <-> b e. suc b ) )
8	7	rspcev 3188	. . . . . . . 8 |- ( ( suc b e. On /\ b e. suc b ) -> E. y e. On b e. y )
9	4, 6, 8	sylancl 666	. . . . . . 7 |- ( b e. N. -> E. y e. On b e. y )
10	9	adantl 467	. . . . . 6 |- ( ( a e. N. /\ b e. N. ) -> E. y e. On b e. y )
11		elequ2 1875	. . . . . . . . . . . . . 14 |- ( y = m -> ( b e. y <-> b e. m ) )
12	11	imbi1d 318	. . . . . . . . . . . . 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 2876	. . . . . . . . . . . 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 4190	. . . . . . . . . . . . . . . . . . 19 |- ( c = a -> <. c , d >. = <. a , d >. )
15	14	breq2d 4438	. . . . . . . . . . . . . . . . . 18 |- ( c = a -> ( x ~Q <. c , d >. <-> x ~Q <. a , d >. ) )
16	15	rexbidv 2946	. . . . . . . . . . . . . . . . 17 |- ( c = a -> ( E. x e. Q. x ~Q <. c , d >. <-> E. x e. Q. x ~Q <. a , d >. ) )
17	16	imbi2d 317	. . . . . . . . . . . . . . . 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 1873	. . . . . . . . . . . . . . . . 17 |- ( d = b -> ( d e. m <-> b e. m ) )
19		opeq2 4191	. . . . . . . . . . . . . . . . . . 19 |- ( d = b -> <. a , d >. = <. a , b >. )
20	19	breq2d 4438	. . . . . . . . . . . . . . . . . 18 |- ( d = b -> ( x ~Q <. a , d >. <-> x ~Q <. a , b >. ) )
21	20	rexbidv 2946	. . . . . . . . . . . . . . . . 17 |- ( d = b -> ( E. x e. Q. x ~Q <. a , d >. <-> E. x e. Q. x ~Q <. a , b >. ) )
22	18, 21	imbi12d 321	. . . . . . . . . . . . . . . 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 3070	. . . . . . . . . . . . . . 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 2863	. . . . . . . . . . . . . 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 2880	. . . . . . . . . . . . . . . . . . 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 422	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) <-> ( <. a , b >. ~Q z /\ ( 2nd ` z ) <N b ) )
27		xp2nd 6838	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( z e. ( N. X. N. ) -> ( 2nd ` z ) e. N. )
28		ltpiord 9311	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 2nd ` z ) e. N. /\ b e. N. ) -> ( ( 2nd ` z ) <N b <-> ( 2nd ` z ) e. b ) )
29	28	ancoms 454	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( b e. N. /\ ( 2nd ` z ) e. N. ) -> ( ( 2nd ` z ) <N b <-> ( 2nd ` z ) e. b ) )
30	27, 29	sylan2 476	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( b e. N. /\ z e. ( N. X. N. ) ) -> ( ( 2nd ` z ) <N b <-> ( 2nd ` z ) e. b ) )
31	30	adantll 718	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( a e. N. /\ b e. N. ) /\ z e. ( N. X. N. ) ) -> ( ( 2nd ` z ) <N b <-> ( 2nd ` z ) e. b ) )
32	31	anbi2d 708	. . . . . . . . . . . . . . . . . . . . 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 260	. . . . . . . . . . . . . . . . . . . 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 2943	. . . . . . . . . . . . . . . . . . 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 262	. . . . . . . . . . . . . . . . . 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 6837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( z e. ( N. X. N. ) -> ( 1st ` z ) e. N. )
37		elequ2 1875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( m = b -> ( d e. m <-> d e. b ) )
38	37	imbi1d 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( c = ( 1st ` z ) -> <. c , d >. = <. ( 1st ` z ) , d >. )
42	41	breq2d 4438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( c = ( 1st ` z ) -> ( x ~Q <. c , d >. <-> x ~Q <. ( 1st ` z ) , d >. ) )
43	42	rexbidv 2946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( c = ( 1st ` z ) -> ( E. x e. Q. x ~Q <. c , d >. <-> E. x e. Q. x ~Q <. ( 1st ` z ) , d >. ) )
44	43	imbi2d 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( d = ( 2nd ` z ) -> ( d e. b <-> ( 2nd ` z ) e. b ) )
48		opeq2 4191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( d = ( 2nd ` z ) -> <. ( 1st ` z ) , d >. = <. ( 1st ` z ) , ( 2nd ` z ) >. )
49	48	breq2d 4438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( d = ( 2nd ` z ) -> ( x ~Q <. ( 1st ` z ) , d >. <-> x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
50	49	rexbidv 2946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 43	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1199	. . . . . . . . . . . . . . . . . . . . . . . . . 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 6844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( z e. ( N. X. N. ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
60	59	breq2d 4438	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z e. ( N. X. N. ) -> ( x ~Q z <-> x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
61	60	rexbidv 2946	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1027	. . . . . . . . . . . . . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . . . . . . . . . . . . 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 9345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( <. a , b >. ~Q z /\ x ~Q z ) -> x ~Q z )
67		simpl 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( <. a , b >. ~Q z /\ x ~Q z ) -> <. a , b >. ~Q z )
68	65, 66, 67	ertr4d 7390	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( <. a , b >. ~Q z /\ x ~Q z ) -> x ~Q <. a , b >. )
69	68	ex 435	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( <. a , b >. ~Q z -> ( x ~Q z -> x ~Q <. a , b >. ) )
70	69	reximdv 2906	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( <. a , b >. ~Q z -> ( E. x e. Q. x ~Q z -> E. x e. Q. x ~Q <. a , b >. ) )
71	63, 70	syl5com 31	. . . . . . . . . . . . . . . . . . . . . . . 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 1207	. . . . . . . . . . . . . . . . . . . . . . 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 81	. . . . . . . . . . . . . . . . . . . . . 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 432	. . . . . . . . . . . . . . . . . . . . 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 2924	. . . . . . . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . . . . . . 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 82	. . . . . . . . . . . . . . . . . 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 231	. . . . . . . . . . . . . . . . 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 83	. . . . . . . . . . . . . . . 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 9320	. . . . . . . . . . . . . . . . . . . 20 |- ( a .N b ) = ( b .N a )
81		enqbreq 9343	. . . . . . . . . . . . . . . . . . . . 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 649	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. N. /\ b e. N. ) -> ( <. a , b >. ~Q <. a , b >. <-> ( a .N b ) = ( b .N a ) ) )
83	80, 82	mpbiri 236	. . . . . . . . . . . . . . . . . . 19 |- ( ( a e. N. /\ b e. N. ) -> <. a , b >. ~Q <. a , b >. )
84		opelxpi 4886	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. N. /\ b e. N. ) -> <. a , b >. e. ( N. X. N. ) )
85		breq1 4429	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = <. a , b >. -> ( y ~Q z <-> <. a , b >. ~Q z ) )
86		vex 3090	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- a e. _V
87	86, 5	op2ndd 6818	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y = <. a , b >. -> ( 2nd ` y ) = b )
88	87	breq2d 4438	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = <. a , b >. -> ( ( 2nd ` z ) <N ( 2nd ` y ) <-> ( 2nd ` z ) <N b ) )
89	88	notbid 295	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = <. a , b >. -> ( -. ( 2nd ` z ) <N ( 2nd ` y ) <-> -. ( 2nd ` z ) <N b ) )
90	85, 89	imbi12d 321	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y = <. a , b >. -> ( ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) <-> ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) ) )
91	90	ralbidv 2871	. . . . . . . . . . . . . . . . . . . . . 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 9336	. . . . . . . . . . . . . . . . . . . . . 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 3237	. . . . . . . . . . . . . . . . . . . . 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 629	. . . . . . . . . . . . . . . . . . . 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 17	. . . . . . . . . . . . . . . . . . 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 4429	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = <. a , b >. -> ( x ~Q <. a , b >. <-> <. a , b >. ~Q <. a , b >. ) )
97	96	rspcev 3188	. . . . . . . . . . . . . . . . . . . 20 |- ( ( <. a , b >. e. Q. /\ <. a , b >. ~Q <. a , b >. ) -> E. x e. Q. x ~Q <. a , b >. )
98	97	expcom 436	. . . . . . . . . . . . . . . . . . 19 |- ( <. a , b >. ~Q <. a , b >. -> ( <. a , b >. e. Q. -> E. x e. Q. x ~Q <. a , b >. ) )
99	83, 95, 98	sylsyld 58	. . . . . . . . . . . . . . . . . 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 32	. . . . . . . . . . . . . . . . 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 47	. . . . . . . . . . . . . . . 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 163	. . . . . . . . . . . . . . 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 2852	. . . . . . . . . . . . . 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 216	. . . . . . . . . . . . 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 6697	. . . . . . . . . . 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 2798	. . . . . . . . . . 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 17	. . . . . . . . . 10 |- ( y e. On -> ( a e. N. -> A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
109		rsp 2798	. . . . . . . . . 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 34	. . . . . . . . 9 |- ( y e. On -> ( a e. N. -> ( b e. N. -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) ) )
111	110	impd 432	. . . . . . . 8 |- ( y e. On -> ( ( a e. N. /\ b e. N. ) -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
112	111	com12 32	. . . . . . 7 |- ( ( a e. N. /\ b e. N. ) -> ( y e. On -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
113	112	rexlimdv 2922	. . . . . 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 4430	. . . . . 6 |- ( A = <. a , b >. -> ( x ~Q A <-> x ~Q <. a , b >. ) )
116	115	rexbidv 2946	. . . . 5 |- ( A = <. a , b >. -> ( E. x e. Q. x ~Q A <-> E. x e. Q. x ~Q <. a , b >. ) )
117	114, 116	syl5ibrcom 225	. . . 4 |- ( ( a e. N. /\ b e. N. ) -> ( A = <. a , b >. -> E. x e. Q. x ~Q A ) )
118	117	rexlimivv 2929	. . 3 |- ( E. a e. N. E. b e. N. A = <. a , b >. -> E. x e. Q. x ~Q A )
119	1, 118	sylbi 198	. 2 |- ( A e. ( N. X. N. ) -> E. x e. Q. x ~Q A )
120		breq2 4430	. . . . . 6 |- ( a = A -> ( x ~Q a <-> x ~Q A ) )
121		breq2 4430	. . . . . 6 |- ( a = A -> ( y ~Q a <-> y ~Q A ) )
122	120, 121	anbi12d 715	. . . . 5 |- ( a = A -> ( ( x ~Q a /\ y ~Q a ) <-> ( x ~Q A /\ y ~Q A ) ) )
123	122	imbi1d 318	. . . 4 |- ( a = A -> ( ( ( x ~Q a /\ y ~Q a ) -> x = y ) <-> ( ( x ~Q A /\ y ~Q A ) -> x = y ) ) )
124	123	2ralbidv 2876	. . 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 458	. . . . . 6 |- ( ( x ~Q a /\ y ~Q a ) -> x ~Q a )
127		simpr 462	. . . . . 6 |- ( ( x ~Q a /\ y ~Q a ) -> y ~Q a )
128	125, 126, 127	ertr4d 7390	. . . . 5 |- ( ( x ~Q a /\ y ~Q a ) -> x ~Q y )
129		mulcompi 9320	. . . . . . . . . . 11 |- ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` x ) )
130		elpqn 9349	. . . . . . . . . . . . . . 15 |- ( y e. Q. -> y e. ( N. X. N. ) )
131		breq1 4429	. . . . . . . . . . . . . . . . . . 19 |- ( y = x -> ( y ~Q z <-> x ~Q z ) )
132		fveq2 5881	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = x -> ( 2nd ` y ) = ( 2nd ` x ) )
133	132	breq2d 4438	. . . . . . . . . . . . . . . . . . . 20 |- ( y = x -> ( ( 2nd ` z ) <N ( 2nd ` y ) <-> ( 2nd ` z ) <N ( 2nd ` x ) ) )
134	133	notbid 295	. . . . . . . . . . . . . . . . . . 19 |- ( y = x -> ( -. ( 2nd ` z ) <N ( 2nd ` y ) <-> -. ( 2nd ` z ) <N ( 2nd ` x ) ) )
135	131, 134	imbi12d 321	. . . . . . . . . . . . . . . . . 18 |- ( y = x -> ( ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) <-> ( x ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` x ) ) ) )
136	135	ralbidv 2871	. . . . . . . . . . . . . . . . 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 3237	. . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . 15 |- ( x e. Q. -> A. z e. ( N. X. N. ) ( x ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` x ) ) )
139		breq2 4430	. . . . . . . . . . . . . . . . 17 |- ( z = y -> ( x ~Q z <-> x ~Q y ) )
140		fveq2 5881	. . . . . . . . . . . . . . . . . . 19 |- ( z = y -> ( 2nd ` z ) = ( 2nd ` y ) )
141	140	breq1d 4436	. . . . . . . . . . . . . . . . . 18 |- ( z = y -> ( ( 2nd ` z ) <N ( 2nd ` x ) <-> ( 2nd ` y ) <N ( 2nd ` x ) ) )
142	141	notbid 295	. . . . . . . . . . . . . . . . 17 |- ( z = y -> ( -. ( 2nd ` z ) <N ( 2nd ` x ) <-> -. ( 2nd ` y ) <N ( 2nd ` x ) ) )
143	139, 142	imbi12d 321	. . . . . . . . . . . . . . . 16 |- ( z = y -> ( ( x ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` x ) ) <-> ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) ) ) )
144	143	rspcva 3186	. . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . 14 |- ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) ) )
146	145	imp 430	. . . . . . . . . . . . 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 23	. . . . . . . . . . . . . . . . . 18 |- ( x ~Q y -> x ~Q y )
149	147, 148	ersym 7383	. . . . . . . . . . . . . . . . 17 |- ( x ~Q y -> y ~Q x )
150		elpqn 9349	. . . . . . . . . . . . . . . . . 18 |- ( x e. Q. -> x e. ( N. X. N. ) )
151	92	rabeq2i 3084	. . . . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . . 18 |- ( y e. Q. -> A. z e. ( N. X. N. ) ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) )
153		breq2 4430	. . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( y ~Q z <-> y ~Q x ) )
154		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z = x -> ( 2nd ` z ) = ( 2nd ` x ) )
155	154	breq1d 4436	. . . . . . . . . . . . . . . . . . . . 21 |- ( z = x -> ( ( 2nd ` z ) <N ( 2nd ` y ) <-> ( 2nd ` x ) <N ( 2nd ` y ) ) )
156	155	notbid 295	. . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( -. ( 2nd ` z ) <N ( 2nd ` y ) <-> -. ( 2nd ` x ) <N ( 2nd ` y ) ) )
157	153, 156	imbi12d 321	. . . . . . . . . . . . . . . . . . 19 |- ( z = x -> ( ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) <-> ( y ~Q x -> -. ( 2nd ` x ) <N ( 2nd ` y ) ) ) )
158	157	rspcva 3186	. . . . . . . . . . . . . . . . . 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 479	. . . . . . . . . . . . . . . . 17 |- ( ( x e. Q. /\ y e. Q. ) -> ( y ~Q x -> -. ( 2nd ` x ) <N ( 2nd ` y ) ) )
160	149, 159	syl5 33	. . . . . . . . . . . . . . . 16 |- ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y -> -. ( 2nd ` x ) <N ( 2nd ` y ) ) )
161	160	imp 430	. . . . . . . . . . . . . . 15 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> -. ( 2nd ` x ) <N ( 2nd ` y ) )
162		xp2nd 6838	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( N. X. N. ) -> ( 2nd ` x ) e. N. )
163	150, 162	syl 17	. . . . . . . . . . . . . . . . 17 |- ( x e. Q. -> ( 2nd ` x ) e. N. )
164	163	ad2antrr 730	. . . . . . . . . . . . . . . 16 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 2nd ` x ) e. N. )
165		xp2nd 6838	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( N. X. N. ) -> ( 2nd ` y ) e. N. )
166	130, 165	syl 17	. . . . . . . . . . . . . . . . 17 |- ( y e. Q. -> ( 2nd ` y ) e. N. )
167	166	ad2antlr 731	. . . . . . . . . . . . . . . 16 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 2nd ` y ) e. N. )
168		ltsopi 9312	. . . . . . . . . . . . . . . . . . 19 |- <N Or N.
169		sotric 4801	. . . . . . . . . . . . . . . . . . 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 674	. . . . . . . . . . . . . . . . . 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 295	. . . . . . . . . . . . . . . . 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 292	. . . . . . . . . . . . . . . . 17 |- ( ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) <-> -. -. ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) )
173	171, 172	syl6bbr 266	. . . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . . 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 213	. . . . . . . . . . . . . 14 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) )
176	175	ord 378	. . . . . . . . . . . . 13 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( -. ( 2nd ` x ) = ( 2nd ` y ) -> ( 2nd ` y ) <N ( 2nd ` x ) ) )
177	146, 176	mt3d 128	. . . . . . . . . . . 12 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 2nd ` x ) = ( 2nd ` y ) )
178	177	oveq2d 6321	. . . . . . . . . . 11 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 1st ` x ) .N ( 2nd ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` y ) ) )
179	129, 178	syl5eq 2482	. . . . . . . . . 10 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` y ) ) )
180		1st2nd2 6844	. . . . . . . . . . . . . 14 |- ( x e. ( N. X. N. ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
181		1st2nd2 6844	. . . . . . . . . . . . . 14 |- ( y e. ( N. X. N. ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
182	180, 181	breqan12d 4441	. . . . . . . . . . . . 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 6837	. . . . . . . . . . . . . . 15 |- ( x e. ( N. X. N. ) -> ( 1st ` x ) e. N. )
184	183, 162	jca 534	. . . . . . . . . . . . . 14 |- ( x e. ( N. X. N. ) -> ( ( 1st ` x ) e. N. /\ ( 2nd ` x ) e. N. ) )
185		xp1st 6837	. . . . . . . . . . . . . . 15 |- ( y e. ( N. X. N. ) -> ( 1st ` y ) e. N. )
186	185, 165	jca 534	. . . . . . . . . . . . . 14 |- ( y e. ( N. X. N. ) -> ( ( 1st ` y ) e. N. /\ ( 2nd ` y ) e. N. ) )
187		enqbreq 9343	. . . . . . . . . . . . . 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 479	. . . . . . . . . . . . 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 256	. . . . . . . . . . . 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 479	. . . . . . . . . . 11 |- ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) ) )
191	190	biimpa 486	. . . . . . . . . 10 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) )
192	179, 191	eqtrd 2470	. . . . . . . . 9 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) )
193	150	ad2antrr 730	. . . . . . . . . 10 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> x e. ( N. X. N. ) )
194		mulcanpi 9324	. . . . . . . . . . 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 665	. . . . . . . . . 10 |- ( x e. ( N. X. N. ) -> ( ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) <-> ( 1st ` x ) = ( 1st ` y ) ) )
196	193, 195	syl 17	. . . . . . . . 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 213	. . . . . . . 8 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 1st ` x ) = ( 1st ` y ) )
198	197, 177	opeq12d 4198	. . . . . . 7 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. = <. ( 1st ` y ) , ( 2nd ` y ) >. )
199	193, 180	syl 17	. . . . . . 7 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
200	130	ad2antlr 731	. . . . . . . 8 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> y e. ( N. X. N. ) )
201	200, 181	syl 17	. . . . . . 7 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
202	198, 199, 201	3eqtr4d 2480	. . . . . 6 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> x = y )
203	202	ex 435	. . . . 5 |- ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y -> x = y ) )
204	128, 203	syl5 33	. . . 4 |- ( ( x e. Q. /\ y e. Q. ) -> ( ( x ~Q a /\ y ~Q a ) -> x = y ) )
205	204	rgen2a 2859	. . 3 |- A. x e. Q. A. y e. Q. ( ( x ~Q a /\ y ~Q a ) -> x = y )
206	124, 205	vtoclg 3145	. 2 |- ( A e. ( N. X. N. ) -> A. x e. Q. A. y e. Q. ( ( x ~Q A /\ y ~Q A ) -> x = y ) )
207		breq1 4429	. . 3 |- ( x = y -> ( x ~Q A <-> y ~Q A ) )
208	207	reu4 3271	. 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 668	1 |- ( A e. ( N. X. N. ) -> E! x e. Q. x ~Q A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   \/ wo 369   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1870   A.wral 2782   E.wrex 2783   E!wreu 2784   <.cop 4008   class class class wbr 4426   Or wor 4774   X. cxp 4852   Oncon0 5442   suc csuc 5444   ` cfv 5601  (class class class)co 6305   1stc1st 6805   2ndc2nd 6806   Er wer 7368   N.cnpi 9268   .N cmi 9270   <N clti 9271   ~Q ceq 9275   Q.cnq 9276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-1st 6807  df-2nd 6808  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-oadd 7194  df-omul 7195  df-er 7371  df-ni 9296  df-mi 9298  df-lti 9299  df-enq 9335  df-nq 9336

This theorem is referenced by:  nqerf  9354  enqeq  9358