Step | Hyp | Ref
| Expression |
1 | | opeq1 3778 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 1o →
⟨𝑤,
1o⟩ = ⟨1o,
1o⟩) |
2 | 1 | eceq1d 6570 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 1o →
[⟨𝑤,
1o⟩] ~Q = [⟨1o,
1o⟩] ~Q ) |
3 | 2 | breq2d 4015 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 1o → (𝑙 <Q
[⟨𝑤,
1o⟩] ~Q ↔ 𝑙 <Q
[⟨1o, 1o⟩] ~Q
)) |
4 | 3 | abbidv 2295 |
. . . . . . . . . . . 12
⊢ (𝑤 = 1o → {𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q } = {𝑙 ∣ 𝑙 <Q
[⟨1o, 1o⟩] ~Q
}) |
5 | 2 | breq1d 4013 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 1o →
([⟨𝑤,
1o⟩] ~Q <Q
𝑢 ↔
[⟨1o, 1o⟩] ~Q
<Q 𝑢)) |
6 | 5 | abbidv 2295 |
. . . . . . . . . . . 12
⊢ (𝑤 = 1o → {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢} = {𝑢 ∣ [⟨1o,
1o⟩] ~Q <Q
𝑢}) |
7 | 4, 6 | opeq12d 3786 |
. . . . . . . . . . 11
⊢ (𝑤 = 1o →
⟨{𝑙 ∣ 𝑙 <Q
[⟨𝑤,
1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ = ⟨{𝑙 ∣ 𝑙 <Q
[⟨1o, 1o⟩] ~Q },
{𝑢 ∣
[⟨1o, 1o⟩] ~Q
<Q 𝑢}⟩) |
8 | 7 | oveq1d 5889 |
. . . . . . . . . 10
⊢ (𝑤 = 1o →
(⟨{𝑙 ∣ 𝑙 <Q
[⟨𝑤,
1o⟩] ~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P) = (⟨{𝑙 ∣ 𝑙 <Q
[⟨1o, 1o⟩] ~Q },
{𝑢 ∣
[⟨1o, 1o⟩] ~Q
<Q 𝑢}⟩ +P
1P)) |
9 | 8 | opeq1d 3784 |
. . . . . . . . 9
⊢ (𝑤 = 1o →
⟨(⟨{𝑙 ∣
𝑙
<Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩ =
⟨(⟨{𝑙 ∣
𝑙
<Q [⟨1o, 1o⟩]
~Q }, {𝑢 ∣ [⟨1o,
1o⟩] ~Q <Q
𝑢}⟩
+P 1P),
1P⟩) |
10 | 9 | eceq1d 6570 |
. . . . . . . 8
⊢ (𝑤 = 1o →
[⟨(⟨{𝑙 ∣
𝑙
<Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R = [⟨(⟨{𝑙 ∣ 𝑙 <Q
[⟨1o, 1o⟩] ~Q },
{𝑢 ∣
[⟨1o, 1o⟩] ~Q
<Q 𝑢}⟩ +P
1P), 1P⟩]
~R ) |
11 | 10 | opeq1d 3784 |
. . . . . . 7
⊢ (𝑤 = 1o →
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ =
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨1o, 1o⟩]
~Q }, {𝑢 ∣ [⟨1o,
1o⟩] ~Q <Q
𝑢}⟩
+P 1P),
1P⟩] ~R ,
0R⟩) |
12 | 11 | eleq1d 2246 |
. . . . . 6
⊢ (𝑤 = 1o →
(⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧 ↔
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨1o, 1o⟩]
~Q }, {𝑢 ∣ [⟨1o,
1o⟩] ~Q <Q
𝑢}⟩
+P 1P),
1P⟩] ~R ,
0R⟩ ∈ 𝑧)) |
13 | 12 | imbi2d 230 |
. . . . 5
⊢ (𝑤 = 1o → (((1
∈ 𝑧 ∧
∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧) ↔ ((1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q
[⟨1o, 1o⟩] ~Q },
{𝑢 ∣
[⟨1o, 1o⟩] ~Q
<Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧))) |
14 | | opeq1 3778 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑘 → ⟨𝑤, 1o⟩ = ⟨𝑘,
1o⟩) |
15 | 14 | eceq1d 6570 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑘 → [⟨𝑤, 1o⟩]
~Q = [⟨𝑘, 1o⟩]
~Q ) |
16 | 15 | breq2d 4015 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑘 → (𝑙 <Q [⟨𝑤, 1o⟩]
~Q ↔ 𝑙 <Q [⟨𝑘, 1o⟩]
~Q )) |
17 | 16 | abbidv 2295 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑘 → {𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q } = {𝑙 ∣ 𝑙 <Q [⟨𝑘, 1o⟩]
~Q }) |
18 | 15 | breq1d 4013 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑘 → ([⟨𝑤, 1o⟩]
~Q <Q 𝑢 ↔ [⟨𝑘, 1o⟩]
~Q <Q 𝑢)) |
19 | 18 | abbidv 2295 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑘 → {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢} = {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}) |
20 | 17, 19 | opeq12d 3786 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑘 → ⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ = ⟨{𝑙 ∣ 𝑙 <Q [⟨𝑘, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}⟩) |
21 | 20 | oveq1d 5889 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑘 → (⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P) = (⟨{𝑙 ∣ 𝑙 <Q [⟨𝑘, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P)) |
22 | 21 | opeq1d 3784 |
. . . . . . . . 9
⊢ (𝑤 = 𝑘 → ⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩ =
⟨(⟨{𝑙 ∣
𝑙
<Q [⟨𝑘, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P),
1P⟩) |
23 | 22 | eceq1d 6570 |
. . . . . . . 8
⊢ (𝑤 = 𝑘 → [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R = [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑘, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R ) |
24 | 23 | opeq1d 3784 |
. . . . . . 7
⊢ (𝑤 = 𝑘 → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ =
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑘, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R ,
0R⟩) |
25 | 24 | eleq1d 2246 |
. . . . . 6
⊢ (𝑤 = 𝑘 → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧 ↔
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑘, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧)) |
26 | 25 | imbi2d 230 |
. . . . 5
⊢ (𝑤 = 𝑘 → (((1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧) ↔ ((1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑘, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧))) |
27 | | opeq1 3778 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝑘 +N 1o)
→ ⟨𝑤,
1o⟩ = ⟨(𝑘 +N 1o),
1o⟩) |
28 | 27 | eceq1d 6570 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝑘 +N 1o)
→ [⟨𝑤,
1o⟩] ~Q = [⟨(𝑘 +N 1o),
1o⟩] ~Q ) |
29 | 28 | breq2d 4015 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝑘 +N 1o)
→ (𝑙
<Q [⟨𝑤, 1o⟩]
~Q ↔ 𝑙 <Q [⟨(𝑘 +N
1o), 1o⟩] ~Q
)) |
30 | 29 | abbidv 2295 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝑘 +N 1o)
→ {𝑙 ∣ 𝑙 <Q
[⟨𝑤,
1o⟩] ~Q } = {𝑙 ∣ 𝑙 <Q [⟨(𝑘 +N
1o), 1o⟩] ~Q
}) |
31 | 28 | breq1d 4013 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝑘 +N 1o)
→ ([⟨𝑤,
1o⟩] ~Q <Q
𝑢 ↔ [⟨(𝑘 +N
1o), 1o⟩] ~Q
<Q 𝑢)) |
32 | 31 | abbidv 2295 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝑘 +N 1o)
→ {𝑢 ∣
[⟨𝑤,
1o⟩] ~Q <Q
𝑢} = {𝑢 ∣ [⟨(𝑘 +N 1o),
1o⟩] ~Q <Q
𝑢}) |
33 | 30, 32 | opeq12d 3786 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑘 +N 1o)
→ ⟨{𝑙 ∣
𝑙
<Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ = ⟨{𝑙 ∣ 𝑙 <Q [⟨(𝑘 +N
1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝑘 +N
1o), 1o⟩] ~Q
<Q 𝑢}⟩) |
34 | 33 | oveq1d 5889 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑘 +N 1o)
→ (⟨{𝑙 ∣
𝑙
<Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P) = (⟨{𝑙 ∣ 𝑙 <Q [⟨(𝑘 +N
1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝑘 +N
1o), 1o⟩] ~Q
<Q 𝑢}⟩ +P
1P)) |
35 | 34 | opeq1d 3784 |
. . . . . . . . 9
⊢ (𝑤 = (𝑘 +N 1o)
→ ⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩ =
⟨(⟨{𝑙 ∣
𝑙
<Q [⟨(𝑘 +N 1o),
1o⟩] ~Q }, {𝑢 ∣ [⟨(𝑘 +N 1o),
1o⟩] ~Q <Q
𝑢}⟩
+P 1P),
1P⟩) |
36 | 35 | eceq1d 6570 |
. . . . . . . 8
⊢ (𝑤 = (𝑘 +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 ) |
37 | 36 | opeq1d 3784 |
. . . . . . 7
⊢ (𝑤 = (𝑘 +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⟩) |
38 | 37 | eleq1d 2246 |
. . . . . 6
⊢ (𝑤 = (𝑘 +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⟩ ∈ 𝑧)) |
39 | 38 | imbi2d 230 |
. . . . 5
⊢ (𝑤 = (𝑘 +N 1o)
→ (((1 ∈ 𝑧 ∧
∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧) ↔ ((1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨(𝑘 +N
1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝑘 +N
1o), 1o⟩] ~Q
<Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧))) |
40 | | opeq1 3778 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑁 → ⟨𝑤, 1o⟩ = ⟨𝑁,
1o⟩) |
41 | 40 | eceq1d 6570 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑁 → [⟨𝑤, 1o⟩]
~Q = [⟨𝑁, 1o⟩]
~Q ) |
42 | 41 | breq2d 4015 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑁 → (𝑙 <Q [⟨𝑤, 1o⟩]
~Q ↔ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q )) |
43 | 42 | abbidv 2295 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑁 → {𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q } = {𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }) |
44 | 41 | breq1d 4013 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑁 → ([⟨𝑤, 1o⟩]
~Q <Q 𝑢 ↔ [⟨𝑁, 1o⟩]
~Q <Q 𝑢)) |
45 | 44 | abbidv 2295 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑁 → {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢} = {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}) |
46 | 43, 45 | opeq12d 3786 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑁 → ⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ = ⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩) |
47 | 46 | oveq1d 5889 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑁 → (⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P) = (⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P)) |
48 | 47 | opeq1d 3784 |
. . . . . . . . 9
⊢ (𝑤 = 𝑁 → ⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩ =
⟨(⟨{𝑙 ∣
𝑙
<Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P),
1P⟩) |
49 | 48 | eceq1d 6570 |
. . . . . . . 8
⊢ (𝑤 = 𝑁 → [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R = [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R ) |
50 | 49 | opeq1d 3784 |
. . . . . . 7
⊢ (𝑤 = 𝑁 → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ =
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R ,
0R⟩) |
51 | 50 | eleq1d 2246 |
. . . . . 6
⊢ (𝑤 = 𝑁 → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧 ↔
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧)) |
52 | 51 | imbi2d 230 |
. . . . 5
⊢ (𝑤 = 𝑁 → (((1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑤, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑤, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧) ↔ ((1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧))) |
53 | | pitonnlem1 7843 |
. . . . . . . 8
⊢
⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q
[⟨1o, 1o⟩] ~Q },
{𝑢 ∣
[⟨1o, 1o⟩] ~Q
<Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ =
1 |
54 | 53 | eleq1i 2243 |
. . . . . . 7
⊢
(⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q
[⟨1o, 1o⟩] ~Q },
{𝑢 ∣
[⟨1o, 1o⟩] ~Q
<Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧 ↔ 1 ∈ 𝑧) |
55 | 54 | biimpri 133 |
. . . . . 6
⊢ (1 ∈
𝑧 →
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨1o, 1o⟩]
~Q }, {𝑢 ∣ [⟨1o,
1o⟩] ~Q <Q
𝑢}⟩
+P 1P),
1P⟩] ~R ,
0R⟩ ∈ 𝑧) |
56 | 55 | adantr 276 |
. . . . 5
⊢ ((1
∈ 𝑧 ∧
∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q
[⟨1o, 1o⟩] ~Q },
{𝑢 ∣
[⟨1o, 1o⟩] ~Q
<Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧) |
57 | | oveq1 5881 |
. . . . . . . . . . 11
⊢ (𝑦 = ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑘, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ → (𝑦 + 1) =
(⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑘, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ +
1)) |
58 | 57 | eleq1d 2246 |
. . . . . . . . . 10
⊢ (𝑦 = ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑘, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ → ((𝑦 + 1) ∈ 𝑧 ↔ (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑘, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ + 1) ∈
𝑧)) |
59 | 58 | rspccv 2838 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
𝑧 (𝑦 + 1) ∈ 𝑧 → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑘, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧 →
(⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑘, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ + 1) ∈
𝑧)) |
60 | 59 | ad2antll 491 |
. . . . . . . 8
⊢ ((𝑘 ∈ N ∧ (1
∈ 𝑧 ∧
∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)) → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑘, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧 →
(⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑘, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ + 1) ∈
𝑧)) |
61 | | pitonnlem2 7845 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 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⟩) |
62 | 61 | eleq1d 2246 |
. . . . . . . . 9
⊢ (𝑘 ∈ 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⟩ ∈ 𝑧)) |
63 | 62 | adantr 276 |
. . . . . . . 8
⊢ ((𝑘 ∈ N ∧ (1
∈ 𝑧 ∧
∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)) → ((⟨[⟨(⟨{𝑙 ∣ 𝑙 <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⟩ ∈ 𝑧)) |
64 | 60, 63 | sylibd 149 |
. . . . . . 7
⊢ ((𝑘 ∈ N ∧ (1
∈ 𝑧 ∧
∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)) → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <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⟩ ∈ 𝑧)) |
65 | 64 | ex 115 |
. . . . . 6
⊢ (𝑘 ∈ N →
((1 ∈ 𝑧 ∧
∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <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⟩ ∈ 𝑧))) |
66 | 65 | a2d 26 |
. . . . 5
⊢ (𝑘 ∈ N →
(((1 ∈ 𝑧 ∧
∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑘, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑘, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧) → ((1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨(𝑘 +N
1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝑘 +N
1o), 1o⟩] ~Q
<Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧))) |
67 | 13, 26, 39, 52, 56, 66 | indpi 7340 |
. . . 4
⊢ (𝑁 ∈ N →
((1 ∈ 𝑧 ∧
∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧)) |
68 | 67 | alrimiv 1874 |
. . 3
⊢ (𝑁 ∈ N →
∀𝑧((1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧)) |
69 | | eleq2 2241 |
. . . . 5
⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧)) |
70 | | eleq2 2241 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧)) |
71 | 70 | raleqbi1dv 2680 |
. . . . 5
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)) |
72 | 69, 71 | anbi12d 473 |
. . . 4
⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))) |
73 | 72 | ralab 2897 |
. . 3
⊢
(∀𝑧 ∈
{𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧 ↔ ∀𝑧((1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧)) |
74 | 68, 73 | sylibr 134 |
. 2
⊢ (𝑁 ∈ N →
∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧) |
75 | | nnprlu 7551 |
. . . . . . 7
⊢ (𝑁 ∈ N →
⟨{𝑙 ∣ 𝑙 <Q
[⟨𝑁,
1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ ∈
P) |
76 | | 1pr 7552 |
. . . . . . 7
⊢
1P ∈ P |
77 | | addclpr 7535 |
. . . . . . 7
⊢
((⟨{𝑙 ∣
𝑙
<Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ ∈ P ∧
1P ∈ P) → (⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P) ∈ P) |
78 | 75, 76, 77 | sylancl 413 |
. . . . . 6
⊢ (𝑁 ∈ N →
(⟨{𝑙 ∣ 𝑙 <Q
[⟨𝑁,
1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P) ∈ P) |
79 | | opelxpi 4658 |
. . . . . 6
⊢
(((⟨{𝑙 ∣
𝑙
<Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P) ∈ P ∧
1P ∈ P) → ⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩ ∈
(P × P)) |
80 | 78, 76, 79 | sylancl 413 |
. . . . 5
⊢ (𝑁 ∈ N →
⟨(⟨{𝑙 ∣
𝑙
<Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩ ∈
(P × P)) |
81 | | enrex 7735 |
. . . . . 6
⊢
~R ∈ V |
82 | 81 | ecelqsi 6588 |
. . . . 5
⊢
(⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩ ∈
(P × P) → [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R ∈ ((P × P)
/ ~R )) |
83 | 80, 82 | syl 14 |
. . . 4
⊢ (𝑁 ∈ N →
[⟨(⟨{𝑙 ∣
𝑙
<Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R ∈ ((P × P)
/ ~R )) |
84 | | 0r 7748 |
. . . 4
⊢
0R ∈ R |
85 | | opelxpi 4658 |
. . . 4
⊢
(([⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R ∈ ((P × P)
/ ~R ) ∧ 0R ∈
R) → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈
(((P × P) /
~R ) × R)) |
86 | 83, 84, 85 | sylancl 413 |
. . 3
⊢ (𝑁 ∈ N →
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈
(((P × P) /
~R ) × R)) |
87 | | elintg 3852 |
. . 3
⊢
(⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈
(((P × P) /
~R ) × R) →
(⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ ∩ {𝑥
∣ (1 ∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧)) |
88 | 86, 87 | syl 14 |
. 2
⊢ (𝑁 ∈ N →
(⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ ∩ {𝑥
∣ (1 ∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ 𝑧)) |
89 | 74, 88 | mpbird 167 |
1
⊢ (𝑁 ∈ N →
⟨[⟨(⟨{𝑙
∣ 𝑙
<Q [⟨𝑁, 1o⟩]
~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩]
~Q <Q 𝑢}⟩ +P
1P), 1P⟩]
~R , 0R⟩ ∈ ∩ {𝑥
∣ (1 ∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}) |