Theorem nqereu 9296

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 5010	. . 3 |- ( A e. ( N. X. N. ) <-> E. a e. N. E. b e. N. A = <. a , b >. )
2		pion 9246	. . . . . . . . 9 |- ( b e. N. -> b e. On )
3		suceloni 6619	. . . . . . . . 9 |- ( b e. On -> suc b e. On )
4	2, 3	syl 16	. . . . . . . 8 |- ( b e. N. -> suc b e. On )
5		vex 3109	. . . . . . . . 9 |- b e. _V
6	5	sucid 4950	. . . . . . . 8 |- b e. suc b
7		eleq2 2533	. . . . . . . . 9 |- ( y = suc b -> ( b e. y <-> b e. suc b ) )
8	7	rspcev 3207	. . . . . . . 8 |- ( ( suc b e. On /\ b e. suc b ) -> E. y e. On b e. y )
9	4, 6, 8	sylancl 662	. . . . . . 7 |- ( b e. N. -> E. y e. On b e. y )
10	9	adantl 466	. . . . . 6 |- ( ( a e. N. /\ b e. N. ) -> E. y e. On b e. y )
11		elequ2 1767	. . . . . . . . . . . . . 14 |- ( y = m -> ( b e. y <-> b e. m ) )
12	11	imbi1d 317	. . . . . . . . . . . . 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 2901	. . . . . . . . . . . 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 4206	. . . . . . . . . . . . . . . . . . 19 |- ( c = a -> <. c , d >. = <. a , d >. )
15	14	breq2d 4452	. . . . . . . . . . . . . . . . . 18 |- ( c = a -> ( x ~Q <. c , d >. <-> x ~Q <. a , d >. ) )
16	15	rexbidv 2966	. . . . . . . . . . . . . . . . 17 |- ( c = a -> ( E. x e. Q. x ~Q <. c , d >. <-> E. x e. Q. x ~Q <. a , d >. ) )
17	16	imbi2d 316	. . . . . . . . . . . . . . . 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 1765	. . . . . . . . . . . . . . . . 17 |- ( d = b -> ( d e. m <-> b e. m ) )
19		opeq2 4207	. . . . . . . . . . . . . . . . . . 19 |- ( d = b -> <. a , d >. = <. a , b >. )
20	19	breq2d 4452	. . . . . . . . . . . . . . . . . 18 |- ( d = b -> ( x ~Q <. a , d >. <-> x ~Q <. a , b >. ) )
21	20	rexbidv 2966	. . . . . . . . . . . . . . . . 17 |- ( d = b -> ( E. x e. Q. x ~Q <. a , d >. <-> E. x e. Q. x ~Q <. a , b >. ) )
22	18, 21	imbi12d 320	. . . . . . . . . . . . . . . 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 3089	. . . . . . . . . . . . . . 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 2888	. . . . . . . . . . . . . 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 2905	. . . . . . . . . . . . . . . . . . 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 421	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) <-> ( <. a , b >. ~Q z /\ ( 2nd ` z ) <N b ) )
27		xp2nd 6805	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( z e. ( N. X. N. ) -> ( 2nd ` z ) e. N. )
28		ltpiord 9254	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 2nd ` z ) e. N. /\ b e. N. ) -> ( ( 2nd ` z ) <N b <-> ( 2nd ` z ) e. b ) )
29	28	ancoms 453	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( b e. N. /\ ( 2nd ` z ) e. N. ) -> ( ( 2nd ` z ) <N b <-> ( 2nd ` z ) e. b ) )
30	27, 29	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( b e. N. /\ z e. ( N. X. N. ) ) -> ( ( 2nd ` z ) <N b <-> ( 2nd ` z ) e. b ) )
31	30	adantll 713	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( a e. N. /\ b e. N. ) /\ z e. ( N. X. N. ) ) -> ( ( 2nd ` z ) <N b <-> ( 2nd ` z ) e. b ) )
32	31	anbi2d 703	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( a e. N. /\ b e. N. ) /\ z e. ( N. X. N. ) ) -> ( ( <. a , b >. ~Q z /\ ( 2nd ` z ) <N b ) <-> ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) ) )
33	26, 32	syl5bb 257	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( a e. N. /\ b e. N. ) /\ z e. ( N. X. N. ) ) -> ( -. ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) <-> ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) ) )
34	33	rexbidva 2963	. . . . . . . . . . . . . . . . . . 19 |- ( ( a e. N. /\ b e. N. ) -> ( E. z e. ( N. X. N. ) -. ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) <-> E. z e. ( N. X. N. ) ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) ) )
35	25, 34	syl5bbr 259	. . . . . . . . . . . . . . . . . 18 |- ( ( a e. N. /\ b e. N. ) -> ( -. A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) <-> E. z e. ( N. X. N. ) ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) ) )
36		xp1st 6804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( z e. ( N. X. N. ) -> ( 1st ` z ) e. N. )
37		elequ2 1767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( m = b -> ( d e. m <-> d e. b ) )
38	37	imbi1d 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( c = ( 1st ` z ) -> <. c , d >. = <. ( 1st ` z ) , d >. )
42	41	breq2d 4452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( c = ( 1st ` z ) -> ( x ~Q <. c , d >. <-> x ~Q <. ( 1st ` z ) , d >. ) )
43	42	rexbidv 2966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( c = ( 1st ` z ) -> ( E. x e. Q. x ~Q <. c , d >. <-> E. x e. Q. x ~Q <. ( 1st ` z ) , d >. ) )
44	43	imbi2d 316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( d = ( 2nd ` z ) -> ( d e. b <-> ( 2nd ` z ) e. b ) )
48		opeq2 4207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( d = ( 2nd ` z ) -> <. ( 1st ` z ) , d >. = <. ( 1st ` z ) , ( 2nd ` z ) >. )
49	48	breq2d 4452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( d = ( 2nd ` z ) -> ( x ~Q <. ( 1st ` z ) , d >. <-> x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
50	49	rexbidv 2966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( A. d e. N. ( d e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , d >. ) -> ( ( 2nd ` z ) e. N. -> ( ( 2nd ` z ) e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) )
53	46, 52	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( A. c e. N. A. d e. N. ( d e. b -> E. x e. Q. x ~Q <. c , d >. ) -> ( ( 1st ` z ) e. N. -> ( ( 2nd ` z ) e. N. -> ( ( 2nd ` z ) e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) ) )
54	40, 53	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) -> ( b e. y -> ( ( 1st ` z ) e. N. -> ( ( 2nd ` z ) e. N. -> ( ( 2nd ` z ) e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) ) ) )
55	54	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) -> ( ( 1st ` z ) e. N. -> ( ( 2nd ` z ) e. N. -> ( ( 2nd ` z ) e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) ) )
56	36, 55	syl5 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) -> ( z e. ( N. X. N. ) -> ( ( 2nd ` z ) e. N. -> ( ( 2nd ` z ) e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) ) )
57	27, 56	mpdi 42	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) -> ( z e. ( N. X. N. ) -> ( ( 2nd ` z ) e. b -> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) )
58	57	3imp 1185	. . . . . . . . . . . . . . . . . . . . . . . . . 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 6811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( z e. ( N. X. N. ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
60	59	breq2d 4452	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z e. ( N. X. N. ) -> ( x ~Q z <-> x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
61	60	rexbidv 2966	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1013	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) /\ z e. ( N. X. N. ) /\ ( 2nd ` z ) e. b ) -> ( E. x e. Q. x ~Q z <-> E. x e. Q. x ~Q <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
63	58, 62	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) /\ z e. ( N. X. N. ) /\ ( 2nd ` z ) e. b ) -> E. x e. Q. x ~Q z )
64		enqer 9288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( <. a , b >. ~Q z /\ x ~Q z ) -> x ~Q z )
67		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( <. a , b >. ~Q z /\ x ~Q z ) -> <. a , b >. ~Q z )
68	65, 66, 67	ertr4d 7320	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( <. a , b >. ~Q z /\ x ~Q z ) -> x ~Q <. a , b >. )
69	68	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( <. a , b >. ~Q z -> ( x ~Q z -> x ~Q <. a , b >. ) )
70	69	reximdv 2930	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( <. a , b >. ~Q z -> ( E. x e. Q. x ~Q z -> E. x e. Q. x ~Q <. a , b >. ) )
71	63, 70	syl5com 30	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) /\ z e. ( N. X. N. ) /\ ( 2nd ` z ) e. b ) -> ( <. a , b >. ~Q z -> E. x e. Q. x ~Q <. a , b >. ) )
72	71	3expia 1193	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) /\ z e. ( N. X. N. ) ) -> ( ( 2nd ` z ) e. b -> ( <. a , b >. ~Q z -> E. x e. Q. x ~Q <. a , b >. ) ) )
73	72	com23 78	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) /\ b e. y ) /\ z e. ( N. X. N. ) ) -> ( <. a , b >. ~Q z -> ( ( 2nd ` z ) e. b -> E. x e. Q. x ~Q <. a , b >. ) ) )
74	73	impd 431	. . . . . . . . . . . . . . . . . . . . 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 2948	. . . . . . . . . . . . . . . . . . . 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 434	. . . . . . . . . . . . . . . . . . 19 |- ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) -> ( b e. y -> ( E. z e. ( N. X. N. ) ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) -> E. x e. Q. x ~Q <. a , b >. ) ) )
77	76	com3r 79	. . . . . . . . . . . . . . . . . 18 |- ( E. z e. ( N. X. N. ) ( <. a , b >. ~Q z /\ ( 2nd ` z ) e. b ) -> ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
78	35, 77	syl6bi 228	. . . . . . . . . . . . . . . . 17 |- ( ( a e. N. /\ b e. N. ) -> ( -. A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) -> ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) ) )
79	78	com13 80	. . . . . . . . . . . . . . . 16 |- ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) -> ( -. A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) -> ( ( a e. N. /\ b e. N. ) -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) ) )
80		mulcompi 9263	. . . . . . . . . . . . . . . . . . . 20 |- ( a .N b ) = ( b .N a )
81		enqbreq 9286	. . . . . . . . . . . . . . . . . . . . 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 645	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. N. /\ b e. N. ) -> ( <. a , b >. ~Q <. a , b >. <-> ( a .N b ) = ( b .N a ) ) )
83	80, 82	mpbiri 233	. . . . . . . . . . . . . . . . . . 19 |- ( ( a e. N. /\ b e. N. ) -> <. a , b >. ~Q <. a , b >. )
84		opelxpi 5023	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. N. /\ b e. N. ) -> <. a , b >. e. ( N. X. N. ) )
85		breq1 4443	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = <. a , b >. -> ( y ~Q z <-> <. a , b >. ~Q z ) )
86		vex 3109	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- a e. _V
87	86, 5	op2ndd 6785	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y = <. a , b >. -> ( 2nd ` y ) = b )
88	87	breq2d 4452	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = <. a , b >. -> ( ( 2nd ` z ) <N ( 2nd ` y ) <-> ( 2nd ` z ) <N b ) )
89	88	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = <. a , b >. -> ( -. ( 2nd ` z ) <N ( 2nd ` y ) <-> -. ( 2nd ` z ) <N b ) )
90	85, 89	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y = <. a , b >. -> ( ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) <-> ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) ) )
91	90	ralbidv 2896	. . . . . . . . . . . . . . . . . . . . . 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 9279	. . . . . . . . . . . . . . . . . . . . . 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 3256	. . . . . . . . . . . . . . . . . . . . 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 625	. . . . . . . . . . . . . . . . . . . 20 |- ( <. a , b >. e. ( N. X. N. ) -> ( A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) -> <. a , b >. e. Q. ) )
95	84, 94	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( a e. N. /\ b e. N. ) -> ( A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) -> <. a , b >. e. Q. ) )
96		breq1 4443	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = <. a , b >. -> ( x ~Q <. a , b >. <-> <. a , b >. ~Q <. a , b >. ) )
97	96	rspcev 3207	. . . . . . . . . . . . . . . . . . . 20 |- ( ( <. a , b >. e. Q. /\ <. a , b >. ~Q <. a , b >. ) -> E. x e. Q. x ~Q <. a , b >. )
98	97	expcom 435	. . . . . . . . . . . . . . . . . . 19 |- ( <. a , b >. ~Q <. a , b >. -> ( <. a , b >. e. Q. -> E. x e. Q. x ~Q <. a , b >. ) )
99	83, 95, 98	sylsyld 56	. . . . . . . . . . . . . . . . . 18 |- ( ( a e. N. /\ b e. N. ) -> ( A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) -> E. x e. Q. x ~Q <. a , b >. ) )
100	99	com12 31	. . . . . . . . . . . . . . . . 17 |- ( A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) -> ( ( a e. N. /\ b e. N. ) -> E. x e. Q. x ~Q <. a , b >. ) )
101	100	a1dd 46	. . . . . . . . . . . . . . . 16 |- ( A. z e. ( N. X. N. ) ( <. a , b >. ~Q z -> -. ( 2nd ` z ) <N b ) -> ( ( a e. N. /\ b e. N. ) -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
102	79, 101	pm2.61d2 160	. . . . . . . . . . . . . . 15 |- ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) -> ( ( a e. N. /\ b e. N. ) -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
103	102	ralrimivv 2877	. . . . . . . . . . . . . 14 |- ( A. m e. y A. c e. N. A. d e. N. ( d e. m -> E. x e. Q. x ~Q <. c , d >. ) -> A. a e. N. A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) )
104	24, 103	sylbir 213	. . . . . . . . . . . . 13 |- ( A. m e. y A. a e. N. A. b e. N. ( b e. m -> E. x e. Q. x ~Q <. a , b >. ) -> A. a e. N. A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) )
105	104	a1i 11	. . . . . . . . . . . 12 |- ( y e. On -> ( A. m e. y A. a e. N. A. b e. N. ( b e. m -> E. x e. Q. x ~Q <. a , b >. ) -> A. a e. N. A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
106	13, 105	tfis2 6662	. . . . . . . . . . 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 2823	. . . . . . . . . . 11 |- ( A. a e. N. A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) -> ( a e. N. -> A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
108	106, 107	syl 16	. . . . . . . . . 10 |- ( y e. On -> ( a e. N. -> A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
109		rsp 2823	. . . . . . . . . 10 |- ( A. b e. N. ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) -> ( b e. N. -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
110	108, 109	syl6 33	. . . . . . . . 9 |- ( y e. On -> ( a e. N. -> ( b e. N. -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) ) )
111	110	impd 431	. . . . . . . 8 |- ( y e. On -> ( ( a e. N. /\ b e. N. ) -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
112	111	com12 31	. . . . . . 7 |- ( ( a e. N. /\ b e. N. ) -> ( y e. On -> ( b e. y -> E. x e. Q. x ~Q <. a , b >. ) ) )
113	112	rexlimdv 2946	. . . . . 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 4444	. . . . . 6 |- ( A = <. a , b >. -> ( x ~Q A <-> x ~Q <. a , b >. ) )
116	115	rexbidv 2966	. . . . 5 |- ( A = <. a , b >. -> ( E. x e. Q. x ~Q A <-> E. x e. Q. x ~Q <. a , b >. ) )
117	114, 116	syl5ibrcom 222	. . . 4 |- ( ( a e. N. /\ b e. N. ) -> ( A = <. a , b >. -> E. x e. Q. x ~Q A ) )
118	117	rexlimivv 2953	. . 3 |- ( E. a e. N. E. b e. N. A = <. a , b >. -> E. x e. Q. x ~Q A )
119	1, 118	sylbi 195	. 2 |- ( A e. ( N. X. N. ) -> E. x e. Q. x ~Q A )
120		breq2 4444	. . . . . 6 |- ( a = A -> ( x ~Q a <-> x ~Q A ) )
121		breq2 4444	. . . . . 6 |- ( a = A -> ( y ~Q a <-> y ~Q A ) )
122	120, 121	anbi12d 710	. . . . 5 |- ( a = A -> ( ( x ~Q a /\ y ~Q a ) <-> ( x ~Q A /\ y ~Q A ) ) )
123	122	imbi1d 317	. . . 4 |- ( a = A -> ( ( ( x ~Q a /\ y ~Q a ) -> x = y ) <-> ( ( x ~Q A /\ y ~Q A ) -> x = y ) ) )
124	123	2ralbidv 2901	. . 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 457	. . . . . 6 |- ( ( x ~Q a /\ y ~Q a ) -> x ~Q a )
127		simpr 461	. . . . . 6 |- ( ( x ~Q a /\ y ~Q a ) -> y ~Q a )
128	125, 126, 127	ertr4d 7320	. . . . 5 |- ( ( x ~Q a /\ y ~Q a ) -> x ~Q y )
129		mulcompi 9263	. . . . . . . . . . 11 |- ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` x ) )
130		elpqn 9292	. . . . . . . . . . . . . . 15 |- ( y e. Q. -> y e. ( N. X. N. ) )
131		breq1 4443	. . . . . . . . . . . . . . . . . . 19 |- ( y = x -> ( y ~Q z <-> x ~Q z ) )
132		fveq2 5857	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = x -> ( 2nd ` y ) = ( 2nd ` x ) )
133	132	breq2d 4452	. . . . . . . . . . . . . . . . . . . 20 |- ( y = x -> ( ( 2nd ` z ) <N ( 2nd ` y ) <-> ( 2nd ` z ) <N ( 2nd ` x ) ) )
134	133	notbid 294	. . . . . . . . . . . . . . . . . . 19 |- ( y = x -> ( -. ( 2nd ` z ) <N ( 2nd ` y ) <-> -. ( 2nd ` z ) <N ( 2nd ` x ) ) )
135	131, 134	imbi12d 320	. . . . . . . . . . . . . . . . . 18 |- ( y = x -> ( ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) <-> ( x ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` x ) ) ) )
136	135	ralbidv 2896	. . . . . . . . . . . . . . . . 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 3256	. . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . 15 |- ( x e. Q. -> A. z e. ( N. X. N. ) ( x ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` x ) ) )
139		breq2 4444	. . . . . . . . . . . . . . . . 17 |- ( z = y -> ( x ~Q z <-> x ~Q y ) )
140		fveq2 5857	. . . . . . . . . . . . . . . . . . 19 |- ( z = y -> ( 2nd ` z ) = ( 2nd ` y ) )
141	140	breq1d 4450	. . . . . . . . . . . . . . . . . 18 |- ( z = y -> ( ( 2nd ` z ) <N ( 2nd ` x ) <-> ( 2nd ` y ) <N ( 2nd ` x ) ) )
142	141	notbid 294	. . . . . . . . . . . . . . . . 17 |- ( z = y -> ( -. ( 2nd ` z ) <N ( 2nd ` x ) <-> -. ( 2nd ` y ) <N ( 2nd ` x ) ) )
143	139, 142	imbi12d 320	. . . . . . . . . . . . . . . 16 |- ( z = y -> ( ( x ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` x ) ) <-> ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) ) ) )
144	143	rspcva 3205	. . . . . . . . . . . . . . 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 478	. . . . . . . . . . . . . 14 |- ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) ) )
146	145	imp 429	. . . . . . . . . . . . 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 7313	. . . . . . . . . . . . . . . . 17 |- ( x ~Q y -> y ~Q x )
150		elpqn 9292	. . . . . . . . . . . . . . . . . 18 |- ( x e. Q. -> x e. ( N. X. N. ) )
151	92	rabeq2i 3103	. . . . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . . . 18 |- ( y e. Q. -> A. z e. ( N. X. N. ) ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) )
153		breq2 4444	. . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( y ~Q z <-> y ~Q x ) )
154		fveq2 5857	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z = x -> ( 2nd ` z ) = ( 2nd ` x ) )
155	154	breq1d 4450	. . . . . . . . . . . . . . . . . . . . 21 |- ( z = x -> ( ( 2nd ` z ) <N ( 2nd ` y ) <-> ( 2nd ` x ) <N ( 2nd ` y ) ) )
156	155	notbid 294	. . . . . . . . . . . . . . . . . . . 20 |- ( z = x -> ( -. ( 2nd ` z ) <N ( 2nd ` y ) <-> -. ( 2nd ` x ) <N ( 2nd ` y ) ) )
157	153, 156	imbi12d 320	. . . . . . . . . . . . . . . . . . 19 |- ( z = x -> ( ( y ~Q z -> -. ( 2nd ` z ) <N ( 2nd ` y ) ) <-> ( y ~Q x -> -. ( 2nd ` x ) <N ( 2nd ` y ) ) ) )
158	157	rspcva 3205	. . . . . . . . . . . . . . . . . 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 477	. . . . . . . . . . . . . . . . 17 |- ( ( x e. Q. /\ y e. Q. ) -> ( y ~Q x -> -. ( 2nd ` x ) <N ( 2nd ` y ) ) )
160	149, 159	syl5 32	. . . . . . . . . . . . . . . 16 |- ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y -> -. ( 2nd ` x ) <N ( 2nd ` y ) ) )
161	160	imp 429	. . . . . . . . . . . . . . 15 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> -. ( 2nd ` x ) <N ( 2nd ` y ) )
162		xp2nd 6805	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( N. X. N. ) -> ( 2nd ` x ) e. N. )
163	150, 162	syl 16	. . . . . . . . . . . . . . . . 17 |- ( x e. Q. -> ( 2nd ` x ) e. N. )
164	163	ad2antrr 725	. . . . . . . . . . . . . . . 16 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 2nd ` x ) e. N. )
165		xp2nd 6805	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( N. X. N. ) -> ( 2nd ` y ) e. N. )
166	130, 165	syl 16	. . . . . . . . . . . . . . . . 17 |- ( y e. Q. -> ( 2nd ` y ) e. N. )
167	166	ad2antlr 726	. . . . . . . . . . . . . . . 16 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 2nd ` y ) e. N. )
168		ltsopi 9255	. . . . . . . . . . . . . . . . . . 19 |- <N Or N.
169		sotric 4819	. . . . . . . . . . . . . . . . . . 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 670	. . . . . . . . . . . . . . . . . 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 294	. . . . . . . . . . . . . . . . 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 291	. . . . . . . . . . . . . . . . 17 |- ( ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) <-> -. -. ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) )
173	171, 172	syl6bbr 263	. . . . . . . . . . . . . . . 16 |- ( ( ( 2nd ` x ) e. N. /\ ( 2nd ` y ) e. N. ) -> ( -. ( 2nd ` x ) <N ( 2nd ` y ) <-> ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) ) )
174	164, 167, 173	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( -. ( 2nd ` x ) <N ( 2nd ` y ) <-> ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) ) )
175	161, 174	mpbid 210	. . . . . . . . . . . . . 14 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 2nd ` x ) = ( 2nd ` y ) \/ ( 2nd ` y ) <N ( 2nd ` x ) ) )
176	175	ord 377	. . . . . . . . . . . . 13 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( -. ( 2nd ` x ) = ( 2nd ` y ) -> ( 2nd ` y ) <N ( 2nd ` x ) ) )
177	146, 176	mt3d 125	. . . . . . . . . . . 12 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 2nd ` x ) = ( 2nd ` y ) )
178	177	oveq2d 6291	. . . . . . . . . . 11 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 1st ` x ) .N ( 2nd ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` y ) ) )
179	129, 178	syl5eq 2513	. . . . . . . . . 10 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` y ) ) )
180		1st2nd2 6811	. . . . . . . . . . . . . 14 |- ( x e. ( N. X. N. ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
181		1st2nd2 6811	. . . . . . . . . . . . . 14 |- ( y e. ( N. X. N. ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
182	180, 181	breqan12d 4455	. . . . . . . . . . . . 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 6804	. . . . . . . . . . . . . . 15 |- ( x e. ( N. X. N. ) -> ( 1st ` x ) e. N. )
184	183, 162	jca 532	. . . . . . . . . . . . . 14 |- ( x e. ( N. X. N. ) -> ( ( 1st ` x ) e. N. /\ ( 2nd ` x ) e. N. ) )
185		xp1st 6804	. . . . . . . . . . . . . . 15 |- ( y e. ( N. X. N. ) -> ( 1st ` y ) e. N. )
186	185, 165	jca 532	. . . . . . . . . . . . . 14 |- ( y e. ( N. X. N. ) -> ( ( 1st ` y ) e. N. /\ ( 2nd ` y ) e. N. ) )
187		enqbreq 9286	. . . . . . . . . . . . . 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 477	. . . . . . . . . . . . 13 |- ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( <. ( 1st ` x ) , ( 2nd ` x ) >. ~Q <. ( 1st ` y ) , ( 2nd ` y ) >. <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) ) )
189	182, 188	bitrd 253	. . . . . . . . . . . 12 |- ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( x ~Q y <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) ) )
190	150, 130, 189	syl2an 477	. . . . . . . . . . 11 |- ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) ) )
191	190	biimpa 484	. . . . . . . . . 10 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) )
192	179, 191	eqtrd 2501	. . . . . . . . 9 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) )
193	150	ad2antrr 725	. . . . . . . . . 10 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> x e. ( N. X. N. ) )
194		mulcanpi 9267	. . . . . . . . . . 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 661	. . . . . . . . . 10 |- ( x e. ( N. X. N. ) -> ( ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) <-> ( 1st ` x ) = ( 1st ` y ) ) )
196	193, 195	syl 16	. . . . . . . . 9 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 2nd ` x ) .N ( 1st ` y ) ) <-> ( 1st ` x ) = ( 1st ` y ) ) )
197	192, 196	mpbid 210	. . . . . . . 8 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> ( 1st ` x ) = ( 1st ` y ) )
198	197, 177	opeq12d 4214	. . . . . . 7 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. = <. ( 1st ` y ) , ( 2nd ` y ) >. )
199	193, 180	syl 16	. . . . . . 7 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
200	130	ad2antlr 726	. . . . . . . 8 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> y e. ( N. X. N. ) )
201	200, 181	syl 16	. . . . . . 7 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
202	198, 199, 201	3eqtr4d 2511	. . . . . 6 |- ( ( ( x e. Q. /\ y e. Q. ) /\ x ~Q y ) -> x = y )
203	202	ex 434	. . . . 5 |- ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y -> x = y ) )
204	128, 203	syl5 32	. . . 4 |- ( ( x e. Q. /\ y e. Q. ) -> ( ( x ~Q a /\ y ~Q a ) -> x = y ) )
205	204	rgen2a 2884	. . 3 |- A. x e. Q. A. y e. Q. ( ( x ~Q a /\ y ~Q a ) -> x = y )
206	124, 205	vtoclg 3164	. 2 |- ( A e. ( N. X. N. ) -> A. x e. Q. A. y e. Q. ( ( x ~Q A /\ y ~Q A ) -> x = y ) )
207		breq1 4443	. . 3 |- ( x = y -> ( x ~Q A <-> y ~Q A ) )
208	207	reu4 3290	. 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 664	1 |- ( A e. ( N. X. N. ) -> E! x e. Q. x ~Q A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 968   = wceq 1374   e. wcel 1762   A.wral 2807   E.wrex 2808   E!wreu 2809   <.cop 4026   class class class wbr 4440   Or wor 4792   Oncon0 4871   suc csuc 4873   X. cxp 4990   ` cfv 5579  (class class class)co 6275   1stc1st 6772   2ndc2nd 6773   Er wer 7298   N.cnpi 9211   .N cmi 9213   <N clti 9214   ~Q ceq 9218   Q.cnq 9219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-pss 3485  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-tp 4025  df-op 4027  df-uni 4239  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-tr 4534  df-eprel 4784  df-id 4788  df-po 4793  df-so 4794  df-fr 4831  df-we 4833  df-ord 4874  df-on 4875  df-lim 4876  df-suc 4877  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-om 6672  df-1st 6774  df-2nd 6775  df-recs 7032  df-rdg 7066  df-oadd 7124  df-omul 7125  df-er 7301  df-ni 9239  df-mi 9241  df-lti 9242  df-enq 9278  df-nq 9279

This theorem is referenced by:  nqerf  9297  enqeq  9301