Step | Hyp | Ref
| Expression |
1 | | elxp2 5132 |
. . 3
⊢ (𝐴 ∈ (N ×
N) ↔ ∃𝑎 ∈ N ∃𝑏 ∈ N 𝐴 = 〈𝑎, 𝑏〉) |
2 | | pion 9701 |
. . . . . . . . 9
⊢ (𝑏 ∈ N →
𝑏 ∈
On) |
3 | | suceloni 7013 |
. . . . . . . . 9
⊢ (𝑏 ∈ On → suc 𝑏 ∈ On) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
⊢ (𝑏 ∈ N →
suc 𝑏 ∈
On) |
5 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
6 | 5 | sucid 5804 |
. . . . . . . 8
⊢ 𝑏 ∈ suc 𝑏 |
7 | | eleq2 2690 |
. . . . . . . . 9
⊢ (𝑦 = suc 𝑏 → (𝑏 ∈ 𝑦 ↔ 𝑏 ∈ suc 𝑏)) |
8 | 7 | rspcev 3309 |
. . . . . . . 8
⊢ ((suc
𝑏 ∈ On ∧ 𝑏 ∈ suc 𝑏) → ∃𝑦 ∈ On 𝑏 ∈ 𝑦) |
9 | 4, 6, 8 | sylancl 694 |
. . . . . . 7
⊢ (𝑏 ∈ N →
∃𝑦 ∈ On 𝑏 ∈ 𝑦) |
10 | 9 | adantl 482 |
. . . . . 6
⊢ ((𝑎 ∈ N ∧
𝑏 ∈ N)
→ ∃𝑦 ∈ On
𝑏 ∈ 𝑦) |
11 | | elequ2 2004 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑚 → (𝑏 ∈ 𝑦 ↔ 𝑏 ∈ 𝑚)) |
12 | 11 | imbi1d 331 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑚 → ((𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉) ↔ (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉))) |
13 | 12 | 2ralbidv 2989 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑚 → (∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉) ↔ ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉))) |
14 | | opeq1 4402 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = 𝑎 → 〈𝑐, 𝑑〉 = 〈𝑎, 𝑑〉) |
15 | 14 | breq2d 4665 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = 𝑎 → (𝑥 ~Q 〈𝑐, 𝑑〉 ↔ 𝑥 ~Q 〈𝑎, 𝑑〉)) |
16 | 15 | rexbidv 3052 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = 𝑎 → (∃𝑥 ∈ Q 𝑥 ~Q 〈𝑐, 𝑑〉 ↔ ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑑〉)) |
17 | 16 | imbi2d 330 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝑎 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑐, 𝑑〉) ↔ (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑑〉))) |
18 | | elequ1 1997 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = 𝑏 → (𝑑 ∈ 𝑚 ↔ 𝑏 ∈ 𝑚)) |
19 | | opeq2 4403 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 = 𝑏 → 〈𝑎, 𝑑〉 = 〈𝑎, 𝑏〉) |
20 | 19 | breq2d 4665 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = 𝑏 → (𝑥 ~Q 〈𝑎, 𝑑〉 ↔ 𝑥 ~Q 〈𝑎, 𝑏〉)) |
21 | 20 | rexbidv 3052 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = 𝑏 → (∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑑〉 ↔ ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉)) |
22 | 18, 21 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 𝑏 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑑〉) ↔ (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉))) |
23 | 17, 22 | cbvral2v 3179 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑐 ∈
N ∀𝑑
∈ N (𝑑
∈ 𝑚 →
∃𝑥 ∈
Q 𝑥
~Q 〈𝑐, 𝑑〉) ↔ ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉)) |
24 | 23 | ralbii 2980 |
. . . . . . . . . . . . . 14
⊢
(∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) ↔ ∀𝑚 ∈ 𝑦 ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉)) |
25 | | rexnal 2995 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑧 ∈
(N × N) ¬ (〈𝑎, 𝑏〉 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N 𝑏) ↔ ¬ ∀𝑧 ∈ (N ×
N)(〈𝑎,
𝑏〉
~Q 𝑧 → ¬ (2nd ‘𝑧) <N
𝑏)) |
26 | | pm4.63 437 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
(〈𝑎, 𝑏〉
~Q 𝑧 → ¬ (2nd ‘𝑧) <N
𝑏) ↔ (〈𝑎, 𝑏〉 ~Q 𝑧 ∧ (2nd
‘𝑧)
<N 𝑏)) |
27 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ (N ×
N) → (2nd ‘𝑧) ∈ N) |
28 | | ltpiord 9709 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((2nd ‘𝑧) ∈ N ∧ 𝑏 ∈ N) →
((2nd ‘𝑧)
<N 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏)) |
29 | 28 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑏 ∈ N ∧
(2nd ‘𝑧)
∈ N) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd
‘𝑧) ∈ 𝑏)) |
30 | 27, 29 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑏 ∈ N ∧
𝑧 ∈ (N
× N)) → ((2nd ‘𝑧) <N 𝑏 ↔ (2nd
‘𝑧) ∈ 𝑏)) |
31 | 30 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑎 ∈ N ∧
𝑏 ∈ N)
∧ 𝑧 ∈
(N × N)) → ((2nd ‘𝑧) <N
𝑏 ↔ (2nd
‘𝑧) ∈ 𝑏)) |
32 | 31 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ N ∧
𝑏 ∈ N)
∧ 𝑧 ∈
(N × N)) → ((〈𝑎, 𝑏〉 ~Q 𝑧 ∧ (2nd
‘𝑧)
<N 𝑏) ↔ (〈𝑎, 𝑏〉 ~Q 𝑧 ∧ (2nd
‘𝑧) ∈ 𝑏))) |
33 | 26, 32 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ N ∧
𝑏 ∈ N)
∧ 𝑧 ∈
(N × N)) → (¬ (〈𝑎, 𝑏〉 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N 𝑏) ↔ (〈𝑎, 𝑏〉 ~Q 𝑧 ∧ (2nd
‘𝑧) ∈ 𝑏))) |
34 | 33 | rexbidva 3049 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ N ∧
𝑏 ∈ N)
→ (∃𝑧 ∈
(N × N) ¬ (〈𝑎, 𝑏〉 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N 𝑏) ↔ ∃𝑧 ∈ (N ×
N)(〈𝑎,
𝑏〉
~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏))) |
35 | 25, 34 | syl5bbr 274 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ N ∧
𝑏 ∈ N)
→ (¬ ∀𝑧
∈ (N × N)(〈𝑎, 𝑏〉 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N 𝑏) ↔ ∃𝑧 ∈ (N ×
N)(〈𝑎,
𝑏〉
~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏))) |
36 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∈ (N ×
N) → (1st ‘𝑧) ∈ N) |
37 | | elequ2 2004 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑚 = 𝑏 → (𝑑 ∈ 𝑚 ↔ 𝑑 ∈ 𝑏)) |
38 | 37 | imbi1d 331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑚 = 𝑏 → ((𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑐, 𝑑〉) ↔ (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑐, 𝑑〉))) |
39 | 38 | 2ralbidv 2989 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑚 = 𝑏 → (∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑐, 𝑑〉) ↔ ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑐, 𝑑〉))) |
40 | 39 | rspccv 3306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) → (𝑏 ∈ 𝑦 → ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑐, 𝑑〉))) |
41 | | opeq1 4402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑐 = (1st ‘𝑧) → 〈𝑐, 𝑑〉 = 〈(1st ‘𝑧), 𝑑〉) |
42 | 41 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑐 = (1st ‘𝑧) → (𝑥 ~Q 〈𝑐, 𝑑〉 ↔ 𝑥 ~Q
〈(1st ‘𝑧), 𝑑〉)) |
43 | 42 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑐 = (1st ‘𝑧) → (∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉 ↔ ∃𝑥 ∈ Q 𝑥 ~Q
〈(1st ‘𝑧), 𝑑〉)) |
44 | 43 | imbi2d 330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑐 = (1st ‘𝑧) → ((𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑐, 𝑑〉) ↔ (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q
〈(1st ‘𝑧), 𝑑〉))) |
45 | 44 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑐 = (1st ‘𝑧) → (∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑐, 𝑑〉) ↔ ∀𝑑 ∈ N (𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q
〈(1st ‘𝑧), 𝑑〉))) |
46 | 45 | rspccv 3306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(∀𝑐 ∈
N ∀𝑑
∈ N (𝑑
∈ 𝑏 →
∃𝑥 ∈
Q 𝑥
~Q 〈𝑐, 𝑑〉) → ((1st ‘𝑧) ∈ N →
∀𝑑 ∈
N (𝑑 ∈
𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q
〈(1st ‘𝑧), 𝑑〉))) |
47 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑑 = (2nd ‘𝑧) → (𝑑 ∈ 𝑏 ↔ (2nd ‘𝑧) ∈ 𝑏)) |
48 | | opeq2 4403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑑 = (2nd ‘𝑧) → 〈(1st
‘𝑧), 𝑑〉 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
49 | 48 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑑 = (2nd ‘𝑧) → (𝑥 ~Q
〈(1st ‘𝑧), 𝑑〉 ↔ 𝑥 ~Q
〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
50 | 49 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑑 = (2nd ‘𝑧) → (∃𝑥 ∈ Q 𝑥 ~Q
〈(1st ‘𝑧), 𝑑〉 ↔ ∃𝑥 ∈ Q 𝑥 ~Q
〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
51 | 47, 50 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑑 = (2nd ‘𝑧) → ((𝑑 ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q
〈(1st ‘𝑧), 𝑑〉) ↔ ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q
〈(1st ‘𝑧), (2nd ‘𝑧)〉))) |
52 | 51 | rspccv 3306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(∀𝑑 ∈
N (𝑑 ∈
𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q
〈(1st ‘𝑧), 𝑑〉) → ((2nd ‘𝑧) ∈ N →
((2nd ‘𝑧)
∈ 𝑏 →
∃𝑥 ∈
Q 𝑥
~Q 〈(1st ‘𝑧), (2nd ‘𝑧)〉))) |
53 | 46, 52 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∀𝑐 ∈
N ∀𝑑
∈ N (𝑑
∈ 𝑏 →
∃𝑥 ∈
Q 𝑥
~Q 〈𝑐, 𝑑〉) → ((1st ‘𝑧) ∈ N →
((2nd ‘𝑧)
∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q
〈(1st ‘𝑧), (2nd ‘𝑧)〉)))) |
54 | 40, 53 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) → (𝑏 ∈ 𝑦 → ((1st ‘𝑧) ∈ N →
((2nd ‘𝑧)
∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q
〈(1st ‘𝑧), (2nd ‘𝑧)〉))))) |
55 | 54 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) ∧ 𝑏 ∈ 𝑦) → ((1st ‘𝑧) ∈ N →
((2nd ‘𝑧)
∈ N → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q
〈(1st ‘𝑧), (2nd ‘𝑧)〉)))) |
56 | 36, 55 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) ∧ 𝑏 ∈ 𝑦) → (𝑧 ∈ (N ×
N) → ((2nd ‘𝑧) ∈ N →
((2nd ‘𝑧)
∈ 𝑏 →
∃𝑥 ∈
Q 𝑥
~Q 〈(1st ‘𝑧), (2nd ‘𝑧)〉)))) |
57 | 27, 56 | mpdi 45 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) ∧ 𝑏 ∈ 𝑦) → (𝑧 ∈ (N ×
N) → ((2nd ‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q
〈(1st ‘𝑧), (2nd ‘𝑧)〉))) |
58 | 57 | 3imp 1256 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N ×
N) ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q
〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
59 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∈ (N ×
N) → 𝑧 =
〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
60 | 59 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 ∈ (N ×
N) → (𝑥
~Q 𝑧 ↔ 𝑥 ~Q
〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
61 | 60 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 ∈ (N ×
N) → (∃𝑥 ∈ Q 𝑥 ~Q 𝑧 ↔ ∃𝑥 ∈ Q 𝑥 ~Q
〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
62 | 61 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N ×
N) ∧ (2nd ‘𝑧) ∈ 𝑏) → (∃𝑥 ∈ Q 𝑥 ~Q 𝑧 ↔ ∃𝑥 ∈ Q 𝑥 ~Q
〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
63 | 58, 62 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N ×
N) ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q 𝑧) |
64 | | enqer 9743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
~Q Er (N ×
N) |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((〈𝑎, 𝑏〉
~Q 𝑧 ∧ 𝑥 ~Q 𝑧) →
~Q Er (N ×
N)) |
66 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((〈𝑎, 𝑏〉
~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → 𝑥 ~Q 𝑧) |
67 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((〈𝑎, 𝑏〉
~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → 〈𝑎, 𝑏〉 ~Q 𝑧) |
68 | 65, 66, 67 | ertr4d 7761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((〈𝑎, 𝑏〉
~Q 𝑧 ∧ 𝑥 ~Q 𝑧) → 𝑥 ~Q 〈𝑎, 𝑏〉) |
69 | 68 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(〈𝑎, 𝑏〉
~Q 𝑧 → (𝑥 ~Q 𝑧 → 𝑥 ~Q 〈𝑎, 𝑏〉)) |
70 | 69 | reximdv 3016 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(〈𝑎, 𝑏〉
~Q 𝑧 → (∃𝑥 ∈ Q 𝑥 ~Q 𝑧 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑎, 𝑏〉)) |
71 | 63, 70 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N ×
N) ∧ (2nd ‘𝑧) ∈ 𝑏) → (〈𝑎, 𝑏〉 ~Q 𝑧 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑎, 𝑏〉)) |
72 | 71 | 3expia 1267 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N ×
N)) → ((2nd ‘𝑧) ∈ 𝑏 → (〈𝑎, 𝑏〉 ~Q 𝑧 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑎, 𝑏〉))) |
73 | 72 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N ×
N)) → (〈𝑎, 𝑏〉 ~Q 𝑧 → ((2nd
‘𝑧) ∈ 𝑏 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑎, 𝑏〉))) |
74 | 73 | impd 447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) ∧ 𝑏 ∈ 𝑦) ∧ 𝑧 ∈ (N ×
N)) → ((〈𝑎, 𝑏〉 ~Q 𝑧 ∧ (2nd
‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑎, 𝑏〉)) |
75 | 74 | rexlimdva 3031 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) ∧ 𝑏 ∈ 𝑦) → (∃𝑧 ∈ (N ×
N)(〈𝑎,
𝑏〉
~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉)) |
76 | 75 | ex 450 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) → (𝑏 ∈ 𝑦 → (∃𝑧 ∈ (N ×
N)(〈𝑎,
𝑏〉
~Q 𝑧 ∧ (2nd ‘𝑧) ∈ 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉))) |
77 | 76 | com3r 87 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑧 ∈
(N × N)(〈𝑎, 𝑏〉 ~Q 𝑧 ∧ (2nd
‘𝑧) ∈ 𝑏) → (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑐, 𝑑〉) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉))) |
78 | 35, 77 | syl6bi 243 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ N ∧
𝑏 ∈ N)
→ (¬ ∀𝑧
∈ (N × N)(〈𝑎, 𝑏〉 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N 𝑏) → (∀𝑚 ∈ 𝑦 ∀𝑐 ∈ N ∀𝑑 ∈ N (𝑑 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑐, 𝑑〉) → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉)))) |
79 | 78 | com13 88 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) → (¬ ∀𝑧 ∈ (N ×
N)(〈𝑎,
𝑏〉
~Q 𝑧 → ¬ (2nd ‘𝑧) <N
𝑏) → ((𝑎 ∈ N ∧
𝑏 ∈ N)
→ (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑎, 𝑏〉)))) |
80 | | mulcompi 9718 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎
·N 𝑏) = (𝑏 ·N 𝑎) |
81 | | enqbreq 9741 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ N ∧
𝑏 ∈ N)
∧ (𝑎 ∈
N ∧ 𝑏
∈ N)) → (〈𝑎, 𝑏〉 ~Q
〈𝑎, 𝑏〉 ↔ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎))) |
82 | 81 | anidms 677 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ N ∧
𝑏 ∈ N)
→ (〈𝑎, 𝑏〉
~Q 〈𝑎, 𝑏〉 ↔ (𝑎 ·N 𝑏) = (𝑏 ·N 𝑎))) |
83 | 80, 82 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ N ∧
𝑏 ∈ N)
→ 〈𝑎, 𝑏〉
~Q 〈𝑎, 𝑏〉) |
84 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ N ∧
𝑏 ∈ N)
→ 〈𝑎, 𝑏〉 ∈ (N
× N)) |
85 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 〈𝑎, 𝑏〉 → (𝑦 ~Q 𝑧 ↔ 〈𝑎, 𝑏〉 ~Q 𝑧)) |
86 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑎 ∈ V |
87 | 86, 5 | op2ndd 7179 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 〈𝑎, 𝑏〉 → (2nd ‘𝑦) = 𝑏) |
88 | 87 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 〈𝑎, 𝑏〉 → ((2nd ‘𝑧) <N
(2nd ‘𝑦)
↔ (2nd ‘𝑧) <N 𝑏)) |
89 | 88 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 〈𝑎, 𝑏〉 → (¬ (2nd
‘𝑧)
<N (2nd ‘𝑦) ↔ ¬ (2nd ‘𝑧) <N
𝑏)) |
90 | 85, 89 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 〈𝑎, 𝑏〉 → ((𝑦 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N (2nd ‘𝑦)) ↔ (〈𝑎, 𝑏〉 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N 𝑏))) |
91 | 90 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 〈𝑎, 𝑏〉 → (∀𝑧 ∈ (N ×
N)(𝑦
~Q 𝑧 → ¬ (2nd ‘𝑧) <N
(2nd ‘𝑦))
↔ ∀𝑧 ∈
(N × N)(〈𝑎, 𝑏〉 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N 𝑏))) |
92 | | df-nq 9734 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Q = {𝑦
∈ (N × N) ∣ ∀𝑧 ∈ (N ×
N)(𝑦
~Q 𝑧 → ¬ (2nd ‘𝑧) <N
(2nd ‘𝑦))} |
93 | 91, 92 | elrab2 3366 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈𝑎, 𝑏〉 ∈ Q
↔ (〈𝑎, 𝑏〉 ∈ (N
× N) ∧ ∀𝑧 ∈ (N ×
N)(〈𝑎,
𝑏〉
~Q 𝑧 → ¬ (2nd ‘𝑧) <N
𝑏))) |
94 | 93 | simplbi2 655 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑎, 𝑏〉 ∈ (N
× N) → (∀𝑧 ∈ (N ×
N)(〈𝑎,
𝑏〉
~Q 𝑧 → ¬ (2nd ‘𝑧) <N
𝑏) → 〈𝑎, 𝑏〉 ∈
Q)) |
95 | 84, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ N ∧
𝑏 ∈ N)
→ (∀𝑧 ∈
(N × N)(〈𝑎, 𝑏〉 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N 𝑏) → 〈𝑎, 𝑏〉 ∈
Q)) |
96 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (𝑥 ~Q 〈𝑎, 𝑏〉 ↔ 〈𝑎, 𝑏〉 ~Q
〈𝑎, 𝑏〉)) |
97 | 96 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈𝑎, 𝑏〉 ∈ Q
∧ 〈𝑎, 𝑏〉
~Q 〈𝑎, 𝑏〉) → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉) |
98 | 97 | expcom 451 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑎, 𝑏〉
~Q 〈𝑎, 𝑏〉 → (〈𝑎, 𝑏〉 ∈ Q →
∃𝑥 ∈
Q 𝑥
~Q 〈𝑎, 𝑏〉)) |
99 | 83, 95, 98 | sylsyld 61 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ N ∧
𝑏 ∈ N)
→ (∀𝑧 ∈
(N × N)(〈𝑎, 𝑏〉 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N 𝑏) → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉)) |
100 | 99 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑧 ∈
(N × N)(〈𝑎, 𝑏〉 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N 𝑏) → ((𝑎 ∈ N ∧ 𝑏 ∈ N) →
∃𝑥 ∈
Q 𝑥
~Q 〈𝑎, 𝑏〉)) |
101 | 100 | a1dd 50 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑧 ∈
(N × N)(〈𝑎, 𝑏〉 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N 𝑏) → ((𝑎 ∈ N ∧ 𝑏 ∈ N) →
(𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑎, 𝑏〉))) |
102 | 79, 101 | pm2.61d2 172 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) → ((𝑎 ∈ N ∧ 𝑏 ∈ N) →
(𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑎, 𝑏〉))) |
103 | 102 | ralrimivv 2970 |
. . . . . . . . . . . . . 14
⊢
(∀𝑚 ∈
𝑦 ∀𝑐 ∈ N
∀𝑑 ∈
N (𝑑 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑐, 𝑑〉) → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉)) |
104 | 24, 103 | sylbir 225 |
. . . . . . . . . . . . 13
⊢
(∀𝑚 ∈
𝑦 ∀𝑎 ∈ N
∀𝑏 ∈
N (𝑏 ∈
𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑎, 𝑏〉) → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉)) |
105 | 104 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ On → (∀𝑚 ∈ 𝑦 ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑚 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉) → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉))) |
106 | 13, 105 | tfis2 7056 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ On → ∀𝑎 ∈ N
∀𝑏 ∈
N (𝑏 ∈
𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑎, 𝑏〉)) |
107 | | rsp 2929 |
. . . . . . . . . . 11
⊢
(∀𝑎 ∈
N ∀𝑏
∈ N (𝑏
∈ 𝑦 →
∃𝑥 ∈
Q 𝑥
~Q 〈𝑎, 𝑏〉) → (𝑎 ∈ N → ∀𝑏 ∈ N (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉))) |
108 | 106, 107 | syl 17 |
. . . . . . . . . 10
⊢ (𝑦 ∈ On → (𝑎 ∈ N →
∀𝑏 ∈
N (𝑏 ∈
𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑎, 𝑏〉))) |
109 | | rsp 2929 |
. . . . . . . . . 10
⊢
(∀𝑏 ∈
N (𝑏 ∈
𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑎, 𝑏〉) → (𝑏 ∈ N → (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉))) |
110 | 108, 109 | syl6 35 |
. . . . . . . . 9
⊢ (𝑦 ∈ On → (𝑎 ∈ N →
(𝑏 ∈ N
→ (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑎, 𝑏〉)))) |
111 | 110 | impd 447 |
. . . . . . . 8
⊢ (𝑦 ∈ On → ((𝑎 ∈ N ∧
𝑏 ∈ N)
→ (𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑎, 𝑏〉))) |
112 | 111 | com12 32 |
. . . . . . 7
⊢ ((𝑎 ∈ N ∧
𝑏 ∈ N)
→ (𝑦 ∈ On →
(𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑎, 𝑏〉))) |
113 | 112 | rexlimdv 3030 |
. . . . . 6
⊢ ((𝑎 ∈ N ∧
𝑏 ∈ N)
→ (∃𝑦 ∈ On
𝑏 ∈ 𝑦 → ∃𝑥 ∈ Q 𝑥 ~Q 〈𝑎, 𝑏〉)) |
114 | 10, 113 | mpd 15 |
. . . . 5
⊢ ((𝑎 ∈ N ∧
𝑏 ∈ N)
→ ∃𝑥 ∈
Q 𝑥
~Q 〈𝑎, 𝑏〉) |
115 | | breq2 4657 |
. . . . . 6
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (𝑥 ~Q 𝐴 ↔ 𝑥 ~Q 〈𝑎, 𝑏〉)) |
116 | 115 | rexbidv 3052 |
. . . . 5
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (∃𝑥 ∈ Q 𝑥 ~Q 𝐴 ↔ ∃𝑥 ∈ Q 𝑥 ~Q
〈𝑎, 𝑏〉)) |
117 | 114, 116 | syl5ibrcom 237 |
. . . 4
⊢ ((𝑎 ∈ N ∧
𝑏 ∈ N)
→ (𝐴 = 〈𝑎, 𝑏〉 → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴)) |
118 | 117 | rexlimivv 3036 |
. . 3
⊢
(∃𝑎 ∈
N ∃𝑏
∈ N 𝐴 =
〈𝑎, 𝑏〉 → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴) |
119 | 1, 118 | sylbi 207 |
. 2
⊢ (𝐴 ∈ (N ×
N) → ∃𝑥 ∈ Q 𝑥 ~Q 𝐴) |
120 | | breq2 4657 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (𝑥 ~Q 𝑎 ↔ 𝑥 ~Q 𝐴)) |
121 | | breq2 4657 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (𝑦 ~Q 𝑎 ↔ 𝑦 ~Q 𝐴)) |
122 | 120, 121 | anbi12d 747 |
. . . . 5
⊢ (𝑎 = 𝐴 → ((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) ↔ (𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴))) |
123 | 122 | imbi1d 331 |
. . . 4
⊢ (𝑎 = 𝐴 → (((𝑥 ~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ((𝑥 ~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦))) |
124 | 123 | 2ralbidv 2989 |
. . 3
⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q
𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q
𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦))) |
125 | 64 | a1i 11 |
. . . . . 6
⊢ ((𝑥 ~Q
𝑎 ∧ 𝑦 ~Q 𝑎) →
~Q Er (N ×
N)) |
126 | | simpl 473 |
. . . . . 6
⊢ ((𝑥 ~Q
𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑎) |
127 | | simpr 477 |
. . . . . 6
⊢ ((𝑥 ~Q
𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑦 ~Q 𝑎) |
128 | 125, 126,
127 | ertr4d 7761 |
. . . . 5
⊢ ((𝑥 ~Q
𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 ~Q 𝑦) |
129 | | mulcompi 9718 |
. . . . . . . . . . 11
⊢
((2nd ‘𝑥) ·N
(1st ‘𝑥))
= ((1st ‘𝑥) ·N
(2nd ‘𝑥)) |
130 | | elpqn 9747 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ Q →
𝑦 ∈ (N
× N)) |
131 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑥 → (𝑦 ~Q 𝑧 ↔ 𝑥 ~Q 𝑧)) |
132 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑥 → (2nd ‘𝑦) = (2nd ‘𝑥)) |
133 | 132 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → ((2nd ‘𝑧) <N
(2nd ‘𝑦)
↔ (2nd ‘𝑧) <N
(2nd ‘𝑥))) |
134 | 133 | notbid 308 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑥 → (¬ (2nd ‘𝑧) <N
(2nd ‘𝑦)
↔ ¬ (2nd ‘𝑧) <N
(2nd ‘𝑥))) |
135 | 131, 134 | imbi12d 334 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑥 → ((𝑦 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N (2nd ‘𝑦)) ↔ (𝑥 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N (2nd ‘𝑥)))) |
136 | 135 | ralbidv 2986 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → (∀𝑧 ∈ (N ×
N)(𝑦
~Q 𝑧 → ¬ (2nd ‘𝑧) <N
(2nd ‘𝑦))
↔ ∀𝑧 ∈
(N × N)(𝑥 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N (2nd ‘𝑥)))) |
137 | 136, 92 | elrab2 3366 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ Q ↔
(𝑥 ∈ (N
× N) ∧ ∀𝑧 ∈ (N ×
N)(𝑥
~Q 𝑧 → ¬ (2nd ‘𝑧) <N
(2nd ‘𝑥)))) |
138 | 137 | simprbi 480 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ Q →
∀𝑧 ∈
(N × N)(𝑥 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N (2nd ‘𝑥))) |
139 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑦 → (𝑥 ~Q 𝑧 ↔ 𝑥 ~Q 𝑦)) |
140 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑦 → (2nd ‘𝑧) = (2nd ‘𝑦)) |
141 | 140 | breq1d 4663 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑦 → ((2nd ‘𝑧) <N
(2nd ‘𝑥)
↔ (2nd ‘𝑦) <N
(2nd ‘𝑥))) |
142 | 141 | notbid 308 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑦 → (¬ (2nd ‘𝑧) <N
(2nd ‘𝑥)
↔ ¬ (2nd ‘𝑦) <N
(2nd ‘𝑥))) |
143 | 139, 142 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑦 → ((𝑥 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N (2nd ‘𝑥)) ↔ (𝑥 ~Q 𝑦 → ¬ (2nd
‘𝑦)
<N (2nd ‘𝑥)))) |
144 | 143 | rspcva 3307 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ (N ×
N) ∧ ∀𝑧 ∈ (N ×
N)(𝑥
~Q 𝑧 → ¬ (2nd ‘𝑧) <N
(2nd ‘𝑥)))
→ (𝑥
~Q 𝑦 → ¬ (2nd ‘𝑦) <N
(2nd ‘𝑥))) |
145 | 130, 138,
144 | syl2anr 495 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥
~Q 𝑦 → ¬ (2nd ‘𝑦) <N
(2nd ‘𝑥))) |
146 | 145 | imp 445 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → ¬ (2nd ‘𝑦) <N
(2nd ‘𝑥)) |
147 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ~Q
𝑦 →
~Q Er (N ×
N)) |
148 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ~Q
𝑦 → 𝑥 ~Q 𝑦) |
149 | 147, 148 | ersym 7754 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ~Q
𝑦 → 𝑦 ~Q 𝑥) |
150 | | elpqn 9747 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ Q →
𝑥 ∈ (N
× N)) |
151 | 92 | rabeq2i 3197 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ Q ↔
(𝑦 ∈ (N
× N) ∧ ∀𝑧 ∈ (N ×
N)(𝑦
~Q 𝑧 → ¬ (2nd ‘𝑧) <N
(2nd ‘𝑦)))) |
152 | 151 | simprbi 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ Q →
∀𝑧 ∈
(N × N)(𝑦 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N (2nd ‘𝑦))) |
153 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → (𝑦 ~Q 𝑧 ↔ 𝑦 ~Q 𝑥)) |
154 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝑥 → (2nd ‘𝑧) = (2nd ‘𝑥)) |
155 | 154 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑥 → ((2nd ‘𝑧) <N
(2nd ‘𝑦)
↔ (2nd ‘𝑥) <N
(2nd ‘𝑦))) |
156 | 155 | notbid 308 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → (¬ (2nd ‘𝑧) <N
(2nd ‘𝑦)
↔ ¬ (2nd ‘𝑥) <N
(2nd ‘𝑦))) |
157 | 153, 156 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑥 → ((𝑦 ~Q 𝑧 → ¬ (2nd
‘𝑧)
<N (2nd ‘𝑦)) ↔ (𝑦 ~Q 𝑥 → ¬ (2nd
‘𝑥)
<N (2nd ‘𝑦)))) |
158 | 157 | rspcva 3307 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (N ×
N) ∧ ∀𝑧 ∈ (N ×
N)(𝑦
~Q 𝑧 → ¬ (2nd ‘𝑧) <N
(2nd ‘𝑦)))
→ (𝑦
~Q 𝑥 → ¬ (2nd ‘𝑥) <N
(2nd ‘𝑦))) |
159 | 150, 152,
158 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑦
~Q 𝑥 → ¬ (2nd ‘𝑥) <N
(2nd ‘𝑦))) |
160 | 149, 159 | syl5 34 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥
~Q 𝑦 → ¬ (2nd ‘𝑥) <N
(2nd ‘𝑦))) |
161 | 160 | imp 445 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → ¬ (2nd ‘𝑥) <N
(2nd ‘𝑦)) |
162 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (N ×
N) → (2nd ‘𝑥) ∈ N) |
163 | 150, 162 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ Q →
(2nd ‘𝑥)
∈ N) |
164 | 163 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → (2nd ‘𝑥) ∈
N) |
165 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (N ×
N) → (2nd ‘𝑦) ∈ N) |
166 | 130, 165 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ Q →
(2nd ‘𝑦)
∈ N) |
167 | 166 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → (2nd ‘𝑦) ∈
N) |
168 | | ltsopi 9710 |
. . . . . . . . . . . . . . . . . . 19
⊢
<N Or N |
169 | | sotric 5061 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((
<N Or N ∧ ((2nd
‘𝑥) ∈
N ∧ (2nd ‘𝑦) ∈ N)) →
((2nd ‘𝑥)
<N (2nd ‘𝑦) ↔ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd
‘𝑦)
<N (2nd ‘𝑥)))) |
170 | 168, 169 | mpan 706 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2nd ‘𝑥) ∈ N ∧
(2nd ‘𝑦)
∈ N) → ((2nd ‘𝑥) <N
(2nd ‘𝑦)
↔ ¬ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N
(2nd ‘𝑥)))) |
171 | 170 | notbid 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 ‘𝑥))) |
173 | 171, 172 | syl6bbr 278 |
. . . . . . . . . . . . . . . 16
⊢
(((2nd ‘𝑥) ∈ N ∧
(2nd ‘𝑦)
∈ N) → (¬ (2nd ‘𝑥) <N
(2nd ‘𝑦)
↔ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N
(2nd ‘𝑥)))) |
174 | 164, 167,
173 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → (¬ (2nd ‘𝑥) <N
(2nd ‘𝑦)
↔ ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd ‘𝑦) <N
(2nd ‘𝑥)))) |
175 | 161, 174 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → ((2nd ‘𝑥) = (2nd ‘𝑦) ∨ (2nd
‘𝑦)
<N (2nd ‘𝑥))) |
176 | 175 | ord 392 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → (¬ (2nd ‘𝑥) = (2nd ‘𝑦) → (2nd
‘𝑦)
<N (2nd ‘𝑥))) |
177 | 146, 176 | mt3d 140 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → (2nd ‘𝑥) = (2nd ‘𝑦)) |
178 | 177 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → ((1st ‘𝑥)
·N (2nd ‘𝑥)) = ((1st ‘𝑥)
·N (2nd ‘𝑦))) |
179 | 129, 178 | syl5eq 2668 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → ((2nd ‘𝑥)
·N (1st ‘𝑥)) = ((1st ‘𝑥)
·N (2nd ‘𝑦))) |
180 | | 1st2nd2 7205 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (N ×
N) → 𝑥 =
〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
181 | | 1st2nd2 7205 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (N ×
N) → 𝑦 =
〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
182 | 180, 181 | breqan12d 4669 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ 〈(1st
‘𝑥), (2nd
‘𝑥)〉
~Q 〈(1st ‘𝑦), (2nd ‘𝑦)〉)) |
183 | | xp1st 7198 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (N ×
N) → (1st ‘𝑥) ∈ N) |
184 | 183, 162 | jca 554 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (N ×
N) → ((1st ‘𝑥) ∈ N ∧
(2nd ‘𝑥)
∈ N)) |
185 | | xp1st 7198 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (N ×
N) → (1st ‘𝑦) ∈ N) |
186 | 185, 165 | jca 554 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (N ×
N) → ((1st ‘𝑦) ∈ N ∧
(2nd ‘𝑦)
∈ N)) |
187 | | enqbreq 9741 |
. . . . . . . . . . . . . 14
⊢
((((1st ‘𝑥) ∈ N ∧
(2nd ‘𝑥)
∈ N) ∧ ((1st ‘𝑦) ∈ N ∧
(2nd ‘𝑦)
∈ N)) → (〈(1st ‘𝑥), (2nd ‘𝑥)〉
~Q 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ↔ ((1st ‘𝑥)
·N (2nd ‘𝑦)) = ((2nd ‘𝑥)
·N (1st ‘𝑦)))) |
188 | 184, 186,
187 | syl2an 494 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) → (〈(1st
‘𝑥), (2nd
‘𝑥)〉
~Q 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ↔ ((1st ‘𝑥)
·N (2nd ‘𝑦)) = ((2nd ‘𝑥)
·N (1st ‘𝑦)))) |
189 | 182, 188 | bitrd 268 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) → (𝑥 ~Q 𝑦 ↔ ((1st
‘𝑥)
·N (2nd ‘𝑦)) = ((2nd ‘𝑥)
·N (1st ‘𝑦)))) |
190 | 150, 130,
189 | syl2an 494 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥
~Q 𝑦 ↔ ((1st ‘𝑥)
·N (2nd ‘𝑦)) = ((2nd ‘𝑥)
·N (1st ‘𝑦)))) |
191 | 190 | biimpa 501 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → ((1st ‘𝑥)
·N (2nd ‘𝑦)) = ((2nd ‘𝑥)
·N (1st ‘𝑦))) |
192 | 179, 191 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → ((2nd ‘𝑥)
·N (1st ‘𝑥)) = ((2nd ‘𝑥)
·N (1st ‘𝑦))) |
193 | 150 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → 𝑥 ∈ (N ×
N)) |
194 | | mulcanpi 9722 |
. . . . . . . . . . 11
⊢
(((2nd ‘𝑥) ∈ N ∧
(1st ‘𝑥)
∈ N) → (((2nd ‘𝑥) ·N
(1st ‘𝑥))
= ((2nd ‘𝑥) ·N
(1st ‘𝑦))
↔ (1st ‘𝑥) = (1st ‘𝑦))) |
195 | 162, 183,
194 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (N ×
N) → (((2nd ‘𝑥) ·N
(1st ‘𝑥))
= ((2nd ‘𝑥) ·N
(1st ‘𝑦))
↔ (1st ‘𝑥) = (1st ‘𝑦))) |
196 | 193, 195 | syl 17 |
. . . . . . . . 9
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → (((2nd ‘𝑥)
·N (1st ‘𝑥)) = ((2nd ‘𝑥)
·N (1st ‘𝑦)) ↔ (1st ‘𝑥) = (1st ‘𝑦))) |
197 | 192, 196 | mpbid 222 |
. . . . . . . 8
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → (1st ‘𝑥) = (1st ‘𝑦)) |
198 | 197, 177 | opeq12d 4410 |
. . . . . . 7
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → 〈(1st ‘𝑥), (2nd ‘𝑥)〉 = 〈(1st
‘𝑦), (2nd
‘𝑦)〉) |
199 | 193, 180 | syl 17 |
. . . . . . 7
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
200 | 130 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → 𝑦 ∈ (N ×
N)) |
201 | 200, 181 | syl 17 |
. . . . . . 7
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
202 | 198, 199,
201 | 3eqtr4d 2666 |
. . . . . 6
⊢ (((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ 𝑥
~Q 𝑦) → 𝑥 = 𝑦) |
203 | 202 | ex 450 |
. . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥
~Q 𝑦 → 𝑥 = 𝑦)) |
204 | 128, 203 | syl5 34 |
. . . 4
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ ((𝑥
~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦)) |
205 | 204 | rgen2a 2977 |
. . 3
⊢
∀𝑥 ∈
Q ∀𝑦
∈ Q ((𝑥
~Q 𝑎 ∧ 𝑦 ~Q 𝑎) → 𝑥 = 𝑦) |
206 | 124, 205 | vtoclg 3266 |
. 2
⊢ (𝐴 ∈ (N ×
N) → ∀𝑥 ∈ Q ∀𝑦 ∈ Q ((𝑥 ~Q
𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦)) |
207 | | breq1 4656 |
. . 3
⊢ (𝑥 = 𝑦 → (𝑥 ~Q 𝐴 ↔ 𝑦 ~Q 𝐴)) |
208 | 207 | reu4 3400 |
. 2
⊢
(∃!𝑥 ∈
Q 𝑥
~Q 𝐴 ↔ (∃𝑥 ∈ Q 𝑥 ~Q 𝐴 ∧ ∀𝑥 ∈ Q
∀𝑦 ∈
Q ((𝑥
~Q 𝐴 ∧ 𝑦 ~Q 𝐴) → 𝑥 = 𝑦))) |
209 | 119, 206,
208 | sylanbrc 698 |
1
⊢ (𝐴 ∈ (N ×
N) → ∃!𝑥 ∈ Q 𝑥 ~Q 𝐴) |