nqereu

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

		Ref	Expression
	Assertion	nqereu	$⊢ A \in (𝑵 \times 𝑵) \to \exists! x \in 𝑸 x ~_{𝑸} A$

Proof

Step	Hyp	Ref	Expression
1		elxp2	$⊢ A \in (𝑵 \times 𝑵) \leftrightarrow \exists a \in 𝑵 \exists b \in 𝑵 A = ⟨a, b⟩$
2		pion	$⊢ b \in 𝑵 \to b \in On$
3		onsuc	$⊢ b \in On \to suc b \in On$
4	2 3	syl	$⊢ b \in 𝑵 \to suc b \in On$
5		vex	$⊢ b \in V$
6	5	sucid	$⊢ b \in suc b$
7		eleq2	$⊢ y = suc b \to (b \in y \leftrightarrow b \in suc b)$
8	7	rspcev	$⊢ (suc b \in On \land b \in suc b) \to \exists y \in On b \in y$
9	4 6 8	sylancl	$⊢ b \in 𝑵 \to \exists y \in On b \in y$
10	9	adantl	$⊢ (a \in 𝑵 \land b \in 𝑵) \to \exists y \in On b \in y$
11		elequ2	$⊢ y = m \to (b \in y \leftrightarrow b \in m)$
12	11	imbi1d	$⊢ y = m \to ((b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩) \leftrightarrow (b \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩))$
13	12	2ralbidv	$⊢ y = m \to (\forall a \in 𝑵 \forall b \in 𝑵 (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩) \leftrightarrow \forall a \in 𝑵 \forall b \in 𝑵 (b \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩))$
14		opeq1	$⊢ c = a \to ⟨c, d⟩ = ⟨a, d⟩$
15	14	breq2d	$⊢ c = a \to (x ~_{𝑸} ⟨c, d⟩ \leftrightarrow x ~_{𝑸} ⟨a, d⟩)$
16	15	rexbidv	$⊢ c = a \to (\exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩ \leftrightarrow \exists x \in 𝑸 x ~_{𝑸} ⟨a, d⟩)$
17	16	imbi2d	$⊢ c = a \to ((d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \leftrightarrow (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, d⟩))$
18		elequ1	$⊢ d = b \to (d \in m \leftrightarrow b \in m)$
19		opeq2	$⊢ d = b \to ⟨a, d⟩ = ⟨a, b⟩$
20	19	breq2d	$⊢ d = b \to (x ~_{𝑸} ⟨a, d⟩ \leftrightarrow x ~_{𝑸} ⟨a, b⟩)$
21	20	rexbidv	$⊢ d = b \to (\exists x \in 𝑸 x ~_{𝑸} ⟨a, d⟩ \leftrightarrow \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)$
22	18 21	imbi12d	$⊢ d = b \to ((d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, d⟩) \leftrightarrow (b \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩))$
23	17 22	cbvral2vw	$⊢ \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \leftrightarrow \forall a \in 𝑵 \forall b \in 𝑵 (b \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)$
24	23	ralbii	$⊢ \forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \leftrightarrow \forall m \in y \forall a \in 𝑵 \forall b \in 𝑵 (b \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)$
25		rexnal	$⊢ \exists z \in (𝑵 \times 𝑵) \neg (⟨a, b⟩ ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} b) \leftrightarrow \neg \forall z \in (𝑵 \times 𝑵) (⟨a, b⟩ ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} b)$
26		pm4.63	$⊢ \neg (⟨a, b⟩ ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} b) \leftrightarrow (⟨a, b⟩ ~_{𝑸} z \land 2^{nd} (z) <_{𝑵} b)$
27		xp2nd	$⊢ z \in (𝑵 \times 𝑵) \to 2^{nd} (z) \in 𝑵$
28		ltpiord	$⊢ (2^{nd} (z) \in 𝑵 \land b \in 𝑵) \to (2^{nd} (z) <_{𝑵} b \leftrightarrow 2^{nd} (z) \in b)$
29	28	ancoms	$⊢ (b \in 𝑵 \land 2^{nd} (z) \in 𝑵) \to (2^{nd} (z) <_{𝑵} b \leftrightarrow 2^{nd} (z) \in b)$
30	27 29	sylan2	$⊢ (b \in 𝑵 \land z \in (𝑵 \times 𝑵)) \to (2^{nd} (z) <_{𝑵} b \leftrightarrow 2^{nd} (z) \in b)$
31	30	adantll	$⊢ ((a \in 𝑵 \land b \in 𝑵) \land z \in (𝑵 \times 𝑵)) \to (2^{nd} (z) <_{𝑵} b \leftrightarrow 2^{nd} (z) \in b)$
32	31	anbi2d	$⊢ ((a \in 𝑵 \land b \in 𝑵) \land z \in (𝑵 \times 𝑵)) \to ((⟨a, b⟩ ~_{𝑸} z \land 2^{nd} (z) <_{𝑵} b) \leftrightarrow (⟨a, b⟩ ~_{𝑸} z \land 2^{nd} (z) \in b))$
33	26 32	bitrid	$⊢ ((a \in 𝑵 \land b \in 𝑵) \land z \in (𝑵 \times 𝑵)) \to (\neg (⟨a, b⟩ ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} b) \leftrightarrow (⟨a, b⟩ ~_{𝑸} z \land 2^{nd} (z) \in b))$
34	33	rexbidva	$⊢ (a \in 𝑵 \land b \in 𝑵) \to (\exists z \in (𝑵 \times 𝑵) \neg (⟨a, b⟩ ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} b) \leftrightarrow \exists z \in (𝑵 \times 𝑵) (⟨a, b⟩ ~_{𝑸} z \land 2^{nd} (z) \in b))$
35	25 34	bitr3id	$⊢ (a \in 𝑵 \land b \in 𝑵) \to (\neg \forall z \in (𝑵 \times 𝑵) (⟨a, b⟩ ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} b) \leftrightarrow \exists z \in (𝑵 \times 𝑵) (⟨a, b⟩ ~_{𝑸} z \land 2^{nd} (z) \in b))$
36		xp1st	$⊢ z \in (𝑵 \times 𝑵) \to 1^{st} (z) \in 𝑵$
37		elequ2	$⊢ m = b \to (d \in m \leftrightarrow d \in b)$
38	37	imbi1d	$⊢ m = b \to ((d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \leftrightarrow (d \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩))$
39	38	2ralbidv	$⊢ m = b \to (\forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \leftrightarrow \forall c \in 𝑵 \forall d \in 𝑵 (d \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩))$
40	39	rspccv	$⊢ \forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \to (b \in y \to \forall c \in 𝑵 \forall d \in 𝑵 (d \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩))$
41		opeq1	$⊢ c = 1^{st} (z) \to ⟨c, d⟩ = ⟨1^{st} (z), d⟩$
42	41	breq2d	$⊢ c = 1^{st} (z) \to (x ~_{𝑸} ⟨c, d⟩ \leftrightarrow x ~_{𝑸} ⟨1^{st} (z), d⟩)$
43	42	rexbidv	$⊢ c = 1^{st} (z) \to (\exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩ \leftrightarrow \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), d⟩)$
44	43	imbi2d	$⊢ c = 1^{st} (z) \to ((d \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \leftrightarrow (d \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), d⟩))$
45	44	ralbidv	$⊢ c = 1^{st} (z) \to (\forall d \in 𝑵 (d \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \leftrightarrow \forall d \in 𝑵 (d \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), d⟩))$
46	45	rspccv	$⊢ \forall c \in 𝑵 \forall d \in 𝑵 (d \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \to (1^{st} (z) \in 𝑵 \to \forall d \in 𝑵 (d \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), d⟩))$
47		eleq1	$⊢ d = 2^{nd} (z) \to (d \in b \leftrightarrow 2^{nd} (z) \in b)$
48		opeq2	$⊢ d = 2^{nd} (z) \to ⟨1^{st} (z), d⟩ = ⟨1^{st} (z), 2^{nd} (z)⟩$
49	48	breq2d	$⊢ d = 2^{nd} (z) \to (x ~_{𝑸} ⟨1^{st} (z), d⟩ \leftrightarrow x ~_{𝑸} ⟨1^{st} (z), 2^{nd} (z)⟩)$
50	49	rexbidv	$⊢ d = 2^{nd} (z) \to (\exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), d⟩ \leftrightarrow \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), 2^{nd} (z)⟩)$
51	47 50	imbi12d	$⊢ d = 2^{nd} (z) \to ((d \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), d⟩) \leftrightarrow (2^{nd} (z) \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), 2^{nd} (z)⟩))$
52	51	rspccv	$⊢ \forall d \in 𝑵 (d \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), d⟩) \to (2^{nd} (z) \in 𝑵 \to (2^{nd} (z) \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), 2^{nd} (z)⟩))$
53	46 52	syl6	$⊢ \forall c \in 𝑵 \forall d \in 𝑵 (d \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \to (1^{st} (z) \in 𝑵 \to (2^{nd} (z) \in 𝑵 \to (2^{nd} (z) \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), 2^{nd} (z)⟩)))$
54	40 53	syl6	$⊢ \forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \to (b \in y \to (1^{st} (z) \in 𝑵 \to (2^{nd} (z) \in 𝑵 \to (2^{nd} (z) \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), 2^{nd} (z)⟩))))$
55	54	imp	$⊢ (\forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \land b \in y) \to (1^{st} (z) \in 𝑵 \to (2^{nd} (z) \in 𝑵 \to (2^{nd} (z) \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), 2^{nd} (z)⟩)))$
56	36 55	syl5	$⊢ (\forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \land b \in y) \to (z \in (𝑵 \times 𝑵) \to (2^{nd} (z) \in 𝑵 \to (2^{nd} (z) \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), 2^{nd} (z)⟩)))$
57	27 56	mpdi	$⊢ (\forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \land b \in y) \to (z \in (𝑵 \times 𝑵) \to (2^{nd} (z) \in b \to \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), 2^{nd} (z)⟩))$
58	57	3imp	$⊢ ((\forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \land b \in y) \land z \in (𝑵 \times 𝑵) \land 2^{nd} (z) \in b) \to \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), 2^{nd} (z)⟩$
59		1st2nd2	$⊢ z \in (𝑵 \times 𝑵) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
60	59	breq2d	$⊢ z \in (𝑵 \times 𝑵) \to (x ~_{𝑸} z \leftrightarrow x ~_{𝑸} ⟨1^{st} (z), 2^{nd} (z)⟩)$
61	60	rexbidv	$⊢ z \in (𝑵 \times 𝑵) \to (\exists x \in 𝑸 x ~_{𝑸} z \leftrightarrow \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), 2^{nd} (z)⟩)$
62	61	3ad2ant2	$⊢ ((\forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \land b \in y) \land z \in (𝑵 \times 𝑵) \land 2^{nd} (z) \in b) \to (\exists x \in 𝑸 x ~_{𝑸} z \leftrightarrow \exists x \in 𝑸 x ~_{𝑸} ⟨1^{st} (z), 2^{nd} (z)⟩)$
63	58 62	mpbird	$⊢ ((\forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \land b \in y) \land z \in (𝑵 \times 𝑵) \land 2^{nd} (z) \in b) \to \exists x \in 𝑸 x ~_{𝑸} z$
64		enqer	$⊢ ~_{𝑸} Er (𝑵 \times 𝑵)$
65	64	a1i	$⊢ (⟨a, b⟩ ~_{𝑸} z \land x ~_{𝑸} z) \to ~_{𝑸} Er (𝑵 \times 𝑵)$
66		simpr	$⊢ (⟨a, b⟩ ~_{𝑸} z \land x ~_{𝑸} z) \to x ~_{𝑸} z$
67		simpl	$⊢ (⟨a, b⟩ ~_{𝑸} z \land x ~_{𝑸} z) \to ⟨a, b⟩ ~_{𝑸} z$
68	65 66 67	ertr4d	$⊢ (⟨a, b⟩ ~_{𝑸} z \land x ~_{𝑸} z) \to x ~_{𝑸} ⟨a, b⟩$
69	68	ex	$⊢ ⟨a, b⟩ ~_{𝑸} z \to (x ~_{𝑸} z \to x ~_{𝑸} ⟨a, b⟩)$
70	69	reximdv	$⊢ ⟨a, b⟩ ~_{𝑸} z \to (\exists x \in 𝑸 x ~_{𝑸} z \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)$
71	63 70	syl5com	$⊢ ((\forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \land b \in y) \land z \in (𝑵 \times 𝑵) \land 2^{nd} (z) \in b) \to (⟨a, b⟩ ~_{𝑸} z \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)$
72	71	3expia	$⊢ ((\forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \land b \in y) \land z \in (𝑵 \times 𝑵)) \to (2^{nd} (z) \in b \to (⟨a, b⟩ ~_{𝑸} z \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩))$
73	72	impcomd	$⊢ ((\forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \land b \in y) \land z \in (𝑵 \times 𝑵)) \to ((⟨a, b⟩ ~_{𝑸} z \land 2^{nd} (z) \in b) \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)$
74	73	rexlimdva	$⊢ (\forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \land b \in y) \to (\exists z \in (𝑵 \times 𝑵) (⟨a, b⟩ ~_{𝑸} z \land 2^{nd} (z) \in b) \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)$
75	74	ex	$⊢ \forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \to (b \in y \to (\exists z \in (𝑵 \times 𝑵) (⟨a, b⟩ ~_{𝑸} z \land 2^{nd} (z) \in b) \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩))$
76	75	com3r	$⊢ \exists z \in (𝑵 \times 𝑵) (⟨a, b⟩ ~_{𝑸} z \land 2^{nd} (z) \in b) \to (\forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \to (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩))$
77	35 76	biimtrdi	$⊢ (a \in 𝑵 \land b \in 𝑵) \to (\neg \forall z \in (𝑵 \times 𝑵) (⟨a, b⟩ ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} b) \to (\forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \to (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)))$
78	77	com13	$⊢ \forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \to (\neg \forall z \in (𝑵 \times 𝑵) (⟨a, b⟩ ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} b) \to ((a \in 𝑵 \land b \in 𝑵) \to (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)))$
79		mulcompi	$⊢ a \cdot_{𝑵} b = b \cdot_{𝑵} a$
80		enqbreq	$⊢ ((a \in 𝑵 \land b \in 𝑵) \land (a \in 𝑵 \land b \in 𝑵)) \to (⟨a, b⟩ ~_{𝑸} ⟨a, b⟩ \leftrightarrow a \cdot_{𝑵} b = b \cdot_{𝑵} a)$
81	80	anidms	$⊢ (a \in 𝑵 \land b \in 𝑵) \to (⟨a, b⟩ ~_{𝑸} ⟨a, b⟩ \leftrightarrow a \cdot_{𝑵} b = b \cdot_{𝑵} a)$
82	79 81	mpbiri	$⊢ (a \in 𝑵 \land b \in 𝑵) \to ⟨a, b⟩ ~_{𝑸} ⟨a, b⟩$
83		opelxpi	$⊢ (a \in 𝑵 \land b \in 𝑵) \to ⟨a, b⟩ \in (𝑵 \times 𝑵)$
84		breq1	$⊢ y = ⟨a, b⟩ \to (y ~_{𝑸} z \leftrightarrow ⟨a, b⟩ ~_{𝑸} z)$
85		vex	$⊢ a \in V$
86	85 5	op2ndd	$⊢ y = ⟨a, b⟩ \to 2^{nd} (y) = b$
87	86	breq2d	$⊢ y = ⟨a, b⟩ \to (2^{nd} (z) <_{𝑵} 2^{nd} (y) \leftrightarrow 2^{nd} (z) <_{𝑵} b)$
88	87	notbid	$⊢ y = ⟨a, b⟩ \to (\neg 2^{nd} (z) <_{𝑵} 2^{nd} (y) \leftrightarrow \neg 2^{nd} (z) <_{𝑵} b)$
89	84 88	imbi12d	$⊢ y = ⟨a, b⟩ \to ((y ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} 2^{nd} (y)) \leftrightarrow (⟨a, b⟩ ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} b))$
90	89	ralbidv	$⊢ y = ⟨a, b⟩ \to (\forall z \in (𝑵 \times 𝑵) (y ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} 2^{nd} (y)) \leftrightarrow \forall z \in (𝑵 \times 𝑵) (⟨a, b⟩ ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} b))$
91		df-nq	$⊢ 𝑸 = \{y \in (𝑵 \times 𝑵) \| \forall z \in (𝑵 \times 𝑵) (y ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} 2^{nd} (y))\}$
92	90 91	elrab2	$⊢ ⟨a, b⟩ \in 𝑸 \leftrightarrow (⟨a, b⟩ \in (𝑵 \times 𝑵) \land \forall z \in (𝑵 \times 𝑵) (⟨a, b⟩ ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} b))$
93	92	simplbi2	$⊢ ⟨a, b⟩ \in (𝑵 \times 𝑵) \to (\forall z \in (𝑵 \times 𝑵) (⟨a, b⟩ ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} b) \to ⟨a, b⟩ \in 𝑸)$
94	83 93	syl	$⊢ (a \in 𝑵 \land b \in 𝑵) \to (\forall z \in (𝑵 \times 𝑵) (⟨a, b⟩ ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} b) \to ⟨a, b⟩ \in 𝑸)$
95		breq1	$⊢ x = ⟨a, b⟩ \to (x ~_{𝑸} ⟨a, b⟩ \leftrightarrow ⟨a, b⟩ ~_{𝑸} ⟨a, b⟩)$
96	95	rspcev	$⊢ (⟨a, b⟩ \in 𝑸 \land ⟨a, b⟩ ~_{𝑸} ⟨a, b⟩) \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩$
97	96	expcom	$⊢ ⟨a, b⟩ ~_{𝑸} ⟨a, b⟩ \to (⟨a, b⟩ \in 𝑸 \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)$
98	82 94 97	sylsyld	$⊢ (a \in 𝑵 \land b \in 𝑵) \to (\forall z \in (𝑵 \times 𝑵) (⟨a, b⟩ ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} b) \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)$
99	98	com12	$⊢ \forall z \in (𝑵 \times 𝑵) (⟨a, b⟩ ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} b) \to ((a \in 𝑵 \land b \in 𝑵) \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)$
100	99	a1dd	$⊢ \forall z \in (𝑵 \times 𝑵) (⟨a, b⟩ ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} b) \to ((a \in 𝑵 \land b \in 𝑵) \to (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩))$
101	78 100	pm2.61d2	$⊢ \forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \to ((a \in 𝑵 \land b \in 𝑵) \to (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩))$
102	101	ralrimivv	$⊢ \forall m \in y \forall c \in 𝑵 \forall d \in 𝑵 (d \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨c, d⟩) \to \forall a \in 𝑵 \forall b \in 𝑵 (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)$
103	24 102	sylbir	$⊢ \forall m \in y \forall a \in 𝑵 \forall b \in 𝑵 (b \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩) \to \forall a \in 𝑵 \forall b \in 𝑵 (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)$
104	103	a1i	$⊢ y \in On \to (\forall m \in y \forall a \in 𝑵 \forall b \in 𝑵 (b \in m \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩) \to \forall a \in 𝑵 \forall b \in 𝑵 (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩))$
105	13 104	tfis2	$⊢ y \in On \to \forall a \in 𝑵 \forall b \in 𝑵 (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)$
106		rsp	$⊢ \forall a \in 𝑵 \forall b \in 𝑵 (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩) \to (a \in 𝑵 \to \forall b \in 𝑵 (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩))$
107	105 106	syl	$⊢ y \in On \to (a \in 𝑵 \to \forall b \in 𝑵 (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩))$
108		rsp	$⊢ \forall b \in 𝑵 (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩) \to (b \in 𝑵 \to (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩))$
109	107 108	syl6	$⊢ y \in On \to (a \in 𝑵 \to (b \in 𝑵 \to (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)))$
110	109	impd	$⊢ y \in On \to ((a \in 𝑵 \land b \in 𝑵) \to (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩))$
111	110	com12	$⊢ (a \in 𝑵 \land b \in 𝑵) \to (y \in On \to (b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩))$
112	111	rexlimdv	$⊢ (a \in 𝑵 \land b \in 𝑵) \to (\exists y \in On b \in y \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)$
113	10 112	mpd	$⊢ (a \in 𝑵 \land b \in 𝑵) \to \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩$
114		breq2	$⊢ A = ⟨a, b⟩ \to (x ~_{𝑸} A \leftrightarrow x ~_{𝑸} ⟨a, b⟩)$
115	114	rexbidv	$⊢ A = ⟨a, b⟩ \to (\exists x \in 𝑸 x ~_{𝑸} A \leftrightarrow \exists x \in 𝑸 x ~_{𝑸} ⟨a, b⟩)$
116	113 115	syl5ibrcom	$⊢ (a \in 𝑵 \land b \in 𝑵) \to (A = ⟨a, b⟩ \to \exists x \in 𝑸 x ~_{𝑸} A)$
117	116	rexlimivv	$⊢ \exists a \in 𝑵 \exists b \in 𝑵 A = ⟨a, b⟩ \to \exists x \in 𝑸 x ~_{𝑸} A$
118	1 117	sylbi	$⊢ A \in (𝑵 \times 𝑵) \to \exists x \in 𝑸 x ~_{𝑸} A$
119		breq2	$⊢ a = A \to (x ~_{𝑸} a \leftrightarrow x ~_{𝑸} A)$
120		breq2	$⊢ a = A \to (y ~_{𝑸} a \leftrightarrow y ~_{𝑸} A)$
121	119 120	anbi12d	$⊢ a = A \to ((x ~_{𝑸} a \land y ~_{𝑸} a) \leftrightarrow (x ~_{𝑸} A \land y ~_{𝑸} A))$
122	121	imbi1d	$⊢ a = A \to (((x ~_{𝑸} a \land y ~_{𝑸} a) \to x = y) \leftrightarrow ((x ~_{𝑸} A \land y ~_{𝑸} A) \to x = y))$
123	122	2ralbidv	$⊢ a = A \to (\forall x \in 𝑸 \forall y \in 𝑸 ((x ~_{𝑸} a \land y ~_{𝑸} a) \to x = y) \leftrightarrow \forall x \in 𝑸 \forall y \in 𝑸 ((x ~_{𝑸} A \land y ~_{𝑸} A) \to x = y))$
124	64	a1i	$⊢ (x ~_{𝑸} a \land y ~_{𝑸} a) \to ~_{𝑸} Er (𝑵 \times 𝑵)$
125		simpl	$⊢ (x ~_{𝑸} a \land y ~_{𝑸} a) \to x ~_{𝑸} a$
126		simpr	$⊢ (x ~_{𝑸} a \land y ~_{𝑸} a) \to y ~_{𝑸} a$
127	124 125 126	ertr4d	$⊢ (x ~_{𝑸} a \land y ~_{𝑸} a) \to x ~_{𝑸} y$
128		mulcompi	$⊢ 2^{nd} (x) \cdot_{𝑵} 1^{st} (x) = 1^{st} (x) \cdot_{𝑵} 2^{nd} (x)$
129		elpqn	$⊢ y \in 𝑸 \to y \in (𝑵 \times 𝑵)$
130		breq1	$⊢ y = x \to (y ~_{𝑸} z \leftrightarrow x ~_{𝑸} z)$
131		fveq2	$⊢ y = x \to 2^{nd} (y) = 2^{nd} (x)$
132	131	breq2d	$⊢ y = x \to (2^{nd} (z) <_{𝑵} 2^{nd} (y) \leftrightarrow 2^{nd} (z) <_{𝑵} 2^{nd} (x))$
133	132	notbid	$⊢ y = x \to (\neg 2^{nd} (z) <_{𝑵} 2^{nd} (y) \leftrightarrow \neg 2^{nd} (z) <_{𝑵} 2^{nd} (x))$
134	130 133	imbi12d	$⊢ y = x \to ((y ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} 2^{nd} (y)) \leftrightarrow (x ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} 2^{nd} (x)))$
135	134	ralbidv	$⊢ y = x \to (\forall z \in (𝑵 \times 𝑵) (y ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} 2^{nd} (y)) \leftrightarrow \forall z \in (𝑵 \times 𝑵) (x ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} 2^{nd} (x)))$
136	135 91	elrab2	$⊢ x \in 𝑸 \leftrightarrow (x \in (𝑵 \times 𝑵) \land \forall z \in (𝑵 \times 𝑵) (x ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} 2^{nd} (x)))$
137	136	simprbi	$⊢ x \in 𝑸 \to \forall z \in (𝑵 \times 𝑵) (x ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} 2^{nd} (x))$
138		breq2	$⊢ z = y \to (x ~_{𝑸} z \leftrightarrow x ~_{𝑸} y)$
139		fveq2	$⊢ z = y \to 2^{nd} (z) = 2^{nd} (y)$
140	139	breq1d	$⊢ z = y \to (2^{nd} (z) <_{𝑵} 2^{nd} (x) \leftrightarrow 2^{nd} (y) <_{𝑵} 2^{nd} (x))$
141	140	notbid	$⊢ z = y \to (\neg 2^{nd} (z) <_{𝑵} 2^{nd} (x) \leftrightarrow \neg 2^{nd} (y) <_{𝑵} 2^{nd} (x))$
142	138 141	imbi12d	$⊢ z = y \to ((x ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} 2^{nd} (x)) \leftrightarrow (x ~_{𝑸} y \to \neg 2^{nd} (y) <_{𝑵} 2^{nd} (x)))$
143	142	rspcva	$⊢ (y \in (𝑵 \times 𝑵) \land \forall z \in (𝑵 \times 𝑵) (x ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} 2^{nd} (x))) \to (x ~_{𝑸} y \to \neg 2^{nd} (y) <_{𝑵} 2^{nd} (x))$
144	129 137 143	syl2anr	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (x ~_{𝑸} y \to \neg 2^{nd} (y) <_{𝑵} 2^{nd} (x))$
145	144	imp	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to \neg 2^{nd} (y) <_{𝑵} 2^{nd} (x)$
146		elpqn	$⊢ x \in 𝑸 \to x \in (𝑵 \times 𝑵)$
147	91	reqabi	$⊢ y \in 𝑸 \leftrightarrow (y \in (𝑵 \times 𝑵) \land \forall z \in (𝑵 \times 𝑵) (y ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} 2^{nd} (y)))$
148	147	simprbi	$⊢ y \in 𝑸 \to \forall z \in (𝑵 \times 𝑵) (y ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} 2^{nd} (y))$
149		breq2	$⊢ z = x \to (y ~_{𝑸} z \leftrightarrow y ~_{𝑸} x)$
150		fveq2	$⊢ z = x \to 2^{nd} (z) = 2^{nd} (x)$
151	150	breq1d	$⊢ z = x \to (2^{nd} (z) <_{𝑵} 2^{nd} (y) \leftrightarrow 2^{nd} (x) <_{𝑵} 2^{nd} (y))$
152	151	notbid	$⊢ z = x \to (\neg 2^{nd} (z) <_{𝑵} 2^{nd} (y) \leftrightarrow \neg 2^{nd} (x) <_{𝑵} 2^{nd} (y))$
153	149 152	imbi12d	$⊢ z = x \to ((y ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} 2^{nd} (y)) \leftrightarrow (y ~_{𝑸} x \to \neg 2^{nd} (x) <_{𝑵} 2^{nd} (y)))$
154	153	rspcva	$⊢ (x \in (𝑵 \times 𝑵) \land \forall z \in (𝑵 \times 𝑵) (y ~_{𝑸} z \to \neg 2^{nd} (z) <_{𝑵} 2^{nd} (y))) \to (y ~_{𝑸} x \to \neg 2^{nd} (x) <_{𝑵} 2^{nd} (y))$
155	146 148 154	syl2an	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (y ~_{𝑸} x \to \neg 2^{nd} (x) <_{𝑵} 2^{nd} (y))$
156	64	a1i	$⊢ x ~_{𝑸} y \to ~_{𝑸} Er (𝑵 \times 𝑵)$
157		id	$⊢ x ~_{𝑸} y \to x ~_{𝑸} y$
158	156 157	ersym	$⊢ x ~_{𝑸} y \to y ~_{𝑸} x$
159	155 158	impel	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to \neg 2^{nd} (x) <_{𝑵} 2^{nd} (y)$
160		xp2nd	$⊢ x \in (𝑵 \times 𝑵) \to 2^{nd} (x) \in 𝑵$
161	146 160	syl	$⊢ x \in 𝑸 \to 2^{nd} (x) \in 𝑵$
162	161	ad2antrr	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to 2^{nd} (x) \in 𝑵$
163		xp2nd	$⊢ y \in (𝑵 \times 𝑵) \to 2^{nd} (y) \in 𝑵$
164	129 163	syl	$⊢ y \in 𝑸 \to 2^{nd} (y) \in 𝑵$
165	164	ad2antlr	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to 2^{nd} (y) \in 𝑵$
166		ltsopi	$⊢ <_{𝑵} Or 𝑵$
167		sotric	$⊢ (<_{𝑵} Or 𝑵 \land (2^{nd} (x) \in 𝑵 \land 2^{nd} (y) \in 𝑵)) \to (2^{nd} (x) <_{𝑵} 2^{nd} (y) \leftrightarrow \neg (2^{nd} (x) = 2^{nd} (y) \lor 2^{nd} (y) <_{𝑵} 2^{nd} (x)))$
168	166 167	mpan	$⊢ (2^{nd} (x) \in 𝑵 \land 2^{nd} (y) \in 𝑵) \to (2^{nd} (x) <_{𝑵} 2^{nd} (y) \leftrightarrow \neg (2^{nd} (x) = 2^{nd} (y) \lor 2^{nd} (y) <_{𝑵} 2^{nd} (x)))$
169	168	notbid	$⊢ (2^{nd} (x) \in 𝑵 \land 2^{nd} (y) \in 𝑵) \to (\neg 2^{nd} (x) <_{𝑵} 2^{nd} (y) \leftrightarrow \neg \neg (2^{nd} (x) = 2^{nd} (y) \lor 2^{nd} (y) <_{𝑵} 2^{nd} (x)))$
170		notnotb	$⊢ (2^{nd} (x) = 2^{nd} (y) \lor 2^{nd} (y) <_{𝑵} 2^{nd} (x)) \leftrightarrow \neg \neg (2^{nd} (x) = 2^{nd} (y) \lor 2^{nd} (y) <_{𝑵} 2^{nd} (x))$
171	169 170	bitr4di	$⊢ (2^{nd} (x) \in 𝑵 \land 2^{nd} (y) \in 𝑵) \to (\neg 2^{nd} (x) <_{𝑵} 2^{nd} (y) \leftrightarrow (2^{nd} (x) = 2^{nd} (y) \lor 2^{nd} (y) <_{𝑵} 2^{nd} (x)))$
172	162 165 171	syl2anc	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to (\neg 2^{nd} (x) <_{𝑵} 2^{nd} (y) \leftrightarrow (2^{nd} (x) = 2^{nd} (y) \lor 2^{nd} (y) <_{𝑵} 2^{nd} (x)))$
173	159 172	mpbid	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to (2^{nd} (x) = 2^{nd} (y) \lor 2^{nd} (y) <_{𝑵} 2^{nd} (x))$
174	173	ord	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to (\neg 2^{nd} (x) = 2^{nd} (y) \to 2^{nd} (y) <_{𝑵} 2^{nd} (x))$
175	145 174	mt3d	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to 2^{nd} (x) = 2^{nd} (y)$
176	175	oveq2d	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to 1^{st} (x) \cdot_{𝑵} 2^{nd} (x) = 1^{st} (x) \cdot_{𝑵} 2^{nd} (y)$
177	128 176	eqtrid	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to 2^{nd} (x) \cdot_{𝑵} 1^{st} (x) = 1^{st} (x) \cdot_{𝑵} 2^{nd} (y)$
178		1st2nd2	$⊢ x \in (𝑵 \times 𝑵) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
179		1st2nd2	$⊢ y \in (𝑵 \times 𝑵) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
180	178 179	breqan12d	$⊢ (x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \to (x ~_{𝑸} y \leftrightarrow ⟨1^{st} (x), 2^{nd} (x)⟩ ~_{𝑸} ⟨1^{st} (y), 2^{nd} (y)⟩)$
181		xp1st	$⊢ x \in (𝑵 \times 𝑵) \to 1^{st} (x) \in 𝑵$
182	181 160	jca	$⊢ x \in (𝑵 \times 𝑵) \to (1^{st} (x) \in 𝑵 \land 2^{nd} (x) \in 𝑵)$
183		xp1st	$⊢ y \in (𝑵 \times 𝑵) \to 1^{st} (y) \in 𝑵$
184	183 163	jca	$⊢ y \in (𝑵 \times 𝑵) \to (1^{st} (y) \in 𝑵 \land 2^{nd} (y) \in 𝑵)$
185		enqbreq	$⊢ ((1^{st} (x) \in 𝑵 \land 2^{nd} (x) \in 𝑵) \land (1^{st} (y) \in 𝑵 \land 2^{nd} (y) \in 𝑵)) \to (⟨1^{st} (x), 2^{nd} (x)⟩ ~_{𝑸} ⟨1^{st} (y), 2^{nd} (y)⟩ \leftrightarrow 1^{st} (x) \cdot_{𝑵} 2^{nd} (y) = 2^{nd} (x) \cdot_{𝑵} 1^{st} (y))$
186	182 184 185	syl2an	$⊢ (x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \to (⟨1^{st} (x), 2^{nd} (x)⟩ ~_{𝑸} ⟨1^{st} (y), 2^{nd} (y)⟩ \leftrightarrow 1^{st} (x) \cdot_{𝑵} 2^{nd} (y) = 2^{nd} (x) \cdot_{𝑵} 1^{st} (y))$
187	180 186	bitrd	$⊢ (x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \to (x ~_{𝑸} y \leftrightarrow 1^{st} (x) \cdot_{𝑵} 2^{nd} (y) = 2^{nd} (x) \cdot_{𝑵} 1^{st} (y))$
188	146 129 187	syl2an	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (x ~_{𝑸} y \leftrightarrow 1^{st} (x) \cdot_{𝑵} 2^{nd} (y) = 2^{nd} (x) \cdot_{𝑵} 1^{st} (y))$
189	188	biimpa	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to 1^{st} (x) \cdot_{𝑵} 2^{nd} (y) = 2^{nd} (x) \cdot_{𝑵} 1^{st} (y)$
190	177 189	eqtrd	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to 2^{nd} (x) \cdot_{𝑵} 1^{st} (x) = 2^{nd} (x) \cdot_{𝑵} 1^{st} (y)$
191	146	ad2antrr	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to x \in (𝑵 \times 𝑵)$
192		mulcanpi	$⊢ (2^{nd} (x) \in 𝑵 \land 1^{st} (x) \in 𝑵) \to (2^{nd} (x) \cdot_{𝑵} 1^{st} (x) = 2^{nd} (x) \cdot_{𝑵} 1^{st} (y) \leftrightarrow 1^{st} (x) = 1^{st} (y))$
193	160 181 192	syl2anc	$⊢ x \in (𝑵 \times 𝑵) \to (2^{nd} (x) \cdot_{𝑵} 1^{st} (x) = 2^{nd} (x) \cdot_{𝑵} 1^{st} (y) \leftrightarrow 1^{st} (x) = 1^{st} (y))$
194	191 193	syl	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to (2^{nd} (x) \cdot_{𝑵} 1^{st} (x) = 2^{nd} (x) \cdot_{𝑵} 1^{st} (y) \leftrightarrow 1^{st} (x) = 1^{st} (y))$
195	190 194	mpbid	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to 1^{st} (x) = 1^{st} (y)$
196	195 175	opeq12d	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to ⟨1^{st} (x), 2^{nd} (x)⟩ = ⟨1^{st} (y), 2^{nd} (y)⟩$
197	191 178	syl	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
198	129	ad2antlr	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to y \in (𝑵 \times 𝑵)$
199	198 179	syl	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
200	196 197 199	3eqtr4d	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land x ~_{𝑸} y) \to x = y$
201	200	ex	$⊢ (x \in 𝑸 \land y \in 𝑸) \to (x ~_{𝑸} y \to x = y)$
202	127 201	syl5	$⊢ (x \in 𝑸 \land y \in 𝑸) \to ((x ~_{𝑸} a \land y ~_{𝑸} a) \to x = y)$
203	202	rgen2	$⊢ \forall x \in 𝑸 \forall y \in 𝑸 ((x ~_{𝑸} a \land y ~_{𝑸} a) \to x = y)$
204	123 203	vtoclg	$⊢ A \in (𝑵 \times 𝑵) \to \forall x \in 𝑸 \forall y \in 𝑸 ((x ~_{𝑸} A \land y ~_{𝑸} A) \to x = y)$
205		breq1	$⊢ x = y \to (x ~_{𝑸} A \leftrightarrow y ~_{𝑸} A)$
206	205	reu4	$⊢ \exists! x \in 𝑸 x ~_{𝑸} A \leftrightarrow (\exists x \in 𝑸 x ~_{𝑸} A \land \forall x \in 𝑸 \forall y \in 𝑸 ((x ~_{𝑸} A \land y ~_{𝑸} A) \to x = y))$
207	118 204 206	sylanbrc	$⊢ A \in (𝑵 \times 𝑵) \to \exists! x \in 𝑸 x ~_{𝑸} A$

Metamath Proof Explorer

Theorem nqereu

Proof