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

Theorem nqereu 9711
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 5102 . . 3 (𝐴 ∈ (N × N) ↔ ∃𝑎N𝑏N 𝐴 = ⟨𝑎, 𝑏⟩)
2 pion 9661 . . . . . . . . 9 (𝑏N𝑏 ∈ On)
3 suceloni 6975 . . . . . . . . 9 (𝑏 ∈ On → suc 𝑏 ∈ On)
42, 3syl 17 . . . . . . . 8 (𝑏N → suc 𝑏 ∈ On)
5 vex 3193 . . . . . . . . 9 𝑏 ∈ V
65sucid 5773 . . . . . . . 8 𝑏 ∈ suc 𝑏
7 eleq2 2687 . . . . . . . . 9 (𝑦 = suc 𝑏 → (𝑏𝑦𝑏 ∈ suc 𝑏))
87rspcev 3299 . . . . . . . 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 2985 . . . . . . . . . . . 12 (𝑦 = 𝑚 → (∀𝑎N𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩) ↔ ∀𝑎N𝑏N (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
14 opeq1 4377 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑎 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑑⟩)
1514breq2d 4635 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑎 → (𝑥 ~Q𝑐, 𝑑⟩ ↔ 𝑥 ~Q𝑎, 𝑑⟩))
1615rexbidv 3047 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑎 → (∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩ ↔ ∃𝑥Q 𝑥 ~Q𝑎, 𝑑⟩))
1716imbi2d 330 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑎 → ((𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑑⟩)))
18 elequ1 1994 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 → (𝑑𝑚𝑏𝑚))
19 opeq2 4378 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑏 → ⟨𝑎, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
2019breq2d 4635 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑏 → (𝑥 ~Q𝑎, 𝑑⟩ ↔ 𝑥 ~Q𝑎, 𝑏⟩))
2120rexbidv 3047 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑏 → (∃𝑥Q 𝑥 ~Q𝑎, 𝑑⟩ ↔ ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
2218, 21imbi12d 334 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑏 → ((𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑑⟩) ↔ (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
2317, 22cbvral2v 3171 . . . . . . . . . . . . . . 15 (∀𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ ∀𝑎N𝑏N (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
2423ralbii 2976 . . . . . . . . . . . . . 14 (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ ∀𝑚𝑦𝑎N𝑏N (𝑏𝑚 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
25 rexnal 2991 . . . . . . . . . . . . . . . . . . 19 (∃𝑧 ∈ (N × N) ¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) ↔ ¬ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏))
26 pm4.63 437 . . . . . . . . . . . . . . . . . . . . 21 (¬ (⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏) ↔ (⟨𝑎, 𝑏⟩ ~Q 𝑧 ∧ (2nd𝑧) <N 𝑏))
27 xp2nd 7159 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ (N × N) → (2nd𝑧) ∈ N)
28 ltpiord 9669 . . . . . . . . . . . . . . . . . . . . . . . . 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 3044 . . . . . . . . . . . . . . . . . . 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 7158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ (N × N) → (1st𝑧) ∈ N)
37 elequ2 2001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑚 = 𝑏 → (𝑑𝑚𝑑𝑏))
3837imbi1d 331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 = 𝑏 → ((𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩)))
39382ralbidv 2985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚 = 𝑏 → (∀𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ ∀𝑐N𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩)))
4039rspccv 3296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑚𝑦𝑐N𝑑N (𝑑𝑚 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → (𝑏𝑦 → ∀𝑐N𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩)))
41 opeq1 4377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑐 = (1st𝑧) → ⟨𝑐, 𝑑⟩ = ⟨(1st𝑧), 𝑑⟩)
4241breq2d 4635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑐 = (1st𝑧) → (𝑥 ~Q𝑐, 𝑑⟩ ↔ 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩))
4342rexbidv 3047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑐 = (1st𝑧) → (∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩ ↔ ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩))
4443imbi2d 330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑐 = (1st𝑧) → ((𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩)))
4544ralbidv 2982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = (1st𝑧) → (∀𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) ↔ ∀𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩)))
4645rspccv 3296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∀𝑐N𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q𝑐, 𝑑⟩) → ((1st𝑧) ∈ N → ∀𝑑N (𝑑𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩)))
47 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑑 = (2nd𝑧) → (𝑑𝑏 ↔ (2nd𝑧) ∈ 𝑏))
48 opeq2 4378 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑑 = (2nd𝑧) → ⟨(1st𝑧), 𝑑⟩ = ⟨(1st𝑧), (2nd𝑧)⟩)
4948breq2d 4635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑑 = (2nd𝑧) → (𝑥 ~Q ⟨(1st𝑧), 𝑑⟩ ↔ 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))
5049rexbidv 3047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑑 = (2nd𝑧) → (∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩ ↔ ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))
5147, 50imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑑 = (2nd𝑧) → ((𝑑𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), 𝑑⟩) ↔ ((2nd𝑧) ∈ 𝑏 → ∃𝑥Q 𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩)))
5251rspccv 3296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 ∈ (N × N) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
6059breq2d 4635 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 ∈ (N × N) → (𝑥 ~Q 𝑧𝑥 ~Q ⟨(1st𝑧), (2nd𝑧)⟩))
6160rexbidv 3047 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7721 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⟨𝑎, 𝑏⟩ ~Q 𝑧𝑥 ~Q 𝑧) → 𝑥 ~Q𝑎, 𝑏⟩)
6968ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (⟨𝑎, 𝑏⟩ ~Q 𝑧 → (𝑥 ~Q 𝑧𝑥 ~Q𝑎, 𝑏⟩))
7069reximdv 3012 . . . . . . . . . . . . . . . . . . . . . . . . 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 3026 . . . . . . . . . . . . . . . . . . . 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 9678 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎)
81 enqbreq 9701 . . . . . . . . . . . . . . . . . . . . 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 5118 . . . . . . . . . . . . . . . . . . . 20 ((𝑎N𝑏N) → ⟨𝑎, 𝑏⟩ ∈ (N × N))
85 breq1 4626 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ~Q 𝑧 ↔ ⟨𝑎, 𝑏⟩ ~Q 𝑧))
86 vex 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎 ∈ V
8786, 5op2ndd 7139 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd𝑦) = 𝑏)
8887breq2d 4635 . . . . . . . . . . . . . . . . . . . . . . . . 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 2982 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = ⟨𝑎, 𝑏⟩ → (∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦)) ↔ ∀𝑧 ∈ (N × N)(⟨𝑎, 𝑏⟩ ~Q 𝑧 → ¬ (2nd𝑧) <N 𝑏)))
92 df-nq 9694 . . . . . . . . . . . . . . . . . . . . . 22 Q = {𝑦 ∈ (N × N) ∣ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦))}
9391, 92elrab2 3353 . . . . . . . . . . . . . . . . . . . . 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 4626 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = ⟨𝑎, 𝑏⟩ → (𝑥 ~Q𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ ~Q𝑎, 𝑏⟩))
9796rspcev 3299 . . . . . . . . . . . . . . . . . . . 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 2966 . . . . . . . . . . . . . 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 7018 . . . . . . . . . . 11 (𝑦 ∈ On → ∀𝑎N𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
107 rsp 2925 . . . . . . . . . . 11 (∀𝑎N𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩) → (𝑎N → ∀𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
108106, 107syl 17 . . . . . . . . . 10 (𝑦 ∈ On → (𝑎N → ∀𝑏N (𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)))
109 rsp 2925 . . . . . . . . . 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 3025 . . . . . 6 ((𝑎N𝑏N) → (∃𝑦 ∈ On 𝑏𝑦 → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
11410, 113mpd 15 . . . . 5 ((𝑎N𝑏N) → ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩)
115 breq2 4627 . . . . . 6 (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑥 ~Q 𝐴𝑥 ~Q𝑎, 𝑏⟩))
116115rexbidv 3047 . . . . 5 (𝐴 = ⟨𝑎, 𝑏⟩ → (∃𝑥Q 𝑥 ~Q 𝐴 ↔ ∃𝑥Q 𝑥 ~Q𝑎, 𝑏⟩))
117114, 116syl5ibrcom 237 . . . 4 ((𝑎N𝑏N) → (𝐴 = ⟨𝑎, 𝑏⟩ → ∃𝑥Q 𝑥 ~Q 𝐴))
118117rexlimivv 3031 . . 3 (∃𝑎N𝑏N 𝐴 = ⟨𝑎, 𝑏⟩ → ∃𝑥Q 𝑥 ~Q 𝐴)
1191, 118sylbi 207 . 2 (𝐴 ∈ (N × N) → ∃𝑥Q 𝑥 ~Q 𝐴)
120 breq2 4627 . . . . . 6 (𝑎 = 𝐴 → (𝑥 ~Q 𝑎𝑥 ~Q 𝐴))
121 breq2 4627 . . . . . 6 (𝑎 = 𝐴 → (𝑦 ~Q 𝑎𝑦 ~Q 𝐴))
122120, 121anbi12d 746 . . . . 5 (𝑎 = 𝐴 → ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) ↔ (𝑥 ~Q 𝐴𝑦 ~Q 𝐴)))
123122imbi1d 331 . . . 4 (𝑎 = 𝐴 → (((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ((𝑥 ~Q 𝐴𝑦 ~Q 𝐴) → 𝑥 = 𝑦)))
1241232ralbidv 2985 . . 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 7721 . . . . 5 ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑦)
129 mulcompi 9678 . . . . . . . . . . 11 ((2nd𝑥) ·N (1st𝑥)) = ((1st𝑥) ·N (2nd𝑥))
130 elpqn 9707 . . . . . . . . . . . . . . 15 (𝑦Q𝑦 ∈ (N × N))
131 breq1 4626 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑥 → (𝑦 ~Q 𝑧𝑥 ~Q 𝑧))
132 fveq2 6158 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑥 → (2nd𝑦) = (2nd𝑥))
133132breq2d 4635 . . . . . . . . . . . . . . . . . . . 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 2982 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑥 → (∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦)) ↔ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑥))))
137136, 92elrab2 3353 . . . . . . . . . . . . . . . 16 (𝑥Q ↔ (𝑥 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑥))))
138137simprbi 480 . . . . . . . . . . . . . . 15 (𝑥Q → ∀𝑧 ∈ (N × N)(𝑥 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑥)))
139 breq2 4627 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑦 → (𝑥 ~Q 𝑧𝑥 ~Q 𝑦))
140 fveq2 6158 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑦 → (2nd𝑧) = (2nd𝑦))
141140breq1d 4633 . . . . . . . . . . . . . . . . . 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 3297 . . . . . . . . . . . . . . 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 7714 . . . . . . . . . . . . . . . . 17 (𝑥 ~Q 𝑦𝑦 ~Q 𝑥)
150 elpqn 9707 . . . . . . . . . . . . . . . . . 18 (𝑥Q𝑥 ∈ (N × N))
15192rabeq2i 3187 . . . . . . . . . . . . . . . . . . 19 (𝑦Q ↔ (𝑦 ∈ (N × N) ∧ ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦))))
152151simprbi 480 . . . . . . . . . . . . . . . . . 18 (𝑦Q → ∀𝑧 ∈ (N × N)(𝑦 ~Q 𝑧 → ¬ (2nd𝑧) <N (2nd𝑦)))
153 breq2 4627 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (𝑦 ~Q 𝑧𝑦 ~Q 𝑥))
154 fveq2 6158 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑥 → (2nd𝑧) = (2nd𝑥))
155154breq1d 4633 . . . . . . . . . . . . . . . . . . . . 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 3297 . . . . . . . . . . . . . . . . . 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 7159 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (N × N) → (2nd𝑥) ∈ N)
163150, 162syl 17 . . . . . . . . . . . . . . . . 17 (𝑥Q → (2nd𝑥) ∈ N)
164163ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → (2nd𝑥) ∈ N)
165 xp2nd 7159 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (N × N) → (2nd𝑦) ∈ N)
166130, 165syl 17 . . . . . . . . . . . . . . . . 17 (𝑦Q → (2nd𝑦) ∈ N)
167166ad2antlr 762 . . . . . . . . . . . . . . . 16 (((𝑥Q𝑦Q) ∧ 𝑥 ~Q 𝑦) → (2nd𝑦) ∈ N)
168 ltsopi 9670 . . . . . . . . . . . . . . . . . . 19 <N Or N
169 sotric 5031 . . . . . . . . . . . . . . . . . . 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 6631 . . . . . . . . . . 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 7165 . . . . . . . . . . . . . 14 (𝑥 ∈ (N × N) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
181 1st2nd2 7165 . . . . . . . . . . . . . 14 (𝑦 ∈ (N × N) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
182180, 181breqan12d 4639 . . . . . . . . . . . . 13 ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ~Q ⟨(1st𝑦), (2nd𝑦)⟩))
183 xp1st 7158 . . . . . . . . . . . . . . 15 (𝑥 ∈ (N × N) → (1st𝑥) ∈ N)
184183, 162jca 554 . . . . . . . . . . . . . 14 (𝑥 ∈ (N × N) → ((1st𝑥) ∈ N ∧ (2nd𝑥) ∈ N))
185 xp1st 7158 . . . . . . . . . . . . . . 15 (𝑦 ∈ (N × N) → (1st𝑦) ∈ N)
186185, 165jca 554 . . . . . . . . . . . . . 14 (𝑦 ∈ (N × N) → ((1st𝑦) ∈ N ∧ (2nd𝑦) ∈ N))
187 enqbreq 9701 . . . . . . . . . . . . . 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 9682 . . . . . . . . . . 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 4385 . . . . . . 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 2973 . . 3 𝑥Q𝑦Q ((𝑥 ~Q 𝑎𝑦 ~Q 𝑎) → 𝑥 = 𝑦)
206124, 205vtoclg 3256 . 2 (𝐴 ∈ (N × N) → ∀𝑥Q𝑦Q ((𝑥 ~Q 𝐴𝑦 ~Q 𝐴) → 𝑥 = 𝑦))
207 breq1 4626 . . 3 (𝑥 = 𝑦 → (𝑥 ~Q 𝐴𝑦 ~Q 𝐴))
208207reu4 3387 . 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 2908  wrex 2909  ∃!wreu 2910  cop 4161   class class class wbr 4623   Or wor 5004   × cxp 5082  Oncon0 5692  suc csuc 5694  cfv 5857  (class class class)co 6615  1st c1st 7126  2nd c2nd 7127   Er wer 7699  Ncnpi 9626   ·N cmi 9628   <N clti 9629   ~Q ceq 9633  Qcnq 9634
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 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914
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 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-oadd 7524  df-omul 7525  df-er 7702  df-ni 9654  df-mi 9656  df-lti 9657  df-enq 9693  df-nq 9694
This theorem is referenced by:  nqerf  9712  enqeq  9716
  Copyright terms: Public domain W3C validator