MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nqereu Structured version   Visualization version   GIF version

Theorem nqereu 9695
Description: There is a unique element of Q equivalent to each element of N × N. (Contributed by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
Assertion
Ref Expression
nqereu (𝐴 ∈ (N × N) → ∃!𝑥Q 𝑥 ~Q 𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem nqereu
Dummy variables 𝑎 𝑏 𝑦 𝑐 𝑑 𝑚 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxp2 5092 . . 3 (𝐴 ∈ (N × N) ↔ ∃𝑎N𝑏N 𝐴 = ⟨𝑎, 𝑏⟩)
2 pion 9645 . . . . . . . . 9 (𝑏N𝑏 ∈ On)
3 suceloni 6960 . . . . . . . . 9 (𝑏 ∈ On → suc 𝑏 ∈ On)
42, 3syl 17 . . . . . . . 8 (𝑏N → suc 𝑏 ∈ On)
5 vex 3189 . . . . . . . . 9 𝑏 ∈ V
65sucid 5763 . . . . . . . 8 𝑏 ∈ suc 𝑏
7 eleq2 2687 . . . . . . . . 9 (𝑦 = suc 𝑏 → (𝑏𝑦𝑏 ∈ suc 𝑏))
87rspcev 3295 . . . . . . . 8 ((suc 𝑏 ∈ On ∧ 𝑏 ∈ suc 𝑏) → ∃𝑦 ∈ On 𝑏𝑦)
94, 6, 8sylancl 693 . . . . . . 7 (𝑏N → ∃𝑦 ∈ On 𝑏𝑦)
109adantl 482 . . . . . 6 ((𝑎N𝑏N) → ∃𝑦 ∈ On 𝑏𝑦)
11 elequ2 2001 . . . . . . . . . . . . . 14 (𝑦 = 𝑚 → (𝑏𝑦𝑏𝑚))
1211imbi1d 331 . . . . . . . . . . . . 13 (𝑦 = 𝑚 → ((𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩) ↔ (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
13122ralbidv 2983 . . . . . . . . . . . 12 (𝑦 = 𝑚 → (∀𝑎N𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩) ↔ ∀𝑎N𝑏N (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
14 opeq1 4370 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑎 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑑⟩)
1514breq2d 4625 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑎 → (𝑥 ~Q𝑐, 𝑑⟩ ↔ 𝑥 ~Q𝑎, 𝑑⟩))
1615rexbidv 3045 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑎 → (∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩ ↔ ∃𝑥Q 𝑥 ~Q𝑎, 𝑑⟩))
1716imbi2d 330 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑎 → ((𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑑⟩)))
18 elequ1 1994 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 → (𝑑𝑚𝑏𝑚))
19 opeq2 4371 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑏 → ⟨𝑎, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
2019breq2d 4625 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑏 → (𝑥 ~Q𝑎, 𝑑⟩ ↔ 𝑥 ~Q𝑎, 𝑏⟩))
2120rexbidv 3045 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 → (∃𝑥Q 𝑥 ~Q𝑎, 𝑑⟩ ↔ ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
2218, 21imbi12d 334 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑏 → ((𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑑⟩) ↔ (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
2317, 22cbvral2v 3167 . . . . . . . . . . . . . . 15 (∀𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ ∀𝑎N𝑏N (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
2423ralbii 2974 . . . . . . . . . . . . . 14 (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ ∀𝑚𝑦𝑎N𝑏N (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
25 rexnal 2989 . . . . . . . . . . . . . . . . . . 19 (∃𝑧 ∈ (N × N) ¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) ↔ ¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏))
26 pm4.63 437 . . . . . . . . . . . . . . . . . . . . 21 (¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) <N 𝑏))
27 xp2nd 7144 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ (N × N) → (2nd𝑧) ∈ N)
28 ltpiord 9653 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2nd𝑧) ∈ N𝑏N) → ((2nd𝑧) <N 𝑏 ↔ (2nd𝑧) ∈ 𝑏))
2928ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏N ∧ (2nd𝑧) ∈ N) → ((2nd𝑧) <N 𝑏 ↔ (2nd𝑧) ∈ 𝑏))
3027, 29sylan2 491 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏N𝑧 ∈ (N × N)) → ((2nd𝑧) <N 𝑏 ↔ (2nd𝑧) ∈ 𝑏))
3130adantll 749 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎N𝑏N) ∧ 𝑧 ∈ (N × N)) → ((2nd𝑧) <N 𝑏 ↔ (2nd𝑧) ∈ 𝑏))
3231anbi2d 739 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎N𝑏N) ∧ 𝑧 ∈ (N × N)) → ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) ∈ 𝑏)))
3326, 32syl5bb 272 . . . . . . . . . . . . . . . . . . . 20 (((𝑎N𝑏N) ∧ 𝑧 ∈ (N × N)) → (¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) ∈ 𝑏)))
3433rexbidva 3042 . . . . . . . . . . . . . . . . . . 19 ((𝑎N𝑏N) → (∃𝑧 ∈ (N × N) ¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) ↔ ∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) ∈ 𝑏)))
3525, 34syl5bbr 274 . . . . . . . . . . . . . . . . . 18 ((𝑎N𝑏N) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) ↔ ∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) ∈ 𝑏)))
36 xp1st 7143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ (N × N) → (1st𝑧) ∈ N)
37 elequ2 2001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑚 = 𝑏 → (𝑑𝑚𝑑𝑏))
3837imbi1d 331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 = 𝑏 → ((𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩)))
39382ralbidv 2983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚 = 𝑏 → (∀𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ ∀𝑐N𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩)))
4039rspccv 3292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → (𝑏𝑦 → ∀𝑐N𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩)))
41 opeq1 4370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑐 = (1st𝑧) → ⟨𝑐, 𝑑⟩ = ⟨(1st𝑧), 𝑑⟩)
4241breq2d 4625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑐 = (1st𝑧) → (𝑥 ~Q𝑐, 𝑑⟩ ↔ 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩))
4342rexbidv 3045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = (1st𝑧) → (∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩ ↔ ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩))
4443imbi2d 330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = (1st𝑧) → ((𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩)))
4544ralbidv 2980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = (1st𝑧) → (∀𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ ∀𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩)))
4645rspccv 3292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∀𝑐N𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → ((1st𝑧) ∈ N → ∀𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩)))
47 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑑 = (2nd𝑧) → (𝑑𝑏 ↔ (2nd𝑧) ∈ 𝑏))
48 opeq2 4371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑑 = (2nd𝑧) → ⟨(1st𝑧), 𝑑⟩ = ⟨(1st𝑧), (2nd𝑧)⟩)
4948breq2d 4625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑑 = (2nd𝑧) → (𝑥 ~Q ⟨(1st𝑧), 𝑑⟩ ↔ 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))
5049rexbidv 3045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑑 = (2nd𝑧) → (∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩ ↔ ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))
5147, 50imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑑 = (2nd𝑧) → ((𝑑𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩) ↔ ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩)))
5251rspccv 3292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∀𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩) → ((2nd𝑧) ∈ N → ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩)))
5346, 52syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑐N𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → ((1st𝑧) ∈ N → ((2nd𝑧) ∈ N → ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))))
5440, 53syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → (𝑏𝑦 → ((1st𝑧) ∈ N → ((2nd𝑧) ∈ N → ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩)))))
5554imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) → ((1st𝑧) ∈ N → ((2nd𝑧) ∈ N → ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))))
5636, 55syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) → (𝑧 ∈ (N × N) → ((2nd𝑧) ∈ N → ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))))
5727, 56mpdi 45 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) → (𝑧 ∈ (N × N) → ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩)))
58573imp 1254 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd𝑧) ∈ 𝑏) → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩)
59 1st2nd2 7150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ (N × N) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
6059breq2d 4625 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ (N × N) → (𝑥 ~Q 𝑧𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))
6160rexbidv 3045 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ (N × N) → (∃𝑥Q 𝑥 ~Q 𝑧 ↔ ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))
62613ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd𝑧) ∈ 𝑏) → (∃𝑥Q 𝑥 ~Q 𝑧 ↔ ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))
6358, 62mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd𝑧) ∈ 𝑏) → ∃𝑥Q 𝑥 ~Q 𝑧)
64 enqer 9687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ~Q Er (N × N)
6564a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((⟨𝑎, 𝑏⟩ ~Q 𝑧𝑥 ~Q 𝑧) → ~Q Er (N × N))
66 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((⟨𝑎, 𝑏⟩ ~Q 𝑧𝑥 ~Q 𝑧) → 𝑥 ~Q 𝑧)
67 simpl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((⟨𝑎, 𝑏⟩ ~Q 𝑧𝑥 ~Q 𝑧) → ⟨𝑎, 𝑏⟩ ~Q 𝑧)
6865, 66, 67ertr4d 7706 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑎, 𝑏⟩ ~Q 𝑧𝑥 ~Q 𝑧) → 𝑥 ~Q𝑎, 𝑏⟩)
6968ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑎, 𝑏⟩ ~Q 𝑧 → (𝑥 ~Q 𝑧𝑥 ~Q𝑎, 𝑏⟩))
7069reximdv 3010 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟨𝑎, 𝑏⟩ ~Q 𝑧 → (∃𝑥Q 𝑥 ~Q 𝑧 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
7163, 70syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . 24 (((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd𝑧) ∈ 𝑏) → (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
72713expia 1264 . . . . . . . . . . . . . . . . . . . . . . 23 (((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) ∧ 𝑧 ∈ (N × N)) → ((2nd𝑧) ∈ 𝑏 → (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
7372com23 86 . . . . . . . . . . . . . . . . . . . . . 22 (((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) ∧ 𝑧 ∈ (N × N)) → (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
7473impd 447 . . . . . . . . . . . . . . . . . . . . 21 (((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) ∧ 𝑧 ∈ (N × N)) → ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) ∈ 𝑏) → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
7574rexlimdva 3024 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) → (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) ∈ 𝑏) → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
7675ex 450 . . . . . . . . . . . . . . . . . . 19 (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → (𝑏𝑦 → (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) ∈ 𝑏) → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
7776com3r 87 . . . . . . . . . . . . . . . . . 18 (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) ∈ 𝑏) → (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
7835, 77syl6bi 243 . . . . . . . . . . . . . . . . 17 ((𝑎N𝑏N) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) → (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))))
7978com13 88 . . . . . . . . . . . . . . . 16 (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) → ((𝑎N𝑏N) → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))))
80 mulcompi 9662 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)
81 enqbreq 9685 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎N𝑏N) ∧ (𝑎N𝑏N)) → (⟨𝑎, 𝑏⟩ ~Q𝑎, 𝑏⟩ ↔ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)))
8281anidms 676 . . . . . . . . . . . . . . . . . . . 20 ((𝑎N𝑏N) → (⟨𝑎, 𝑏⟩ ~Q𝑎, 𝑏⟩ ↔ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)))
8380, 82mpbiri 248 . . . . . . . . . . . . . . . . . . 19 ((𝑎N𝑏N) → ⟨𝑎, 𝑏⟩ ~Q𝑎, 𝑏⟩)
84 opelxpi 5108 . . . . . . . . . . . . . . . . . . . 20 ((𝑎N𝑏N) → ⟨𝑎, 𝑏⟩ ∈ (N × N))
85 breq1 4616 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ~Q 𝑧 ↔ ⟨𝑎, 𝑏⟩ ~Q 𝑧))
86 vex 3189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎 ∈ V
8786, 5op2ndd 7124 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd𝑦) = 𝑏)
8887breq2d 4625 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd𝑧) <N (2nd𝑦) ↔ (2nd𝑧) <N 𝑏))
8988notbid 308 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → (¬ (2nd𝑧) <N (2nd𝑦) ↔ ¬ (2nd𝑧) <N 𝑏))
9085, 89imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦)) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏)))
9190ralbidv 2980 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = ⟨𝑎, 𝑏⟩ → (∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦)) ↔ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏)))
92 df-nq 9678 . . . . . . . . . . . . . . . . . . . . . 22 Q = {𝑦 ∈ (N × N) ∣ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦))}
9391, 92elrab2 3348 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑎, 𝑏⟩ ∈ Q ↔ (⟨𝑎, 𝑏⟩ ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏)))
9493simplbi2 654 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑎, 𝑏⟩ ∈ (N × N) → (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) → ⟨𝑎, 𝑏⟩ ∈ Q))
9584, 94syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑎N𝑏N) → (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) → ⟨𝑎, 𝑏⟩ ∈ Q))
96 breq1 4616 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨𝑎, 𝑏⟩ → (𝑥 ~Q𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ ~Q𝑎, 𝑏⟩))
9796rspcev 3295 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑎, 𝑏⟩ ∈ Q ∧ ⟨𝑎, 𝑏⟩ ~Q𝑎, 𝑏⟩) → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)
9897expcom 451 . . . . . . . . . . . . . . . . . . 19 (⟨𝑎, 𝑏⟩ ~Q𝑎, 𝑏⟩ → (⟨𝑎, 𝑏⟩ ∈ Q → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
9983, 95, 98sylsyld 61 . . . . . . . . . . . . . . . . . 18 ((𝑎N𝑏N) → (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
10099com12 32 . . . . . . . . . . . . . . . . 17 (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) → ((𝑎N𝑏N) → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
101100a1dd 50 . . . . . . . . . . . . . . . 16 (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) → ((𝑎N𝑏N) → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
10279, 101pm2.61d2 172 . . . . . . . . . . . . . . 15 (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → ((𝑎N𝑏N) → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
103102ralrimivv 2964 . . . . . . . . . . . . . 14 (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → ∀𝑎N𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
10424, 103sylbir 225 . . . . . . . . . . . . 13 (∀𝑚𝑦𝑎N𝑏N (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩) → ∀𝑎N𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
105104a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ On → (∀𝑚𝑦𝑎N𝑏N (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩) → ∀𝑎N𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
10613, 105tfis2 7003 . . . . . . . . . . 11 (𝑦 ∈ On → ∀𝑎N𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
107 rsp 2924 . . . . . . . . . . 11 (∀𝑎N𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩) → (𝑎N → ∀𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
108106, 107syl 17 . . . . . . . . . 10 (𝑦 ∈ On → (𝑎N → ∀𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
109 rsp 2924 . . . . . . . . . 10 (∀𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩) → (𝑏N → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
110108, 109syl6 35 . . . . . . . . 9 (𝑦 ∈ On → (𝑎N → (𝑏N → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))))
111110impd 447 . . . . . . . 8 (𝑦 ∈ On → ((𝑎N𝑏N) → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
112111com12 32 . . . . . . 7 ((𝑎N𝑏N) → (𝑦 ∈ On → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
113112rexlimdv 3023 . . . . . 6 ((𝑎N𝑏N) → (∃𝑦 ∈ On 𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
11410, 113mpd 15 . . . . 5 ((𝑎N𝑏N) → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)
115 breq2 4617 . . . . . 6 (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑥 ~Q 𝐴𝑥 ~Q𝑎, 𝑏⟩))
116115rexbidv 3045 . . . . 5 (𝐴 = ⟨𝑎, 𝑏⟩ → (∃𝑥Q 𝑥 ~Q 𝐴 ↔ ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
117114, 116syl5ibrcom 237 . . . 4 ((𝑎N𝑏N) → (𝐴 = ⟨𝑎, 𝑏⟩ → ∃𝑥Q 𝑥 ~Q 𝐴))
118117rexlimivv 3029 . . 3 (∃𝑎N𝑏N 𝐴 = ⟨𝑎, 𝑏⟩ → ∃𝑥Q 𝑥 ~Q 𝐴)
1191, 118sylbi 207 . 2 (𝐴 ∈ (N × N) → ∃𝑥Q 𝑥 ~Q 𝐴)
120 breq2 4617 . . . . . 6 (𝑎 = 𝐴 → (𝑥 ~Q 𝑎𝑥 ~Q 𝐴))
121 breq2 4617 . . . . . 6 (𝑎 = 𝐴 → (𝑦 ~Q 𝑎𝑦 ~Q 𝐴))
122120, 121anbi12d 746 . . . . 5 (𝑎 = 𝐴 → ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) ↔ (𝑥 ~Q 𝐴𝑦 ~Q 𝐴)))
123122imbi1d 331 . . . 4 (𝑎 = 𝐴 → (((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ((𝑥 ~Q 𝐴𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
1241232ralbidv 2983 . . 3 (𝑎 = 𝐴 → (∀𝑥Q𝑦Q ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ∀𝑥Q𝑦Q ((𝑥 ~Q 𝐴𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
12564a1i 11 . . . . . 6 ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → ~Q Er (N × N))
126 simpl 473 . . . . . 6 ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑎)
127 simpr 477 . . . . . 6 ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑦 ~Q 𝑎)
128125, 126, 127ertr4d 7706 . . . . 5 ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑦)
129 mulcompi 9662 . . . . . . . . . . 11 ((2nd𝑥) ·N (1st𝑥)) = ((1st𝑥) ·N (2nd𝑥))
130 elpqn 9691 . . . . . . . . . . . . . . 15 (𝑦Q𝑦 ∈ (N × N))
131 breq1 4616 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → (𝑦 ~Q 𝑧𝑥 ~Q 𝑧))
132 fveq2 6148 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → (2nd𝑦) = (2nd𝑥))
133132breq2d 4625 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → ((2nd𝑧) <N (2nd𝑦) ↔ (2nd𝑧) <N (2nd𝑥)))
134133notbid 308 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → (¬ (2nd𝑧) <N (2nd𝑦) ↔ ¬ (2nd𝑧) <N (2nd𝑥)))
135131, 134imbi12d 334 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑥 → ((𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦)) ↔ (𝑥 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑥))))
136135ralbidv 2980 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑥 → (∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦)) ↔ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑥))))
137136, 92elrab2 3348 . . . . . . . . . . . . . . . 16 (𝑥Q ↔ (𝑥 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑥))))
138137simprbi 480 . . . . . . . . . . . . . . 15 (𝑥Q → ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑥)))
139 breq2 4617 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑦 → (𝑥 ~Q 𝑧𝑥 ~Q 𝑦))
140 fveq2 6148 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑦 → (2nd𝑧) = (2nd𝑦))
141140breq1d 4623 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → ((2nd𝑧) <N (2nd𝑥) ↔ (2nd𝑦) <N (2nd𝑥)))
142141notbid 308 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑦 → (¬ (2nd𝑧) <N (2nd𝑥) ↔ ¬ (2nd𝑦) <N (2nd𝑥)))
143139, 142imbi12d 334 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → ((𝑥 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑥)) ↔ (𝑥 ~Q 𝑦 → ¬ (2nd𝑦) <N (2nd𝑥))))
144143rspcva 3293 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑥))) → (𝑥 ~Q 𝑦 → ¬ (2nd𝑦) <N (2nd𝑥)))
145130, 138, 144syl2anr 495 . . . . . . . . . . . . . 14 ((𝑥Q𝑦Q) → (𝑥 ~Q 𝑦 → ¬ (2nd𝑦) <N (2nd𝑥)))
146145imp 445 . . . . . . . . . . . . 13 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → ¬ (2nd𝑦) <N (2nd𝑥))
14764a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ~Q 𝑦 → ~Q Er (N × N))
148 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 ~Q 𝑦𝑥 ~Q 𝑦)
149147, 148ersym 7699 . . . . . . . . . . . . . . . . 17 (𝑥 ~Q 𝑦𝑦 ~Q 𝑥)
150 elpqn 9691 . . . . . . . . . . . . . . . . . 18 (𝑥Q𝑥 ∈ (N × N))
15192rabeq2i 3183 . . . . . . . . . . . . . . . . . . 19 (𝑦Q ↔ (𝑦 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦))))
152151simprbi 480 . . . . . . . . . . . . . . . . . 18 (𝑦Q → ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦)))
153 breq2 4617 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (𝑦 ~Q 𝑧𝑦 ~Q 𝑥))
154 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑥 → (2nd𝑧) = (2nd𝑥))
155154breq1d 4623 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑥 → ((2nd𝑧) <N (2nd𝑦) ↔ (2nd𝑥) <N (2nd𝑦)))
156155notbid 308 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (¬ (2nd𝑧) <N (2nd𝑦) ↔ ¬ (2nd𝑥) <N (2nd𝑦)))
157153, 156imbi12d 334 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑥 → ((𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦)) ↔ (𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))))
158157rspcva 3293 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦))) → (𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦)))
159150, 152, 158syl2an 494 . . . . . . . . . . . . . . . . 17 ((𝑥Q𝑦Q) → (𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦)))
160149, 159syl5 34 . . . . . . . . . . . . . . . 16 ((𝑥Q𝑦Q) → (𝑥 ~Q 𝑦 → ¬ (2nd𝑥) <N (2nd𝑦)))
161160imp 445 . . . . . . . . . . . . . . 15 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → ¬ (2nd𝑥) <N (2nd𝑦))
162 xp2nd 7144 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (N × N) → (2nd𝑥) ∈ N)
163150, 162syl 17 . . . . . . . . . . . . . . . . 17 (𝑥Q → (2nd𝑥) ∈ N)
164163ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → (2nd𝑥) ∈ N)
165 xp2nd 7144 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (N × N) → (2nd𝑦) ∈ N)
166130, 165syl 17 . . . . . . . . . . . . . . . . 17 (𝑦Q → (2nd𝑦) ∈ N)
167166ad2antlr 762 . . . . . . . . . . . . . . . 16 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → (2nd𝑦) ∈ N)
168 ltsopi 9654 . . . . . . . . . . . . . . . . . . 19 <N Or N
169 sotric 5021 . . . . . . . . . . . . . . . . . . 19 (( <N Or N ∧ ((2nd𝑥) ∈ N ∧ (2nd𝑦) ∈ N)) → ((2nd𝑥) <N (2nd𝑦) ↔ ¬ ((2nd𝑥) = (2nd𝑦) ∨ (2nd𝑦) <N (2nd𝑥))))
170168, 169mpan 705 . . . . . . . . . . . . . . . . . 18 (((2nd𝑥) ∈ N ∧ (2nd𝑦) ∈ N) → ((2nd𝑥) <N (2nd𝑦) ↔ ¬ ((2nd𝑥) = (2nd𝑦) ∨ (2nd𝑦) <N (2nd𝑥))))
171170notbid 308 . . . . . . . . . . . . . . . . 17 (((2nd𝑥) ∈ N ∧ (2nd𝑦) ∈ N) → (¬ (2nd𝑥) <N (2nd𝑦) ↔ ¬ ¬ ((2nd𝑥) = (2nd𝑦) ∨ (2nd𝑦) <N (2nd𝑥))))
172 notnotb 304 . . . . . . . . . . . . . . . . 17 (((2nd𝑥) = (2nd𝑦) ∨ (2nd𝑦) <N (2nd𝑥)) ↔ ¬ ¬ ((2nd𝑥) = (2nd𝑦) ∨ (2nd𝑦) <N (2nd𝑥)))
173171, 172syl6bbr 278 . . . . . . . . . . . . . . . 16 (((2nd𝑥) ∈ N ∧ (2nd𝑦) ∈ N) → (¬ (2nd𝑥) <N (2nd𝑦) ↔ ((2nd𝑥) = (2nd𝑦) ∨ (2nd𝑦) <N (2nd𝑥))))
174164, 167, 173syl2anc 692 . . . . . . . . . . . . . . 15 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → (¬ (2nd𝑥) <N (2nd𝑦) ↔ ((2nd𝑥) = (2nd𝑦) ∨ (2nd𝑦) <N (2nd𝑥))))
175161, 174mpbid 222 . . . . . . . . . . . . . 14 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → ((2nd𝑥) = (2nd𝑦) ∨ (2nd𝑦) <N (2nd𝑥)))
176175ord 392 . . . . . . . . . . . . 13 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → (¬ (2nd𝑥) = (2nd𝑦) → (2nd𝑦) <N (2nd𝑥)))
177146, 176mt3d 140 . . . . . . . . . . . 12 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → (2nd𝑥) = (2nd𝑦))
178177oveq2d 6620 . . . . . . . . . . 11 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → ((1st𝑥) ·N (2nd𝑥)) = ((1st𝑥) ·N (2nd𝑦)))
179129, 178syl5eq 2667 . . . . . . . . . 10 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → ((2nd𝑥) ·N (1st𝑥)) = ((1st𝑥) ·N (2nd𝑦)))
180 1st2nd2 7150 . . . . . . . . . . . . . 14 (𝑥 ∈ (N × N) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
181 1st2nd2 7150 . . . . . . . . . . . . . 14 (𝑦 ∈ (N × N) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
182180, 181breqan12d 4629 . . . . . . . . . . . . 13 ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ~Q ⟨(1st𝑦), (2nd𝑦)⟩))
183 xp1st 7143 . . . . . . . . . . . . . . 15 (𝑥 ∈ (N × N) → (1st𝑥) ∈ N)
184183, 162jca 554 . . . . . . . . . . . . . 14 (𝑥 ∈ (N × N) → ((1st𝑥) ∈ N ∧ (2nd𝑥) ∈ N))
185 xp1st 7143 . . . . . . . . . . . . . . 15 (𝑦 ∈ (N × N) → (1st𝑦) ∈ N)
186185, 165jca 554 . . . . . . . . . . . . . 14 (𝑦 ∈ (N × N) → ((1st𝑦) ∈ N ∧ (2nd𝑦) ∈ N))
187 enqbreq 9685 . . . . . . . . . . . . . 14 ((((1st𝑥) ∈ N ∧ (2nd𝑥) ∈ N) ∧ ((1st𝑦) ∈ N ∧ (2nd𝑦) ∈ N)) → (⟨(1st𝑥), (2nd𝑥)⟩ ~Q ⟨(1st𝑦), (2nd𝑦)⟩ ↔ ((1st𝑥) ·N (2nd𝑦)) = ((2nd𝑥) ·N (1st𝑦))))
188184, 186, 187syl2an 494 . . . . . . . . . . . . 13 ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (⟨(1st𝑥), (2nd𝑥)⟩ ~Q ⟨(1st𝑦), (2nd𝑦)⟩ ↔ ((1st𝑥) ·N (2nd𝑦)) = ((2nd𝑥) ·N (1st𝑦))))
189182, 188bitrd 268 . . . . . . . . . . . 12 ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ((1st𝑥) ·N (2nd𝑦)) = ((2nd𝑥) ·N (1st𝑦))))
190150, 130, 189syl2an 494 . . . . . . . . . . 11 ((𝑥Q𝑦Q) → (𝑥 ~Q 𝑦 ↔ ((1st𝑥) ·N (2nd𝑦)) = ((2nd𝑥) ·N (1st𝑦))))
191190biimpa 501 . . . . . . . . . 10 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → ((1st𝑥) ·N (2nd𝑦)) = ((2nd𝑥) ·N (1st𝑦)))
192179, 191eqtrd 2655 . . . . . . . . 9 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → ((2nd𝑥) ·N (1st𝑥)) = ((2nd𝑥) ·N (1st𝑦)))
193150ad2antrr 761 . . . . . . . . . 10 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 ∈ (N × N))
194 mulcanpi 9666 . . . . . . . . . . 11 (((2nd𝑥) ∈ N ∧ (1st𝑥) ∈ N) → (((2nd𝑥) ·N (1st𝑥)) = ((2nd𝑥) ·N (1st𝑦)) ↔ (1st𝑥) = (1st𝑦)))
195162, 183, 194syl2anc 692 . . . . . . . . . 10 (𝑥 ∈ (N × N) → (((2nd𝑥) ·N (1st𝑥)) = ((2nd𝑥) ·N (1st𝑦)) ↔ (1st𝑥) = (1st𝑦)))
196193, 195syl 17 . . . . . . . . 9 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → (((2nd𝑥) ·N (1st𝑥)) = ((2nd𝑥) ·N (1st𝑦)) ↔ (1st𝑥) = (1st𝑦)))
197192, 196mpbid 222 . . . . . . . 8 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → (1st𝑥) = (1st𝑦))
198197, 177opeq12d 4378 . . . . . . 7 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → ⟨(1st𝑥), (2nd𝑥)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩)
199193, 180syl 17 . . . . . . 7 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
200130ad2antlr 762 . . . . . . . 8 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → 𝑦 ∈ (N × N))
201200, 181syl 17 . . . . . . 7 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
202198, 199, 2013eqtr4d 2665 . . . . . 6 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 = 𝑦)
203202ex 450 . . . . 5 ((𝑥Q𝑦Q) → (𝑥 ~Q 𝑦𝑥 = 𝑦))
204128, 203syl5 34 . . . 4 ((𝑥Q𝑦Q) → ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑥 = 𝑦))
205204rgen2a 2971 . . 3 𝑥Q𝑦Q ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑥 = 𝑦)
206124, 205vtoclg 3252 . 2 (𝐴 ∈ (N × N) → ∀𝑥Q𝑦Q ((𝑥 ~Q 𝐴𝑦 ~Q 𝐴) → 𝑥 = 𝑦))
207 breq1 4616 . . 3 (𝑥 = 𝑦 → (𝑥 ~Q 𝐴𝑦 ~Q 𝐴))
208207reu4 3382 . 2 (∃!𝑥Q 𝑥 ~Q 𝐴 ↔ (∃𝑥Q 𝑥 ~Q 𝐴 ∧ ∀𝑥Q𝑦Q ((𝑥 ~Q 𝐴𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
209119, 206, 208sylanbrc 697 1 (𝐴 ∈ (N × N) → ∃!𝑥Q 𝑥 ~Q 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  wrex 2908  ∃!wreu 2909  cop 4154   class class class wbr 4613   Or wor 4994   × cxp 5072  Oncon0 5682  suc csuc 5684  cfv 5847  (class class class)co 6604  1st c1st 7111  2nd c2nd 7112   Er wer 7684  Ncnpi 9610   ·N cmi 9612   <N clti 9613   ~Q ceq 9617  Qcnq 9618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-oadd 7509  df-omul 7510  df-er 7687  df-ni 9638  df-mi 9640  df-lti 9641  df-enq 9677  df-nq 9678
This theorem is referenced by:  nqerf  9696  enqeq  9700
  Copyright terms: Public domain W3C validator