Theorem nqereu 9361

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 4871	. . 3 |- ( A e. ( N. X. N. ) <-> E. a e. N. E. b e. N. A = <. a , b >. )
2		pion 9311	. . . . . . . . 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 3083	. . . . . . . . 9 |- b e. _V
6	5	sucid 5521	. . . . . . . 8 |- b e. suc b
7		eleq2 2496	. . . . . . . . 9 |- ( y = suc b -> ( b e. y <-> b e. suc b ) )
8	7	rspcev 3182	. . . . . . . 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 1877	. . . . . . . . . . . . . 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 2866	. . . . . . . . . . . 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 4187	. . . . . . . . . . . . . . . . . . 19 |- ( c = a -> <. c , d >. = <. a , d >. )
15	14	breq2d 4435	. . . . . . . . . . . . . . . . . 18 |- ( c = a -> ( x ~Q <. c , d >. <-> x ~Q <. a , d >. ) )
16	15	rexbidv 2936	. . . . . . . . . . . . . . . . 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 1875	. . . . . . . . . . . . . . . . 17 |- ( d = b -> ( d e. m <-> b e. m ) )
19		opeq2 4188	. . . . . . . . . . . . . . . . . . 19 |- ( d = b -> <. a , d >. = <. a , b >. )
20	19	breq2d 4435	. . . . . . . . . . . . . . . . . 18 |- ( d = b -> ( x ~Q <. a , d >. <-> x ~Q <. a , b >. ) )
21	20	rexbidv 2936	. . . . . . . . . . . . . . . . 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 3062	. . . . . . . . . . . . . . 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 2853	. . . . . . . . . . . . . 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 2870	. . . . . . . . . . . . . . . . . . 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 9319	. . . . . . . . . . . . . . . . . . . . . . . . 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 2933	. . . . . . . . . . . . . . . . . . 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 1877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( c = ( 1st ` z ) -> <. c , d >. = <. ( 1st ` z ) , d >. )
42	41	breq2d 4435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( c = ( 1st ` z ) -> ( x ~Q <. c , d >. <-> x ~Q <. ( 1st ` z ) , d >. ) )
43	42	rexbidv 2936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( d = ( 2nd ` z ) -> ( d e. b <-> ( 2nd ` z ) e. b ) )
48		opeq2 4188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( d = ( 2nd ` z ) -> <. ( 1st ` z ) , d >. = <. ( 1st ` z ) , ( 2nd ` z ) >. )
49	48	breq2d 4435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( d = ( 2nd ` z ) -> ( x ~Q <. ( 1st ` z ) , d >. <-> x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
50	49	rexbidv 2936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4435	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z e. ( N. X. N. ) -> ( x ~Q z <-> x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
61	60	rexbidv 2936	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 9353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7393	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2896	. . . . . . . . . . . . . . . . . . . . . . . . 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 2914	. . . . . . . . . . . . . . . . . . . 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 9328	. . . . . . . . . . . . . . . . . . . 20 |- ( a .N b ) = ( b .N a )
81		enqbreq 9351	. . . . . . . . . . . . . . . . . . . . 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 4885	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. N. /\ b e. N. ) -> <. a , b >. e. ( N. X. N. ) )
85		breq1 4426	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = <. a , b >. -> ( y ~Q z <-> <. a , b >. ~Q z ) )
86		vex 3083	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- a e. _V
87	86, 5	op2ndd 6818	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y = <. a , b >. -> ( 2nd ` y ) = b )
88	87	breq2d 4435	. . . . . . . . . . . . . . . . . . . . . . . . 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 2861	. . . . . . . . . . . . . . . . . . . . . 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 9344	. . . . . . . . . . . . . . . . . . . . . 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 3230	. . . . . . . . . . . . . . . . . . . . 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 4426	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = <. a , b >. -> ( x ~Q <. a , b >. <-> <. a , b >. ~Q <. a , b >. ) )
97	96	rspcev 3182	. . . . . . . . . . . . . . . . . . . 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 2842	. . . . . . . . . . . . . 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 2788	. . . . . . . . . . 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 2788	. . . . . . . . . 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 2912	. . . . . 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 4427	. . . . . 6 |- ( A = <. a , b >. -> ( x ~Q A <-> x ~Q <. a , b >. ) )
116	115	rexbidv 2936	. . . . 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 2919	. . 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 4427	. . . . . 6 |- ( a = A -> ( x ~Q a <-> x ~Q A ) )
121		breq2 4427	. . . . . 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 2866	. . 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 7393	. . . . 5 |- ( ( x ~Q a /\ y ~Q a ) -> x ~Q y )
129		mulcompi 9328	. . . . . . . . . . 11 |- ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` x ) )
130		elpqn 9357	. . . . . . . . . . . . . . 15 |- ( y e. Q. -> y e. ( N. X. N. ) )
131		breq1 4426	. . . . . . . . . . . . . . . . . . 19 |- ( y = x -> ( y ~Q z <-> x ~Q z ) )
132		fveq2 5881	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = x -> ( 2nd ` y ) = ( 2nd ` x ) )
133	132	breq2d 4435	. . . . . . . . . . . . . . . . . . . 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 2861	. . . . . . . . . . . . . . . . 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 3230	. . . . . . . . . . . . . . . 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 4427	. . . . . . . . . . . . . . . . 17 |- ( z = y -> ( x ~Q z <-> x ~Q y ) )
140		fveq2 5881	. . . . . . . . . . . . . . . . . . 19 |- ( z = y -> ( 2nd ` z ) = ( 2nd ` y ) )
141	140	breq1d 4433	. . . . . . . . . . . . . . . . . 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 3180	. . . . . . . . . . . . . . 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 22	. . . . . . . . . . . . . . . . . 18 |- ( x ~Q y -> x ~Q y )
149	147, 148	ersym 7386	. . . . . . . . . . . . . . . . 17 |- ( x ~Q y -> y ~Q x )
150		elpqn 9357	. . . . . . . . . . . . . . . . . 18 |- ( x e. Q. -> x e. ( N. X. N. ) )
151	92	rabeq2i 3077	. . . . . . . . . . . . . . . . . . 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 4427	. . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( y ~Q z <-> y ~Q x ) )
154		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z = x -> ( 2nd ` z ) = ( 2nd ` x ) )
155	154	breq1d 4433	. . . . . . . . . . . . . . . . . . . . 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 3180	. . . . . . . . . . . . . . . . . 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 9320	. . . . . . . . . . . . . . . . . . 19 |- <N Or N.
169		sotric 4800	. . . . . . . . . . . . . . . . . . 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 2475	. . . . . . . . . 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 4439	. . . . . . . . . . . . 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 9351	. . . . . . . . . . . . . 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 2463	. . . . . . . . 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 9332	. . . . . . . . . . 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 4195	. . . . . . 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 2473	. . . . . 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 2849	. . 3 |- A. x e. Q. A. y e. Q. ( ( x ~Q a /\ y ~Q a ) -> x = y )
206	124, 205	vtoclg 3139	. 2 |- ( A e. ( N. X. N. ) -> A. x e. Q. A. y e. Q. ( ( x ~Q A /\ y ~Q A ) -> x = y ) )
207		breq1 4426	. . 3 |- ( x = y -> ( x ~Q A <-> y ~Q A ) )
208	207	reu4 3264	. 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 1872   A.wral 2771   E.wrex 2772   E!wreu 2773   <.cop 4004   class class class wbr 4423   Or wor 4773   X. cxp 4851   Oncon0 5442   suc csuc 5444   ` cfv 5601  (class class class)co 6305   1stc1st 6805   2ndc2nd 6806   Er wer 7371   N.cnpi 9276   .N cmi 9278   <N clti 9279   ~Q ceq 9283   Q.cnq 9284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  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 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  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 7039  df-recs 7101  df-rdg 7139  df-oadd 7197  df-omul 7198  df-er 7374  df-ni 9304  df-mi 9306  df-lti 9307  df-enq 9343  df-nq 9344

This theorem is referenced by:  nqerf  9362  enqeq  9366