Step | Hyp | Ref
| Expression |
1 | | nntopi.n |
. 2
⊢ 𝑁 = ∩
{𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} |
2 | | eqeq2 2187 |
. . 3
⊢ (𝑤 = 1 →
(⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑤 ↔
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ =
1)) |
3 | 2 | rexbidv 2478 |
. 2
⊢ (𝑤 = 1 → (∃𝑧 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑤 ↔ ∃𝑧 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ =
1)) |
4 | | eqeq2 2187 |
. . 3
⊢ (𝑤 = 𝑘 → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑤 ↔
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑘)) |
5 | 4 | rexbidv 2478 |
. 2
⊢ (𝑤 = 𝑘 → (∃𝑧 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑤 ↔ ∃𝑧 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑘)) |
6 | | eqeq2 2187 |
. . 3
⊢ (𝑤 = (𝑘 + 1) → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑤 ↔
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = (𝑘 + 1))) |
7 | 6 | rexbidv 2478 |
. 2
⊢ (𝑤 = (𝑘 + 1) → (∃𝑧 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑤 ↔ ∃𝑧 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = (𝑘 + 1))) |
8 | | eqeq2 2187 |
. . 3
⊢ (𝑤 = 𝐴 → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑤 ↔
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝐴)) |
9 | 8 | rexbidv 2478 |
. 2
⊢ (𝑤 = 𝐴 → (∃𝑧 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑤 ↔ ∃𝑧 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝐴)) |
10 | | 1pi 7314 |
. . 3
⊢
1o ∈ N |
11 | | eqid 2177 |
. . 3
⊢ 1 =
1 |
12 | | opeq1 3779 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 1o →
⟨𝑧,
1o⟩ = ⟨1o,
1o⟩) |
13 | 12 | eceq1d 6571 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 1o →
[⟨𝑧,
1o⟩] ~Q = [⟨1o,
1o⟩] ~Q ) |
14 | | df-1nqqs 7350 |
. . . . . . . . . . . . . . . 16
⊢
1Q = [⟨1o, 1o⟩]
~Q |
15 | 13, 14 | eqtr4di 2228 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 1o →
[⟨𝑧,
1o⟩] ~Q =
1Q) |
16 | 15 | breq2d 4016 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 1o → (𝑙 <Q
[⟨𝑧,
1o⟩] ~Q ↔ 𝑙 <Q
1Q)) |
17 | 16 | abbidv 2295 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 1o → {𝑙 ∣ 𝑙 <Q [⟨𝑧, 1o⟩]
~Q } = {𝑙 ∣ 𝑙 <Q
1Q}) |
18 | 15 | breq1d 4014 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 1o →
([⟨𝑧,
1o⟩] ~Q <Q
𝑢 ↔
1Q <Q 𝑢)) |
19 | 18 | abbidv 2295 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 1o → {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢} = {𝑢 ∣ 1Q
<Q 𝑢}) |
20 | 17, 19 | opeq12d 3787 |
. . . . . . . . . . . 12
⊢ (𝑧 = 1o →
⟨{𝑙 ∣ 𝑙 <Q
[⟨𝑧,
1o⟩] ~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ = ⟨{𝑙 ∣ 𝑙 <Q
1Q}, {𝑢 ∣ 1Q
<Q 𝑢}⟩) |
21 | | df-i1p 7466 |
. . . . . . . . . . . 12
⊢
1P = ⟨{𝑙 ∣ 𝑙 <Q
1Q}, {𝑢 ∣ 1Q
<Q 𝑢}⟩ |
22 | 20, 21 | eqtr4di 2228 |
. . . . . . . . . . 11
⊢ (𝑧 = 1o →
⟨{𝑙 ∣ 𝑙 <Q
[⟨𝑧,
1o⟩] ~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ =
1P) |
23 | 22 | oveq1d 5890 |
. . . . . . . . . 10
⊢ (𝑧 = 1o →
(⟨{𝑙 ∣ 𝑙 <Q
[⟨𝑧,
1o⟩] ~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P) = (1P
+P 1P)) |
24 | 23 | opeq1d 3785 |
. . . . . . . . 9
⊢ (𝑧 = 1o →
⟨(⟨{𝑙 ∣
𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩ =
⟨(1P +P
1P),
1P⟩) |
25 | 24 | eceq1d 6571 |
. . . . . . . 8
⊢ (𝑧 = 1o →
[⟨(⟨{𝑙 ∣
𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R = [⟨(1P
+P 1P),
1P⟩] ~R
) |
26 | | df-1r 7731 |
. . . . . . . 8
⊢
1R = [⟨(1P
+P 1P),
1P⟩] ~R |
27 | 25, 26 | eqtr4di 2228 |
. . . . . . 7
⊢ (𝑧 = 1o →
[⟨(⟨{𝑙 ∣
𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R = 1R) |
28 | 27 | opeq1d 3785 |
. . . . . 6
⊢ (𝑧 = 1o →
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ =
⟨1R,
0R⟩) |
29 | | df-1 7819 |
. . . . . 6
⊢ 1 =
⟨1R,
0R⟩ |
30 | 28, 29 | eqtr4di 2228 |
. . . . 5
⊢ (𝑧 = 1o →
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ =
1) |
31 | 30 | eqeq1d 2186 |
. . . 4
⊢ (𝑧 = 1o →
(⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 1 ↔ 1 =
1)) |
32 | 31 | rspcev 2842 |
. . 3
⊢
((1o ∈ N ∧ 1 = 1) → ∃𝑧 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ =
1) |
33 | 10, 11, 32 | mp2an 426 |
. 2
⊢
∃𝑧 ∈
N ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ =
1 |
34 | | simplr 528 |
. . . . . . 7
⊢ (((𝑘 ∈ 𝑁 ∧ 𝑧 ∈ N) ∧
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑘) → 𝑧 ∈ N) |
35 | | addclpi 7326 |
. . . . . . 7
⊢ ((𝑧 ∈ N ∧
1o ∈ N) → (𝑧 +N 1o)
∈ N) |
36 | 34, 10, 35 | sylancl 413 |
. . . . . 6
⊢ (((𝑘 ∈ 𝑁 ∧ 𝑧 ∈ N) ∧
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑘) → (𝑧 +N 1o)
∈ N) |
37 | | pitonnlem2 7846 |
. . . . . . . 8
⊢ (𝑧 ∈ N →
(⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ + 1) =
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨(𝑧 +N 1o),
1o⟩] ~Q }, {𝑢 ∣ [⟨(𝑧 +N 1o),
1o⟩] ~Q <Q
𝑢}⟩
+P 1P),
1P⟩] ~R ,
0R⟩) |
38 | 34, 37 | syl 14 |
. . . . . . 7
⊢ (((𝑘 ∈ 𝑁 ∧ 𝑧 ∈ N) ∧
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑘) →
(⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ + 1) =
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨(𝑧 +N 1o),
1o⟩] ~Q }, {𝑢 ∣ [⟨(𝑧 +N 1o),
1o⟩] ~Q <Q
𝑢}⟩
+P 1P),
1P⟩] ~R ,
0R⟩) |
39 | | simpr 110 |
. . . . . . . 8
⊢ (((𝑘 ∈ 𝑁 ∧ 𝑧 ∈ N) ∧
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑘) →
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑘) |
40 | 39 | oveq1d 5890 |
. . . . . . 7
⊢ (((𝑘 ∈ 𝑁 ∧ 𝑧 ∈ N) ∧
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑘) →
(⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ + 1) = (𝑘 + 1)) |
41 | 38, 40 | eqtr3d 2212 |
. . . . . 6
⊢ (((𝑘 ∈ 𝑁 ∧ 𝑧 ∈ N) ∧
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑘) →
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨(𝑧 +N 1o),
1o⟩] ~Q }, {𝑢 ∣ [⟨(𝑧 +N 1o),
1o⟩] ~Q <Q
𝑢}⟩
+P 1P),
1P⟩] ~R ,
0R⟩ = (𝑘 + 1)) |
42 | | opeq1 3779 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = (𝑧 +N 1o)
→ ⟨𝑣,
1o⟩ = ⟨(𝑧 +N 1o),
1o⟩) |
43 | 42 | eceq1d 6571 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = (𝑧 +N 1o)
→ [⟨𝑣,
1o⟩] ~Q = [⟨(𝑧 +N 1o),
1o⟩] ~Q ) |
44 | 43 | breq2d 4016 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑧 +N 1o)
→ (𝑙
<Q [⟨𝑣, 1o⟩]
~Q ↔ 𝑙 <Q [⟨(𝑧 +N
1o), 1o⟩] ~Q
)) |
45 | 44 | abbidv 2295 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (𝑧 +N 1o)
→ {𝑙 ∣ 𝑙 <Q
[⟨𝑣,
1o⟩] ~Q } = {𝑙 ∣ 𝑙 <Q [⟨(𝑧 +N
1o), 1o⟩] ~Q
}) |
46 | 43 | breq1d 4014 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑧 +N 1o)
→ ([⟨𝑣,
1o⟩] ~Q <Q
𝑢 ↔ [⟨(𝑧 +N
1o), 1o⟩] ~Q
<Q 𝑢)) |
47 | 46 | abbidv 2295 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (𝑧 +N 1o)
→ {𝑢 ∣
[⟨𝑣,
1o⟩] ~Q <Q
𝑢} = {𝑢 ∣ [⟨(𝑧 +N 1o),
1o⟩] ~Q <Q
𝑢}) |
48 | 45, 47 | opeq12d 3787 |
. . . . . . . . . . . 12
⊢ (𝑣 = (𝑧 +N 1o)
→ ⟨{𝑙 ∣
𝑙
<Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ = ⟨{𝑙 ∣ 𝑙 <Q [⟨(𝑧 +N
1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝑧 +N
1o), 1o⟩] ~Q
<Q 𝑢}⟩) |
49 | 48 | oveq1d 5890 |
. . . . . . . . . . 11
⊢ (𝑣 = (𝑧 +N 1o)
→ (⟨{𝑙 ∣
𝑙
<Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P) = (⟨{𝑙 ∣ 𝑙 <Q [⟨(𝑧 +N
1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝑧 +N
1o), 1o⟩] ~Q
<Q 𝑢}⟩ +P
1P)) |
50 | 49 | opeq1d 3785 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑧 +N 1o)
→ ⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩ =
⟨(⟨{𝑙 ∣
𝑙
<Q [⟨(𝑧 +N 1o),
1o⟩] ~Q }, {𝑢 ∣ [⟨(𝑧 +N 1o),
1o⟩] ~Q <Q
𝑢}⟩
+P 1P),
1P⟩) |
51 | 50 | eceq1d 6571 |
. . . . . . . . 9
⊢ (𝑣 = (𝑧 +N 1o)
→ [⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R = [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨(𝑧 +N
1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝑧 +N
1o), 1o⟩] ~Q
<Q 𝑢}⟩ +P
1P), 1P⟩]
~R ) |
52 | 51 | opeq1d 3785 |
. . . . . . . 8
⊢ (𝑣 = (𝑧 +N 1o)
→ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ =
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨(𝑧 +N 1o),
1o⟩] ~Q }, {𝑢 ∣ [⟨(𝑧 +N 1o),
1o⟩] ~Q <Q
𝑢}⟩
+P 1P),
1P⟩] ~R ,
0R⟩) |
53 | 52 | eqeq1d 2186 |
. . . . . . 7
⊢ (𝑣 = (𝑧 +N 1o)
→ (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = (𝑘 + 1) ↔
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨(𝑧 +N 1o),
1o⟩] ~Q }, {𝑢 ∣ [⟨(𝑧 +N 1o),
1o⟩] ~Q <Q
𝑢}⟩
+P 1P),
1P⟩] ~R ,
0R⟩ = (𝑘 + 1))) |
54 | 53 | rspcev 2842 |
. . . . . 6
⊢ (((𝑧 +N
1o) ∈ N ∧ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨(𝑧 +N
1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝑧 +N
1o), 1o⟩] ~Q
<Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = (𝑘 + 1)) → ∃𝑣 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = (𝑘 + 1)) |
55 | 36, 41, 54 | syl2anc 411 |
. . . . 5
⊢ (((𝑘 ∈ 𝑁 ∧ 𝑧 ∈ N) ∧
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑘) → ∃𝑣 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = (𝑘 + 1)) |
56 | 55 | ex 115 |
. . . 4
⊢ ((𝑘 ∈ 𝑁 ∧ 𝑧 ∈ N) →
(⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑘 → ∃𝑣 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = (𝑘 + 1))) |
57 | 56 | rexlimdva 2594 |
. . 3
⊢ (𝑘 ∈ 𝑁 → (∃𝑧 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑘 → ∃𝑣 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = (𝑘 + 1))) |
58 | | opeq1 3779 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑧 → ⟨𝑣, 1o⟩ = ⟨𝑧,
1o⟩) |
59 | 58 | eceq1d 6571 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑧 → [⟨𝑣, 1o⟩]
~Q = [⟨𝑧, 1o⟩]
~Q ) |
60 | 59 | breq2d 4016 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑧 → (𝑙 <Q [⟨𝑣, 1o⟩]
~Q ↔ 𝑙 <Q [⟨𝑧, 1o⟩]
~Q )) |
61 | 60 | abbidv 2295 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑧 → {𝑙 ∣ 𝑙 <Q [⟨𝑣, 1o⟩]
~Q } = {𝑙 ∣ 𝑙 <Q [⟨𝑧, 1o⟩]
~Q }) |
62 | 59 | breq1d 4014 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑧 → ([⟨𝑣, 1o⟩]
~Q <Q 𝑢 ↔ [⟨𝑧, 1o⟩]
~Q <Q 𝑢)) |
63 | 62 | abbidv 2295 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑧 → {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢} = {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}) |
64 | 61, 63 | opeq12d 3787 |
. . . . . . . . 9
⊢ (𝑣 = 𝑧 → ⟨{𝑙 ∣ 𝑙 <Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ = ⟨{𝑙 ∣ 𝑙 <Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩) |
65 | 64 | oveq1d 5890 |
. . . . . . . 8
⊢ (𝑣 = 𝑧 → (⟨{𝑙 ∣ 𝑙 <Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P) = (⟨{𝑙 ∣ 𝑙 <Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P)) |
66 | 65 | opeq1d 3785 |
. . . . . . 7
⊢ (𝑣 = 𝑧 → ⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩ =
⟨(⟨{𝑙 ∣
𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P),
1P⟩) |
67 | 66 | eceq1d 6571 |
. . . . . 6
⊢ (𝑣 = 𝑧 → [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R = [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R ) |
68 | 67 | opeq1d 3785 |
. . . . 5
⊢ (𝑣 = 𝑧 → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ =
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R ,
0R⟩) |
69 | 68 | eqeq1d 2186 |
. . . 4
⊢ (𝑣 = 𝑧 → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = (𝑘 + 1) ↔
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = (𝑘 + 1))) |
70 | 69 | cbvrexv 2705 |
. . 3
⊢
(∃𝑣 ∈
N ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑣, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑣, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = (𝑘 + 1) ↔ ∃𝑧 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = (𝑘 + 1)) |
71 | 57, 70 | imbitrdi 161 |
. 2
⊢ (𝑘 ∈ 𝑁 → (∃𝑧 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝑘 → ∃𝑧 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = (𝑘 + 1))) |
72 | 1, 3, 5, 7, 9, 33,
71 | nnindnn 7892 |
1
⊢ (𝐴 ∈ 𝑁 → ∃𝑧 ∈ N
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑧, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ = 𝐴) |