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

Theorem nqereu 9439
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 4898 . . 3 (𝐴 ∈ (N × N) ↔ ∃𝑎N𝑏N 𝐴 = ⟨𝑎, 𝑏⟩)
2 pion 9389 . . . . . . . . 9 (𝑏N𝑏 ∈ On)
3 suceloni 6717 . . . . . . . . 9 (𝑏 ∈ On → suc 𝑏 ∈ On)
42, 3syl 17 . . . . . . . 8 (𝑏N → suc 𝑏 ∈ On)
5 vex 3069 . . . . . . . . 9 𝑏 ∈ V
65sucid 5553 . . . . . . . 8 𝑏 ∈ suc 𝑏
7 eleq2 2572 . . . . . . . . 9 (𝑦 = suc 𝑏 → (𝑏𝑦𝑏 ∈ suc 𝑏))
87rspcev 3171 . . . . . . . 8 ((suc 𝑏 ∈ On ∧ 𝑏 ∈ suc 𝑏) → ∃𝑦 ∈ On 𝑏𝑦)
94, 6, 8sylancl 684 . . . . . . 7 (𝑏N → ∃𝑦 ∈ On 𝑏𝑦)
109adantl 475 . . . . . 6 ((𝑎N𝑏N) → ∃𝑦 ∈ On 𝑏𝑦)
11 elequ2 1951 . . . . . . . . . . . . . 14 (𝑦 = 𝑚 → (𝑏𝑦𝑏𝑚))
1211imbi1d 326 . . . . . . . . . . . . 13 (𝑦 = 𝑚 → ((𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩) ↔ (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
13122ralbidv 2867 . . . . . . . . . . . 12 (𝑦 = 𝑚 → (∀𝑎N𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩) ↔ ∀𝑎N𝑏N (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
14 opeq1 4196 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑎 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑑⟩)
1514breq2d 4446 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑎 → (𝑥 ~Q𝑐, 𝑑⟩ ↔ 𝑥 ~Q𝑎, 𝑑⟩))
1615rexbidv 2927 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑎 → (∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩ ↔ ∃𝑥Q 𝑥 ~Q𝑎, 𝑑⟩))
1716imbi2d 325 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑎 → ((𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑑⟩)))
18 elequ1 1944 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 → (𝑑𝑚𝑏𝑚))
19 opeq2 4197 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑏 → ⟨𝑎, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
2019breq2d 4446 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑏 → (𝑥 ~Q𝑎, 𝑑⟩ ↔ 𝑥 ~Q𝑎, 𝑏⟩))
2120rexbidv 2927 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 → (∃𝑥Q 𝑥 ~Q𝑎, 𝑑⟩ ↔ ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
2218, 21imbi12d 329 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑏 → ((𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑑⟩) ↔ (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
2317, 22cbvral2v 3048 . . . . . . . . . . . . . . 15 (∀𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ ∀𝑎N𝑏N (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
2423ralbii 2858 . . . . . . . . . . . . . 14 (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ ∀𝑚𝑦𝑎N𝑏N (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
25 rexnal 2871 . . . . . . . . . . . . . . . . . . 19 (∃𝑧 ∈ (N × N) ¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) ↔ ¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏))
26 pm4.63 430 . . . . . . . . . . . . . . . . . . . . 21 (¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) <N 𝑏))
27 xp2nd 6901 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ (N × N) → (2nd𝑧) ∈ N)
28 ltpiord 9397 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2nd𝑧) ∈ N𝑏N) → ((2nd𝑧) <N 𝑏 ↔ (2nd𝑧) ∈ 𝑏))
2928ancoms 462 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏N ∧ (2nd𝑧) ∈ N) → ((2nd𝑧) <N 𝑏 ↔ (2nd𝑧) ∈ 𝑏))
3027, 29sylan2 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏N𝑧 ∈ (N × N)) → ((2nd𝑧) <N 𝑏 ↔ (2nd𝑧) ∈ 𝑏))
3130adantll 737 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎N𝑏N) ∧ 𝑧 ∈ (N × N)) → ((2nd𝑧) <N 𝑏 ↔ (2nd𝑧) ∈ 𝑏))
3231anbi2d 727 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎N𝑏N) ∧ 𝑧 ∈ (N × N)) → ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) ∈ 𝑏)))
3326, 32syl5bb 267 . . . . . . . . . . . . . . . . . . . 20 (((𝑎N𝑏N) ∧ 𝑧 ∈ (N × N)) → (¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) ∈ 𝑏)))
3433rexbidva 2924 . . . . . . . . . . . . . . . . . . 19 ((𝑎N𝑏N) → (∃𝑧 ∈ (N × N) ¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) ↔ ∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) ∈ 𝑏)))
3525, 34syl5bbr 269 . . . . . . . . . . . . . . . . . 18 ((𝑎N𝑏N) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) ↔ ∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) ∈ 𝑏)))
36 xp1st 6900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ (N × N) → (1st𝑧) ∈ N)
37 elequ2 1951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑚 = 𝑏 → (𝑑𝑚𝑑𝑏))
3837imbi1d 326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 = 𝑏 → ((𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩)))
39382ralbidv 2867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚 = 𝑏 → (∀𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ ∀𝑐N𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩)))
4039rspccv 3168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → (𝑏𝑦 → ∀𝑐N𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩)))
41 opeq1 4196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑐 = (1st𝑧) → ⟨𝑐, 𝑑⟩ = ⟨(1st𝑧), 𝑑⟩)
4241breq2d 4446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑐 = (1st𝑧) → (𝑥 ~Q𝑐, 𝑑⟩ ↔ 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩))
4342rexbidv 2927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = (1st𝑧) → (∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩ ↔ ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩))
4443imbi2d 325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = (1st𝑧) → ((𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩)))
4544ralbidv 2864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = (1st𝑧) → (∀𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ ∀𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩)))
4645rspccv 3168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∀𝑐N𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → ((1st𝑧) ∈ N → ∀𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩)))
47 eleq1 2571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑑 = (2nd𝑧) → (𝑑𝑏 ↔ (2nd𝑧) ∈ 𝑏))
48 opeq2 4197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑑 = (2nd𝑧) → ⟨(1st𝑧), 𝑑⟩ = ⟨(1st𝑧), (2nd𝑧)⟩)
4948breq2d 4446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑑 = (2nd𝑧) → (𝑥 ~Q ⟨(1st𝑧), 𝑑⟩ ↔ 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))
5049rexbidv 2927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑑 = (2nd𝑧) → (∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩ ↔ ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))
5147, 50imbi12d 329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑑 = (2nd𝑧) → ((𝑑𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩) ↔ ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩)))
5251rspccv 3168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∀𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩) → ((2nd𝑧) ∈ N → ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩)))
5346, 52syl6 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑐N𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → ((1st𝑧) ∈ N → ((2nd𝑧) ∈ N → ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))))
5440, 53syl6 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → (𝑏𝑦 → ((1st𝑧) ∈ N → ((2nd𝑧) ∈ N → ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩)))))
5554imp 438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) → ((1st𝑧) ∈ N → ((2nd𝑧) ∈ N → ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))))
5636, 55syl5 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) → (𝑧 ∈ (N × N) → ((2nd𝑧) ∈ N → ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))))
5727, 56mpdi 43 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) → (𝑧 ∈ (N × N) → ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩)))
58573imp 1239 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd𝑧) ∈ 𝑏) → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩)
59 1st2nd2 6907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ (N × N) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
6059breq2d 4446 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ (N × N) → (𝑥 ~Q 𝑧𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))
6160rexbidv 2927 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 ∈ (N × N) → (∃𝑥Q 𝑥 ~Q 𝑧 ↔ ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))
62613ad2ant2 1066 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd𝑧) ∈ 𝑏) → (∃𝑥Q 𝑥 ~Q 𝑧 ↔ ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))
6358, 62mpbird 242 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd𝑧) ∈ 𝑏) → ∃𝑥Q 𝑥 ~Q 𝑧)
64 enqer 9431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ~Q Er (N × N)
6564a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((⟨𝑎, 𝑏⟩ ~Q 𝑧𝑥 ~Q 𝑧) → ~Q Er (N × N))
66 simpr 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((⟨𝑎, 𝑏⟩ ~Q 𝑧𝑥 ~Q 𝑧) → 𝑥 ~Q 𝑧)
67 simpl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((⟨𝑎, 𝑏⟩ ~Q 𝑧𝑥 ~Q 𝑧) → ⟨𝑎, 𝑏⟩ ~Q 𝑧)
6865, 66, 67ertr4d 7459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑎, 𝑏⟩ ~Q 𝑧𝑥 ~Q 𝑧) → 𝑥 ~Q𝑎, 𝑏⟩)
6968ex 443 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑎, 𝑏⟩ ~Q 𝑧 → (𝑥 ~Q 𝑧𝑥 ~Q𝑎, 𝑏⟩))
7069reximdv 2892 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟨𝑎, 𝑏⟩ ~Q 𝑧 → (∃𝑥Q 𝑥 ~Q 𝑧 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
7163, 70syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . 24 (((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) ∧ 𝑧 ∈ (N × N) ∧ (2nd𝑧) ∈ 𝑏) → (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
72713expia 1249 . . . . . . . . . . . . . . . . . . . . . . 23 (((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) ∧ 𝑧 ∈ (N × N)) → ((2nd𝑧) ∈ 𝑏 → (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
7372com23 82 . . . . . . . . . . . . . . . . . . . . . 22 (((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) ∧ 𝑧 ∈ (N × N)) → (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
7473impd 440 . . . . . . . . . . . . . . . . . . . . 21 (((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) ∧ 𝑧 ∈ (N × N)) → ((⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) ∈ 𝑏) → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
7574rexlimdva 2906 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ∧ 𝑏𝑦) → (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) ∈ 𝑏) → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
7675ex 443 . . . . . . . . . . . . . . . . . . 19 (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → (𝑏𝑦 → (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) ∈ 𝑏) → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
7776com3r 83 . . . . . . . . . . . . . . . . . 18 (∃𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) ∈ 𝑏) → (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
7835, 77syl6bi 238 . . . . . . . . . . . . . . . . 17 ((𝑎N𝑏N) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) → (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))))
7978com13 84 . . . . . . . . . . . . . . . 16 (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → (¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) → ((𝑎N𝑏N) → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))))
80 mulcompi 9406 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)
81 enqbreq 9429 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎N𝑏N) ∧ (𝑎N𝑏N)) → (⟨𝑎, 𝑏⟩ ~Q𝑎, 𝑏⟩ ↔ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)))
8281anidms 666 . . . . . . . . . . . . . . . . . . . 20 ((𝑎N𝑏N) → (⟨𝑎, 𝑏⟩ ~Q𝑎, 𝑏⟩ ↔ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)))
8380, 82mpbiri 243 . . . . . . . . . . . . . . . . . . 19 ((𝑎N𝑏N) → ⟨𝑎, 𝑏⟩ ~Q𝑎, 𝑏⟩)
84 opelxpi 4912 . . . . . . . . . . . . . . . . . . . 20 ((𝑎N𝑏N) → ⟨𝑎, 𝑏⟩ ∈ (N × N))
85 breq1 4437 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ~Q 𝑧 ↔ ⟨𝑎, 𝑏⟩ ~Q 𝑧))
86 vex 3069 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎 ∈ V
8786, 5op2ndd 6881 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd𝑦) = 𝑏)
8887breq2d 4446 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd𝑧) <N (2nd𝑦) ↔ (2nd𝑧) <N 𝑏))
8988notbid 303 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → (¬ (2nd𝑧) <N (2nd𝑦) ↔ ¬ (2nd𝑧) <N 𝑏))
9085, 89imbi12d 329 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦)) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏)))
9190ralbidv 2864 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = ⟨𝑎, 𝑏⟩ → (∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦)) ↔ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏)))
92 df-nq 9422 . . . . . . . . . . . . . . . . . . . . . 22 Q = {𝑦 ∈ (N × N) ∣ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦))}
9391, 92elrab2 3222 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑎, 𝑏⟩ ∈ Q ↔ (⟨𝑎, 𝑏⟩ ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏)))
9493simplbi2 644 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑎, 𝑏⟩ ∈ (N × N) → (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) → ⟨𝑎, 𝑏⟩ ∈ Q))
9584, 94syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑎N𝑏N) → (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) → ⟨𝑎, 𝑏⟩ ∈ Q))
96 breq1 4437 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨𝑎, 𝑏⟩ → (𝑥 ~Q𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ ~Q𝑎, 𝑏⟩))
9796rspcev 3171 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑎, 𝑏⟩ ∈ Q ∧ ⟨𝑎, 𝑏⟩ ~Q𝑎, 𝑏⟩) → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)
9897expcom 444 . . . . . . . . . . . . . . . . . . 19 (⟨𝑎, 𝑏⟩ ~Q𝑎, 𝑏⟩ → (⟨𝑎, 𝑏⟩ ∈ Q → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
9983, 95, 98sylsyld 58 . . . . . . . . . . . . . . . . . 18 ((𝑎N𝑏N) → (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
10099com12 32 . . . . . . . . . . . . . . . . 17 (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) → ((𝑎N𝑏N) → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
101100a1dd 47 . . . . . . . . . . . . . . . 16 (∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) → ((𝑎N𝑏N) → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
10279, 101pm2.61d2 167 . . . . . . . . . . . . . . 15 (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → ((𝑎N𝑏N) → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
103102ralrimivv 2848 . . . . . . . . . . . . . 14 (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → ∀𝑎N𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
10424, 103sylbir 220 . . . . . . . . . . . . 13 (∀𝑚𝑦𝑎N𝑏N (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩) → ∀𝑎N𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
105104a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ On → (∀𝑚𝑦𝑎N𝑏N (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩) → ∀𝑎N𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
10613, 105tfis2 6760 . . . . . . . . . . 11 (𝑦 ∈ On → ∀𝑎N𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
107 rsp 2808 . . . . . . . . . . 11 (∀𝑎N𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩) → (𝑎N → ∀𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
108106, 107syl 17 . . . . . . . . . 10 (𝑦 ∈ On → (𝑎N → ∀𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
109 rsp 2808 . . . . . . . . . 10 (∀𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩) → (𝑏N → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
110108, 109syl6 34 . . . . . . . . 9 (𝑦 ∈ On → (𝑎N → (𝑏N → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))))
111110impd 440 . . . . . . . 8 (𝑦 ∈ On → ((𝑎N𝑏N) → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
112111com12 32 . . . . . . 7 ((𝑎N𝑏N) → (𝑦 ∈ On → (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
113112rexlimdv 2905 . . . . . 6 ((𝑎N𝑏N) → (∃𝑦 ∈ On 𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
11410, 113mpd 15 . . . . 5 ((𝑎N𝑏N) → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)
115 breq2 4438 . . . . . 6 (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑥 ~Q 𝐴𝑥 ~Q𝑎, 𝑏⟩))
116115rexbidv 2927 . . . . 5 (𝐴 = ⟨𝑎, 𝑏⟩ → (∃𝑥Q 𝑥 ~Q 𝐴 ↔ ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
117114, 116syl5ibrcom 232 . . . 4 ((𝑎N𝑏N) → (𝐴 = ⟨𝑎, 𝑏⟩ → ∃𝑥Q 𝑥 ~Q 𝐴))
118117rexlimivv 2911 . . 3 (∃𝑎N𝑏N 𝐴 = ⟨𝑎, 𝑏⟩ → ∃𝑥Q 𝑥 ~Q 𝐴)
1191, 118sylbi 202 . 2 (𝐴 ∈ (N × N) → ∃𝑥Q 𝑥 ~Q 𝐴)
120 breq2 4438 . . . . . 6 (𝑎 = 𝐴 → (𝑥 ~Q 𝑎𝑥 ~Q 𝐴))
121 breq2 4438 . . . . . 6 (𝑎 = 𝐴 → (𝑦 ~Q 𝑎𝑦 ~Q 𝐴))
122120, 121anbi12d 734 . . . . 5 (𝑎 = 𝐴 → ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) ↔ (𝑥 ~Q 𝐴𝑦 ~Q 𝐴)))
123122imbi1d 326 . . . 4 (𝑎 = 𝐴 → (((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ((𝑥 ~Q 𝐴𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
1241232ralbidv 2867 . . 3 (𝑎 = 𝐴 → (∀𝑥Q𝑦Q ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ∀𝑥Q𝑦Q ((𝑥 ~Q 𝐴𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
12564a1i 11 . . . . . 6 ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → ~Q Er (N × N))
126 simpl 466 . . . . . 6 ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑎)
127 simpr 470 . . . . . 6 ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑦 ~Q 𝑎)
128125, 126, 127ertr4d 7459 . . . . 5 ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑦)
129 mulcompi 9406 . . . . . . . . . . 11 ((2nd𝑥) ·N (1st𝑥)) = ((1st𝑥) ·N (2nd𝑥))
130 elpqn 9435 . . . . . . . . . . . . . . 15 (𝑦Q𝑦 ∈ (N × N))
131 breq1 4437 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → (𝑦 ~Q 𝑧𝑥 ~Q 𝑧))
132 fveq2 5927 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → (2nd𝑦) = (2nd𝑥))
133132breq2d 4446 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑥 → ((2nd𝑧) <N (2nd𝑦) ↔ (2nd𝑧) <N (2nd𝑥)))
134133notbid 303 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → (¬ (2nd𝑧) <N (2nd𝑦) ↔ ¬ (2nd𝑧) <N (2nd𝑥)))
135131, 134imbi12d 329 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑥 → ((𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦)) ↔ (𝑥 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑥))))
136135ralbidv 2864 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑥 → (∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦)) ↔ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑥))))
137136, 92elrab2 3222 . . . . . . . . . . . . . . . 16 (𝑥Q ↔ (𝑥 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑥))))
138137simprbi 473 . . . . . . . . . . . . . . 15 (𝑥Q → ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑥)))
139 breq2 4438 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑦 → (𝑥 ~Q 𝑧𝑥 ~Q 𝑦))
140 fveq2 5927 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑦 → (2nd𝑧) = (2nd𝑦))
141140breq1d 4444 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → ((2nd𝑧) <N (2nd𝑥) ↔ (2nd𝑦) <N (2nd𝑥)))
142141notbid 303 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑦 → (¬ (2nd𝑧) <N (2nd𝑥) ↔ ¬ (2nd𝑦) <N (2nd𝑥)))
143139, 142imbi12d 329 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → ((𝑥 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑥)) ↔ (𝑥 ~Q 𝑦 → ¬ (2nd𝑦) <N (2nd𝑥))))
144143rspcva 3169 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑥))) → (𝑥 ~Q 𝑦 → ¬ (2nd𝑦) <N (2nd𝑥)))
145130, 138, 144syl2anr 488 . . . . . . . . . . . . . 14 ((𝑥Q𝑦Q) → (𝑥 ~Q 𝑦 → ¬ (2nd𝑦) <N (2nd𝑥)))
146145imp 438 . . . . . . . . . . . . 13 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → ¬ (2nd𝑦) <N (2nd𝑥))
14764a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ~Q 𝑦 → ~Q Er (N × N))
148 id 22 . . . . . . . . . . . . . . . . . 18 (𝑥 ~Q 𝑦𝑥 ~Q 𝑦)
149147, 148ersym 7452 . . . . . . . . . . . . . . . . 17 (𝑥 ~Q 𝑦𝑦 ~Q 𝑥)
150 elpqn 9435 . . . . . . . . . . . . . . . . . 18 (𝑥Q𝑥 ∈ (N × N))
15192rabeq2i 3063 . . . . . . . . . . . . . . . . . . 19 (𝑦Q ↔ (𝑦 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦))))
152151simprbi 473 . . . . . . . . . . . . . . . . . 18 (𝑦Q → ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦)))
153 breq2 4438 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (𝑦 ~Q 𝑧𝑦 ~Q 𝑥))
154 fveq2 5927 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑥 → (2nd𝑧) = (2nd𝑥))
155154breq1d 4444 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑥 → ((2nd𝑧) <N (2nd𝑦) ↔ (2nd𝑥) <N (2nd𝑦)))
156155notbid 303 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (¬ (2nd𝑧) <N (2nd𝑦) ↔ ¬ (2nd𝑥) <N (2nd𝑦)))
157153, 156imbi12d 329 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑥 → ((𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦)) ↔ (𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦))))
158157rspcva 3169 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦))) → (𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦)))
159150, 152, 158syl2an 487 . . . . . . . . . . . . . . . . 17 ((𝑥Q𝑦Q) → (𝑦 ~Q 𝑥 → ¬ (2nd𝑥) <N (2nd𝑦)))
160149, 159syl5 33 . . . . . . . . . . . . . . . 16 ((𝑥Q𝑦Q) → (𝑥 ~Q 𝑦 → ¬ (2nd𝑥) <N (2nd𝑦)))
161160imp 438 . . . . . . . . . . . . . . 15 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → ¬ (2nd𝑥) <N (2nd𝑦))
162 xp2nd 6901 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (N × N) → (2nd𝑥) ∈ N)
163150, 162syl 17 . . . . . . . . . . . . . . . . 17 (𝑥Q → (2nd𝑥) ∈ N)
164163ad2antrr 749 . . . . . . . . . . . . . . . 16 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → (2nd𝑥) ∈ N)
165 xp2nd 6901 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (N × N) → (2nd𝑦) ∈ N)
166130, 165syl 17 . . . . . . . . . . . . . . . . 17 (𝑦Q → (2nd𝑦) ∈ N)
167166ad2antlr 750 . . . . . . . . . . . . . . . 16 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → (2nd𝑦) ∈ N)
168 ltsopi 9398 . . . . . . . . . . . . . . . . . . 19 <N Or N
169 sotric 4827 . . . . . . . . . . . . . . . . . . 19 (( <N Or N ∧ ((2nd𝑥) ∈ N ∧ (2nd𝑦) ∈ N)) → ((2nd𝑥) <N (2nd𝑦) ↔ ¬ ((2nd𝑥) = (2nd𝑦) ∨ (2nd𝑦) <N (2nd𝑥))))
170168, 169mpan 693 . . . . . . . . . . . . . . . . . 18 (((2nd𝑥) ∈ N ∧ (2nd𝑦) ∈ N) → ((2nd𝑥) <N (2nd𝑦) ↔ ¬ ((2nd𝑥) = (2nd𝑦) ∨ (2nd𝑦) <N (2nd𝑥))))
171170notbid 303 . . . . . . . . . . . . . . . . 17 (((2nd𝑥) ∈ N ∧ (2nd𝑦) ∈ N) → (¬ (2nd𝑥) <N (2nd𝑦) ↔ ¬ ¬ ((2nd𝑥) = (2nd𝑦) ∨ (2nd𝑦) <N (2nd𝑥))))
172 notnotb 299 . . . . . . . . . . . . . . . . 17 (((2nd𝑥) = (2nd𝑦) ∨ (2nd𝑦) <N (2nd𝑥)) ↔ ¬ ¬ ((2nd𝑥) = (2nd𝑦) ∨ (2nd𝑦) <N (2nd𝑥)))
173171, 172syl6bbr 273 . . . . . . . . . . . . . . . 16 (((2nd𝑥) ∈ N ∧ (2nd𝑦) ∈ N) → (¬ (2nd𝑥) <N (2nd𝑦) ↔ ((2nd𝑥) = (2nd𝑦) ∨ (2nd𝑦) <N (2nd𝑥))))
174164, 167, 173syl2anc 682 . . . . . . . . . . . . . . 15 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → (¬ (2nd𝑥) <N (2nd𝑦) ↔ ((2nd𝑥) = (2nd𝑦) ∨ (2nd𝑦) <N (2nd𝑥))))
175161, 174mpbid 217 . . . . . . . . . . . . . 14 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → ((2nd𝑥) = (2nd𝑦) ∨ (2nd𝑦) <N (2nd𝑥)))
176175ord 386 . . . . . . . . . . . . 13 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → (¬ (2nd𝑥) = (2nd𝑦) → (2nd𝑦) <N (2nd𝑥)))
177146, 176mt3d 132 . . . . . . . . . . . 12 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → (2nd𝑥) = (2nd𝑦))
178177oveq2d 6379 . . . . . . . . . . 11 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → ((1st𝑥) ·N (2nd𝑥)) = ((1st𝑥) ·N (2nd𝑦)))
179129, 178syl5eq 2551 . . . . . . . . . 10 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → ((2nd𝑥) ·N (1st𝑥)) = ((1st𝑥) ·N (2nd𝑦)))
180 1st2nd2 6907 . . . . . . . . . . . . . 14 (𝑥 ∈ (N × N) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
181 1st2nd2 6907 . . . . . . . . . . . . . 14 (𝑦 ∈ (N × N) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
182180, 181breqan12d 4450 . . . . . . . . . . . . 13 ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ~Q ⟨(1st𝑦), (2nd𝑦)⟩))
183 xp1st 6900 . . . . . . . . . . . . . . 15 (𝑥 ∈ (N × N) → (1st𝑥) ∈ N)
184183, 162jca 547 . . . . . . . . . . . . . 14 (𝑥 ∈ (N × N) → ((1st𝑥) ∈ N ∧ (2nd𝑥) ∈ N))
185 xp1st 6900 . . . . . . . . . . . . . . 15 (𝑦 ∈ (N × N) → (1st𝑦) ∈ N)
186185, 165jca 547 . . . . . . . . . . . . . 14 (𝑦 ∈ (N × N) → ((1st𝑦) ∈ N ∧ (2nd𝑦) ∈ N))
187 enqbreq 9429 . . . . . . . . . . . . . 14 ((((1st𝑥) ∈ N ∧ (2nd𝑥) ∈ N) ∧ ((1st𝑦) ∈ N ∧ (2nd𝑦) ∈ N)) → (⟨(1st𝑥), (2nd𝑥)⟩ ~Q ⟨(1st𝑦), (2nd𝑦)⟩ ↔ ((1st𝑥) ·N (2nd𝑦)) = ((2nd𝑥) ·N (1st𝑦))))
188184, 186, 187syl2an 487 . . . . . . . . . . . . 13 ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (⟨(1st𝑥), (2nd𝑥)⟩ ~Q ⟨(1st𝑦), (2nd𝑦)⟩ ↔ ((1st𝑥) ·N (2nd𝑦)) = ((2nd𝑥) ·N (1st𝑦))))
189182, 188bitrd 263 . . . . . . . . . . . 12 ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ((1st𝑥) ·N (2nd𝑦)) = ((2nd𝑥) ·N (1st𝑦))))
190150, 130, 189syl2an 487 . . . . . . . . . . 11 ((𝑥Q𝑦Q) → (𝑥 ~Q 𝑦 ↔ ((1st𝑥) ·N (2nd𝑦)) = ((2nd𝑥) ·N (1st𝑦))))
191190biimpa 494 . . . . . . . . . 10 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → ((1st𝑥) ·N (2nd𝑦)) = ((2nd𝑥) ·N (1st𝑦)))
192179, 191eqtrd 2539 . . . . . . . . 9 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → ((2nd𝑥) ·N (1st𝑥)) = ((2nd𝑥) ·N (1st𝑦)))
193150ad2antrr 749 . . . . . . . . . 10 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 ∈ (N × N))
194 mulcanpi 9410 . . . . . . . . . . 11 (((2nd𝑥) ∈ N ∧ (1st𝑥) ∈ N) → (((2nd𝑥) ·N (1st𝑥)) = ((2nd𝑥) ·N (1st𝑦)) ↔ (1st𝑥) = (1st𝑦)))
195162, 183, 194syl2anc 682 . . . . . . . . . 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 217 . . . . . . . 8 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → (1st𝑥) = (1st𝑦))
198197, 177opeq12d 4204 . . . . . . 7 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → ⟨(1st𝑥), (2nd𝑥)⟩ = ⟨(1st𝑦), (2nd𝑦)⟩)
199193, 180syl 17 . . . . . . 7 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
200130ad2antlr 750 . . . . . . . 8 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → 𝑦 ∈ (N × N))
201200, 181syl 17 . . . . . . 7 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
202198, 199, 2013eqtr4d 2549 . . . . . 6 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → 𝑥 = 𝑦)
203202ex 443 . . . . 5 ((𝑥Q𝑦Q) → (𝑥 ~Q 𝑦𝑥 = 𝑦))
204128, 203syl5 33 . . . 4 ((𝑥Q𝑦Q) → ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑥 = 𝑦))
205204rgen2a 2855 . . 3 𝑥Q𝑦Q ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑥 = 𝑦)
206124, 205vtoclg 3128 . 2 (𝐴 ∈ (N × N) → ∀𝑥Q𝑦Q ((𝑥 ~Q 𝐴𝑦 ~Q 𝐴) → 𝑥 = 𝑦))
207 breq1 4437 . . 3 (𝑥 = 𝑦 → (𝑥 ~Q 𝐴𝑦 ~Q 𝐴))
208207reu4 3256 . 2 (∃!𝑥Q 𝑥 ~Q 𝐴 ↔ (∃𝑥Q 𝑥 ~Q 𝐴 ∧ ∀𝑥Q𝑦Q ((𝑥 ~Q 𝐴𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
209119, 206, 208sylanbrc 686 1 (𝐴 ∈ (N × N) → ∃!𝑥Q 𝑥 ~Q 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 191  wo 377  wa 378  w3a 1021   = wceq 1468  wcel 1937  wral 2791  wrex 2792  ∃!wreu 2793  cop 4001   class class class wbr 4434   Or wor 4800   × cxp 4878  Oncon0 5474  suc csuc 5476  cfv 5633  (class class class)co 6363  1st c1st 6868  2nd c2nd 6869   Er wer 7437  Ncnpi 9354   ·N cmi 9356   <N clti 9357   ~Q ceq 9361  Qcnq 9362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pow 4619  ax-pr 4680  ax-un 6659
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3068  df-sbc 3292  df-csb 3386  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-tp 4000  df-op 4002  df-uni 4229  df-iun 4309  df-br 4435  df-opab 4494  df-mpt 4495  df-tr 4531  df-eprel 4791  df-id 4795  df-po 4801  df-so 4802  df-fr 4839  df-we 4841  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-pred 5431  df-ord 5477  df-on 5478  df-lim 5479  df-suc 5480  df-iota 5597  df-fun 5635  df-fn 5636  df-f 5637  df-f1 5638  df-fo 5639  df-f1o 5640  df-fv 5641  df-ov 6366  df-oprab 6367  df-mpt2 6368  df-om 6770  df-1st 6870  df-2nd 6871  df-wrecs 7105  df-recs 7167  df-rdg 7205  df-oadd 7263  df-omul 7264  df-er 7440  df-ni 9382  df-mi 9384  df-lti 9385  df-enq 9421  df-nq 9422
This theorem is referenced by:  nqerf  9440  enqeq  9444
  Copyright terms: Public domain W3C validator