Theorem nqereu 9385

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 4874	. . 3 |- ( A e. ( N. X. N. ) <-> E. a e. N. E. b e. N. A = <. a , b >. )
2		pion 9335	. . . . . . . . 9 |- ( b e. N. -> b e. On )
3		suceloni 6672	. . . . . . . . 9 |- ( b e. On -> suc b e. On )
4	2, 3	syl 17	. . . . . . . 8 |- ( b e. N. -> suc b e. On )
5		vex 3060	. . . . . . . . 9 |- b e. _V
6	5	sucid 5525	. . . . . . . 8 |- b e. suc b
7		eleq2 2529	. . . . . . . . 9 |- ( y = suc b -> ( b e. y <-> b e. suc b ) )
8	7	rspcev 3162	. . . . . . . 8 |- ( ( suc b e. On /\ b e. suc b ) -> E. y e. On b e. y )
9	4, 6, 8	sylancl 673	. . . . . . 7 |- ( b e. N. -> E. y e. On b e. y )
10	9	adantl 472	. . . . . 6 |- ( ( a e. N. /\ b e. N. ) -> E. y e. On b e. y )
11		elequ2 1912	. . . . . . . . . . . . . 14 |- ( y = m -> ( b e. y <-> b e. m ) )
12	11	imbi1d 323	. . . . . . . . . . . . 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 2844	. . . . . . . . . . . 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 4180	. . . . . . . . . . . . . . . . . . 19 |- ( c = a -> <. c , d >. = <. a , d >. )
15	14	breq2d 4430	. . . . . . . . . . . . . . . . . 18 |- ( c = a -> ( x ~Q <. c , d >. <-> x ~Q <. a , d >. ) )
16	15	rexbidv 2913	. . . . . . . . . . . . . . . . 17 |- ( c = a -> ( E. x e. Q. x ~Q <. c , d >. <-> E. x e. Q. x ~Q <. a , d >. ) )
17	16	imbi2d 322	. . . . . . . . . . . . . . . 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 1905	. . . . . . . . . . . . . . . . 17 |- ( d = b -> ( d e. m <-> b e. m ) )
19		opeq2 4181	. . . . . . . . . . . . . . . . . . 19 |- ( d = b -> <. a , d >. = <. a , b >. )
20	19	breq2d 4430	. . . . . . . . . . . . . . . . . 18 |- ( d = b -> ( x ~Q <. a , d >. <-> x ~Q <. a , b >. ) )
21	20	rexbidv 2913	. . . . . . . . . . . . . . . . 17 |- ( d = b -> ( E. x e. Q. x ~Q <. a , d >. <-> E. x e. Q. x ~Q <. a , b >. ) )
22	18, 21	imbi12d 326	. . . . . . . . . . . . . . . 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 3039	. . . . . . . . . . . . . . 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 2831	. . . . . . . . . . . . . 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 2848	. . . . . . . . . . . . . . . . . . 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 427	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) <-> ( <. a , b >. ~Q z /\ ( 2nd ` z ) <N b ) )
27		xp2nd 6856	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( z e. ( N. X. N. ) -> ( 2nd ` z ) e. N. )
28		ltpiord 9343	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 2nd ` z ) e. N. /\ b e. N. ) -> ( ( 2nd ` z ) <N b <-> ( 2nd ` z ) e. b ) )
29	28	ancoms 459	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( b e. N. /\ ( 2nd ` z ) e. N. ) -> ( ( 2nd ` z ) <N b <-> ( 2nd ` z ) e. b ) )
30	27, 29	sylan2 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( b e. N. /\ z e. ( N. X. N. ) ) -> ( ( 2nd ` z ) <N b <-> ( 2nd ` z ) e. b ) )
31	30	adantll 725	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( a e. N. /\ b e. N. ) /\ z e. ( N. X. N. ) ) -> ( ( 2nd ` z ) <N b <-> ( 2nd ` z ) e. b ) )
32	31	anbi2d 715	. . . . . . . . . . . . . . . . . . . . 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 265	. . . . . . . . . . . . . . . . . . . 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 2910	. . . . . . . . . . . . . . . . . . 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 267	. . . . . . . . . . . . . . . . . 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 6855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( z e. ( N. X. N. ) -> ( 1st ` z ) e. N. )
37		elequ2 1912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( m = b -> ( d e. m <-> d e. b ) )
38	37	imbi1d 323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4180	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( c = ( 1st ` z ) -> <. c , d >. = <. ( 1st ` z ) , d >. )
42	41	breq2d 4430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( c = ( 1st ` z ) -> ( x ~Q <. c , d >. <-> x ~Q <. ( 1st ` z ) , d >. ) )
43	42	rexbidv 2913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( c = ( 1st ` z ) -> ( E. x e. Q. x ~Q <. c , d >. <-> E. x e. Q. x ~Q <. ( 1st ` z ) , d >. ) )
44	43	imbi2d 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( d = ( 2nd ` z ) -> ( d e. b <-> ( 2nd ` z ) e. b ) )
48		opeq2 4181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( d = ( 2nd ` z ) -> <. ( 1st ` z ) , d >. = <. ( 1st ` z ) , ( 2nd ` z ) >. )
49	48	breq2d 4430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( d = ( 2nd ` z ) -> ( x ~Q <. ( 1st ` z ) , d >. <-> x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
50	49	rexbidv 2913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1208	. . . . . . . . . . . . . . . . . . . . . . . . . 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 6862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( z e. ( N. X. N. ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
60	59	breq2d 4430	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z e. ( N. X. N. ) -> ( x ~Q z <-> x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
61	60	rexbidv 2913	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1036	. . . . . . . . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . . . . . . . . . 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 9377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( <. a , b >. ~Q z /\ x ~Q z ) -> x ~Q z )
67		simpl 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( <. a , b >. ~Q z /\ x ~Q z ) -> <. a , b >. ~Q z )
68	65, 66, 67	ertr4d 7413	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( <. a , b >. ~Q z /\ x ~Q z ) -> x ~Q <. a , b >. )
69	68	ex 440	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( <. a , b >. ~Q z -> ( x ~Q z -> x ~Q <. a , b >. ) )
70	69	reximdv 2873	. . . . . . . . . . . . . . . . . . . . . . . . 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 1217	. . . . . . . . . . . . . . . . . . . . . . 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 437	. . . . . . . . . . . . . . . . . . . . 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 2891	. . . . . . . . . . . . . . . . . . . 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 440	. . . . . . . . . . . . . . . . . . 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 236	. . . . . . . . . . . . . . . . 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 9352	. . . . . . . . . . . . . . . . . . . 20 |- ( a .N b ) = ( b .N a )
81		enqbreq 9375	. . . . . . . . . . . . . . . . . . . . 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 655	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. N. /\ b e. N. ) -> ( <. a , b >. ~Q <. a , b >. <-> ( a .N b ) = ( b .N a ) ) )
83	80, 82	mpbiri 241	. . . . . . . . . . . . . . . . . . 19 |- ( ( a e. N. /\ b e. N. ) -> <. a , b >. ~Q <. a , b >. )
84		opelxpi 4888	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. N. /\ b e. N. ) -> <. a , b >. e. ( N. X. N. ) )
85		breq1 4421	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = <. a , b >. -> ( y ~Q z <-> <. a , b >. ~Q z ) )
86		vex 3060	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- a e. _V
87	86, 5	op2ndd 6836	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y = <. a , b >. -> ( 2nd ` y ) = b )
88	87	breq2d 4430	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = <. a , b >. -> ( ( 2nd ` z ) <N ( 2nd ` y ) <-> ( 2nd ` z ) <N b ) )
89	88	notbid 300	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = <. a , b >. -> ( -. ( 2nd ` z ) <N ( 2nd ` y ) <-> -. ( 2nd ` z ) <N b ) )
90	85, 89	imbi12d 326	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y = <. a , b >. -> ( ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) <-> ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) ) )
91	90	ralbidv 2839	. . . . . . . . . . . . . . . . . . . . . 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 9368	. . . . . . . . . . . . . . . . . . . . . 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 3210	. . . . . . . . . . . . . . . . . . . . 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 635	. . . . . . . . . . . . . . . . . . . 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 4421	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = <. a , b >. -> ( x ~Q <. a , b >. <-> <. a , b >. ~Q <. a , b >. ) )
97	96	rspcev 3162	. . . . . . . . . . . . . . . . . . . 20 |- ( ( <. a , b >. e. Q. /\ <. a , b >. ~Q <. a , b >. ) -> E. x e. Q. x ~Q <. a , b >. )
98	97	expcom 441	. . . . . . . . . . . . . . . . . . 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 165	. . . . . . . . . . . . . . 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 2820	. . . . . . . . . . . . . 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 218	. . . . . . . . . . . . 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 6715	. . . . . . . . . . 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 2766	. . . . . . . . . . 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 2766	. . . . . . . . . 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 437	. . . . . . . 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 2889	. . . . . 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 4422	. . . . . 6 |- ( A = <. a , b >. -> ( x ~Q A <-> x ~Q <. a , b >. ) )
116	115	rexbidv 2913	. . . . 5 |- ( A = <. a , b >. -> ( E. x e. Q. x ~Q A <-> E. x e. Q. x ~Q <. a , b >. ) )
117	114, 116	syl5ibrcom 230	. . . 4 |- ( ( a e. N. /\ b e. N. ) -> ( A = <. a , b >. -> E. x e. Q. x ~Q A ) )
118	117	rexlimivv 2896	. . 3 |- ( E. a e. N. E. b e. N. A = <. a , b >. -> E. x e. Q. x ~Q A )
119	1, 118	sylbi 200	. 2 |- ( A e. ( N. X. N. ) -> E. x e. Q. x ~Q A )
120		breq2 4422	. . . . . 6 |- ( a = A -> ( x ~Q a <-> x ~Q A ) )
121		breq2 4422	. . . . . 6 |- ( a = A -> ( y ~Q a <-> y ~Q A ) )
122	120, 121	anbi12d 722	. . . . 5 |- ( a = A -> ( ( x ~Q a /\ y ~Q a ) <-> ( x ~Q A /\ y ~Q A ) ) )
123	122	imbi1d 323	. . . 4 |- ( a = A -> ( ( ( x ~Q a /\ y ~Q a ) -> x = y ) <-> ( ( x ~Q A /\ y ~Q A ) -> x = y ) ) )
124	123	2ralbidv 2844	. . 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 463	. . . . . 6 |- ( ( x ~Q a /\ y ~Q a ) -> x ~Q a )
127		simpr 467	. . . . . 6 |- ( ( x ~Q a /\ y ~Q a ) -> y ~Q a )
128	125, 126, 127	ertr4d 7413	. . . . 5 |- ( ( x ~Q a /\ y ~Q a ) -> x ~Q y )
129		mulcompi 9352	. . . . . . . . . . 11 |- ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` x ) )
130		elpqn 9381	. . . . . . . . . . . . . . 15 |- ( y e. Q. -> y e. ( N. X. N. ) )
131		breq1 4421	. . . . . . . . . . . . . . . . . . 19 |- ( y = x -> ( y ~Q z <-> x ~Q z ) )
132		fveq2 5892	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = x -> ( 2nd ` y ) = ( 2nd ` x ) )
133	132	breq2d 4430	. . . . . . . . . . . . . . . . . . . 20 |- ( y = x -> ( ( 2nd ` z ) <N ( 2nd ` y ) <-> ( 2nd ` z ) <N ( 2nd ` x ) ) )
134	133	notbid 300	. . . . . . . . . . . . . . . . . . 19 |- ( y = x -> ( -. ( 2nd ` z ) <N ( 2nd ` y ) <-> -. ( 2nd ` z ) <N ( 2nd ` x ) ) )
135	131, 134	imbi12d 326	. . . . . . . . . . . . . . . . . 18 |- ( y = x -> ( ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) <-> ( x ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` x ) ) ) )
136	135	ralbidv 2839	. . . . . . . . . . . . . . . . 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 3210	. . . . . . . . . . . . . . . 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 470	. . . . . . . . . . . . . . 15 |- ( x e. Q. -> A. z e. ( N. X. N. ) ( x ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` x ) ) )
139		breq2 4422	. . . . . . . . . . . . . . . . 17 |- ( z = y -> ( x ~Q z <-> x ~Q y ) )
140		fveq2 5892	. . . . . . . . . . . . . . . . . . 19 |- ( z = y -> ( 2nd ` z ) = ( 2nd ` y ) )
141	140	breq1d 4428	. . . . . . . . . . . . . . . . . 18 |- ( z = y -> ( ( 2nd ` z ) <N ( 2nd ` x ) <-> ( 2nd ` y ) <N ( 2nd ` x ) ) )
142	141	notbid 300	. . . . . . . . . . . . . . . . 17 |- ( z = y -> ( -. ( 2nd ` z ) <N ( 2nd ` x ) <-> -. ( 2nd ` y ) <N ( 2nd ` x ) ) )
143	139, 142	imbi12d 326	. . . . . . . . . . . . . . . 16 |- ( z = y -> ( ( x ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` x ) ) <-> ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) ) ) )
144	143	rspcva 3160	. . . . . . . . . . . . . . 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 485	. . . . . . . . . . . . . 14 |- ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) ) )
146	145	imp 435	. . . . . . . . . . . . 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 7406	. . . . . . . . . . . . . . . . 17 |- ( x ~Q y -> y ~Q x )
150		elpqn 9381	. . . . . . . . . . . . . . . . . 18 |- ( x e. Q. -> x e. ( N. X. N. ) )
151	92	rabeq2i 3054	. . . . . . . . . . . . . . . . . . 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 470	. . . . . . . . . . . . . . . . . 18 |- ( y e. Q. -> A. z e. ( N. X. N. ) ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) )
153		breq2 4422	. . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( y ~Q z <-> y ~Q x ) )
154		fveq2 5892	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z = x -> ( 2nd ` z ) = ( 2nd ` x ) )
155	154	breq1d 4428	. . . . . . . . . . . . . . . . . . . . 21 |- ( z = x -> ( ( 2nd ` z ) <N ( 2nd ` y ) <-> ( 2nd ` x ) <N ( 2nd ` y ) ) )
156	155	notbid 300	. . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( -. ( 2nd ` z ) <N ( 2nd ` y ) <-> -. ( 2nd ` x ) <N ( 2nd ` y ) ) )
157	153, 156	imbi12d 326	. . . . . . . . . . . . . . . . . . 19 |- ( z = x -> ( ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) <-> ( y ~Q x -> -. ( 2nd ` x ) <N ( 2nd ` y ) ) ) )
158	157	rspcva 3160	. . . . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . . 15 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> -. ( 2nd ` x ) <N ( 2nd ` y ) )
162		xp2nd 6856	. . . . . . . . . . . . . . . . . 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 737	. . . . . . . . . . . . . . . 16 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 2nd ` x ) e. N. )
165		xp2nd 6856	. . . . . . . . . . . . . . . . . 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 738	. . . . . . . . . . . . . . . 16 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 2nd ` y ) e. N. )
168		ltsopi 9344	. . . . . . . . . . . . . . . . . . 19 |- <N Or N.
169		sotric 4803	. . . . . . . . . . . . . . . . . . 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 681	. . . . . . . . . . . . . . . . . 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 300	. . . . . . . . . . . . . . . . 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 297	. . . . . . . . . . . . . . . . 17 |- ( ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) <-> -. -. ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) )
173	171, 172	syl6bbr 271	. . . . . . . . . . . . . . . 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 671	. . . . . . . . . . . . . . 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 215	. . . . . . . . . . . . . 14 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) )
176	175	ord 383	. . . . . . . . . . . . 13 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( -. ( 2nd ` x ) = ( 2nd ` y ) -> ( 2nd ` y ) <N ( 2nd ` x ) ) )
177	146, 176	mt3d 130	. . . . . . . . . . . 12 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 2nd ` x ) = ( 2nd ` y ) )
178	177	oveq2d 6336	. . . . . . . . . . 11 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 1st ` x ) .N ( 2nd ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` y ) ) )
179	129, 178	syl5eq 2508	. . . . . . . . . 10 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` y ) ) )
180		1st2nd2 6862	. . . . . . . . . . . . . 14 |- ( x e. ( N. X. N. ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
181		1st2nd2 6862	. . . . . . . . . . . . . 14 |- ( y e. ( N. X. N. ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
182	180, 181	breqan12d 4434	. . . . . . . . . . . . 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 6855	. . . . . . . . . . . . . . 15 |- ( x e. ( N. X. N. ) -> ( 1st ` x ) e. N. )
184	183, 162	jca 539	. . . . . . . . . . . . . 14 |- ( x e. ( N. X. N. ) -> ( ( 1st ` x ) e. N. /\ ( 2nd ` x ) e. N. ) )
185		xp1st 6855	. . . . . . . . . . . . . . 15 |- ( y e. ( N. X. N. ) -> ( 1st ` y ) e. N. )
186	185, 165	jca 539	. . . . . . . . . . . . . 14 |- ( y e. ( N. X. N. ) -> ( ( 1st ` y ) e. N. /\ ( 2nd ` y ) e. N. ) )
187		enqbreq 9375	. . . . . . . . . . . . . 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 484	. . . . . . . . . . . . 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 261	. . . . . . . . . . . 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 484	. . . . . . . . . . 11 |- ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) ) )
191	190	biimpa 491	. . . . . . . . . 10 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) )
192	179, 191	eqtrd 2496	. . . . . . . . 9 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) )
193	150	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> x e. ( N. X. N. ) )
194		mulcanpi 9356	. . . . . . . . . . 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 671	. . . . . . . . . 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 215	. . . . . . . 8 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 1st ` x ) = ( 1st ` y ) )
198	197, 177	opeq12d 4188	. . . . . . 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 738	. . . . . . . 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 2506	. . . . . 6 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> x = y )
203	202	ex 440	. . . . 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 2827	. . 3 |- A. x e. Q. A. y e. Q. ( ( x ~Q a /\ y ~Q a ) -> x = y )
206	124, 205	vtoclg 3119	. 2 |- ( A e. ( N. X. N. ) -> A. x e. Q. A. y e. Q. ( ( x ~Q A /\ y ~Q A ) -> x = y ) )
207		breq1 4421	. . 3 |- ( x = y -> ( x ~Q A <-> y ~Q A ) )
208	207	reu4 3244	. 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 675	1 |- ( A e. ( N. X. N. ) -> E! x e. Q. x ~Q A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   \/ wo 374   /\ wa 375   /\ w3a 991   = wceq 1455   e. wcel 1898   A.wral 2749   E.wrex 2750   E!wreu 2751   <.cop 3986   class class class wbr 4418   Or wor 4776   X. cxp 4854   Oncon0 5446   suc csuc 5448   ` cfv 5605  (class class class)co 6320   1stc1st 6823   2ndc2nd 6824   Er wer 7391   N.cnpi 9300   .N cmi 9302   <N clti 9303   ~Q ceq 9307   Q.cnq 9308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-1st 6825  df-2nd 6826  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-oadd 7217  df-omul 7218  df-er 7394  df-ni 9328  df-mi 9330  df-lti 9331  df-enq 9367  df-nq 9368

This theorem is referenced by:  nqerf  9386  enqeq  9390