Step | Hyp | Ref
| Expression |
1 | | breq2 3993 |
. . . . 5
⊢ (𝑧 = 1 → (𝑦 < 𝑧 ↔ 𝑦 < 1)) |
2 | 1 | imbi1d 230 |
. . . 4
⊢ (𝑧 = 1 → ((𝑦 < 𝑧 → 𝜓) ↔ (𝑦 < 1 → 𝜓))) |
3 | 2 | ralbidv 2470 |
. . 3
⊢ (𝑧 = 1 → (∀𝑦 ∈ ℕ (𝑦 < 𝑧 → 𝜓) ↔ ∀𝑦 ∈ ℕ (𝑦 < 1 → 𝜓))) |
4 | | breq2 3993 |
. . . . 5
⊢ (𝑧 = 𝑤 → (𝑦 < 𝑧 ↔ 𝑦 < 𝑤)) |
5 | 4 | imbi1d 230 |
. . . 4
⊢ (𝑧 = 𝑤 → ((𝑦 < 𝑧 → 𝜓) ↔ (𝑦 < 𝑤 → 𝜓))) |
6 | 5 | ralbidv 2470 |
. . 3
⊢ (𝑧 = 𝑤 → (∀𝑦 ∈ ℕ (𝑦 < 𝑧 → 𝜓) ↔ ∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓))) |
7 | | breq2 3993 |
. . . . 5
⊢ (𝑧 = (𝑤 + 1) → (𝑦 < 𝑧 ↔ 𝑦 < (𝑤 + 1))) |
8 | 7 | imbi1d 230 |
. . . 4
⊢ (𝑧 = (𝑤 + 1) → ((𝑦 < 𝑧 → 𝜓) ↔ (𝑦 < (𝑤 + 1) → 𝜓))) |
9 | 8 | ralbidv 2470 |
. . 3
⊢ (𝑧 = (𝑤 + 1) → (∀𝑦 ∈ ℕ (𝑦 < 𝑧 → 𝜓) ↔ ∀𝑦 ∈ ℕ (𝑦 < (𝑤 + 1) → 𝜓))) |
10 | | breq2 3993 |
. . . . 5
⊢ (𝑧 = 𝑥 → (𝑦 < 𝑧 ↔ 𝑦 < 𝑥)) |
11 | 10 | imbi1d 230 |
. . . 4
⊢ (𝑧 = 𝑥 → ((𝑦 < 𝑧 → 𝜓) ↔ (𝑦 < 𝑥 → 𝜓))) |
12 | 11 | ralbidv 2470 |
. . 3
⊢ (𝑧 = 𝑥 → (∀𝑦 ∈ ℕ (𝑦 < 𝑧 → 𝜓) ↔ ∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓))) |
13 | | nnnlt1 8904 |
. . . . 5
⊢ (𝑦 ∈ ℕ → ¬
𝑦 < 1) |
14 | 13 | pm2.21d 614 |
. . . 4
⊢ (𝑦 ∈ ℕ → (𝑦 < 1 → 𝜓)) |
15 | 14 | rgen 2523 |
. . 3
⊢
∀𝑦 ∈
ℕ (𝑦 < 1 →
𝜓) |
16 | | 1nn 8889 |
. . . . 5
⊢ 1 ∈
ℕ |
17 | | elex2 2746 |
. . . . 5
⊢ (1 ∈
ℕ → ∃𝑢
𝑢 ∈
ℕ) |
18 | | nfra1 2501 |
. . . . . 6
⊢
Ⅎ𝑦∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) |
19 | 18 | r19.3rm 3503 |
. . . . 5
⊢
(∃𝑢 𝑢 ∈ ℕ →
(∀𝑦 ∈ ℕ
(𝑦 < 𝑤 → 𝜓) ↔ ∀𝑦 ∈ ℕ ∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓))) |
20 | 16, 17, 19 | mp2b 8 |
. . . 4
⊢
(∀𝑦 ∈
ℕ (𝑦 < 𝑤 → 𝜓) ↔ ∀𝑦 ∈ ℕ ∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓)) |
21 | | rsp 2517 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
ℕ (𝑦 < 𝑤 → 𝜓) → (𝑦 ∈ ℕ → (𝑦 < 𝑤 → 𝜓))) |
22 | 21 | com12 30 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
(∀𝑦 ∈ ℕ
(𝑦 < 𝑤 → 𝜓) → (𝑦 < 𝑤 → 𝜓))) |
23 | 22 | adantl 275 |
. . . . . . . 8
⊢ ((𝑤 ∈ ℕ ∧ 𝑦 ∈ ℕ) →
(∀𝑦 ∈ ℕ
(𝑦 < 𝑤 → 𝜓) → (𝑦 < 𝑤 → 𝜓))) |
24 | | indstr.2 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ →
(∀𝑦 ∈ ℕ
(𝑦 < 𝑥 → 𝜓) → 𝜑)) |
25 | 24 | rgen 2523 |
. . . . . . . . . . . 12
⊢
∀𝑥 ∈
ℕ (∀𝑦 ∈
ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑) |
26 | | nfv 1521 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑤(∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑) |
27 | | nfv 1521 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) |
28 | | nfsbc1v 2973 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥[𝑤 / 𝑥]𝜑 |
29 | 27, 28 | nfim 1565 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → [𝑤 / 𝑥]𝜑) |
30 | | breq2 3993 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑤 → (𝑦 < 𝑥 ↔ 𝑦 < 𝑤)) |
31 | 30 | imbi1d 230 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → ((𝑦 < 𝑥 → 𝜓) ↔ (𝑦 < 𝑤 → 𝜓))) |
32 | 31 | ralbidv 2470 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) ↔ ∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓))) |
33 | | sbceq1a 2964 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑥]𝜑)) |
34 | 32, 33 | imbi12d 233 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → ((∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑) ↔ (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → [𝑤 / 𝑥]𝜑))) |
35 | 26, 29, 34 | cbvral 2692 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
ℕ (∀𝑦 ∈
ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑) ↔ ∀𝑤 ∈ ℕ (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → [𝑤 / 𝑥]𝜑)) |
36 | 25, 35 | mpbi 144 |
. . . . . . . . . . 11
⊢
∀𝑤 ∈
ℕ (∀𝑦 ∈
ℕ (𝑦 < 𝑤 → 𝜓) → [𝑤 / 𝑥]𝜑) |
37 | 36 | rspec 2522 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℕ →
(∀𝑦 ∈ ℕ
(𝑦 < 𝑤 → 𝜓) → [𝑤 / 𝑥]𝜑)) |
38 | | vex 2733 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
39 | | indstr.1 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
40 | 38, 39 | sbcie 2989 |
. . . . . . . . . . . 12
⊢
([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
41 | | dfsbcq 2957 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → ([𝑦 / 𝑥]𝜑 ↔ [𝑤 / 𝑥]𝜑)) |
42 | 40, 41 | bitr3id 193 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑥]𝜑)) |
43 | 42 | biimprcd 159 |
. . . . . . . . . 10
⊢
([𝑤 / 𝑥]𝜑 → (𝑦 = 𝑤 → 𝜓)) |
44 | 37, 43 | syl6 33 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℕ →
(∀𝑦 ∈ ℕ
(𝑦 < 𝑤 → 𝜓) → (𝑦 = 𝑤 → 𝜓))) |
45 | 44 | adantr 274 |
. . . . . . . 8
⊢ ((𝑤 ∈ ℕ ∧ 𝑦 ∈ ℕ) →
(∀𝑦 ∈ ℕ
(𝑦 < 𝑤 → 𝜓) → (𝑦 = 𝑤 → 𝜓))) |
46 | 23, 45 | jcad 305 |
. . . . . . 7
⊢ ((𝑤 ∈ ℕ ∧ 𝑦 ∈ ℕ) →
(∀𝑦 ∈ ℕ
(𝑦 < 𝑤 → 𝜓) → ((𝑦 < 𝑤 → 𝜓) ∧ (𝑦 = 𝑤 → 𝜓)))) |
47 | | jaob 705 |
. . . . . . 7
⊢ (((𝑦 < 𝑤 ∨ 𝑦 = 𝑤) → 𝜓) ↔ ((𝑦 < 𝑤 → 𝜓) ∧ (𝑦 = 𝑤 → 𝜓))) |
48 | 46, 47 | syl6ibr 161 |
. . . . . 6
⊢ ((𝑤 ∈ ℕ ∧ 𝑦 ∈ ℕ) →
(∀𝑦 ∈ ℕ
(𝑦 < 𝑤 → 𝜓) → ((𝑦 < 𝑤 ∨ 𝑦 = 𝑤) → 𝜓))) |
49 | | nnleltp1 9271 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) → (𝑦 ≤ 𝑤 ↔ 𝑦 < (𝑤 + 1))) |
50 | | nnz 9231 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
51 | | nnz 9231 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℕ → 𝑤 ∈
ℤ) |
52 | | zleloe 9259 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℤ ∧ 𝑤 ∈ ℤ) → (𝑦 ≤ 𝑤 ↔ (𝑦 < 𝑤 ∨ 𝑦 = 𝑤))) |
53 | 50, 51, 52 | syl2an 287 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) → (𝑦 ≤ 𝑤 ↔ (𝑦 < 𝑤 ∨ 𝑦 = 𝑤))) |
54 | 49, 53 | bitr3d 189 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) → (𝑦 < (𝑤 + 1) ↔ (𝑦 < 𝑤 ∨ 𝑦 = 𝑤))) |
55 | 54 | ancoms 266 |
. . . . . . 7
⊢ ((𝑤 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑤 + 1) ↔ (𝑦 < 𝑤 ∨ 𝑦 = 𝑤))) |
56 | 55 | imbi1d 230 |
. . . . . 6
⊢ ((𝑤 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑦 < (𝑤 + 1) → 𝜓) ↔ ((𝑦 < 𝑤 ∨ 𝑦 = 𝑤) → 𝜓))) |
57 | 48, 56 | sylibrd 168 |
. . . . 5
⊢ ((𝑤 ∈ ℕ ∧ 𝑦 ∈ ℕ) →
(∀𝑦 ∈ ℕ
(𝑦 < 𝑤 → 𝜓) → (𝑦 < (𝑤 + 1) → 𝜓))) |
58 | 57 | ralimdva 2537 |
. . . 4
⊢ (𝑤 ∈ ℕ →
(∀𝑦 ∈ ℕ
∀𝑦 ∈ ℕ
(𝑦 < 𝑤 → 𝜓) → ∀𝑦 ∈ ℕ (𝑦 < (𝑤 + 1) → 𝜓))) |
59 | 20, 58 | syl5bi 151 |
. . 3
⊢ (𝑤 ∈ ℕ →
(∀𝑦 ∈ ℕ
(𝑦 < 𝑤 → 𝜓) → ∀𝑦 ∈ ℕ (𝑦 < (𝑤 + 1) → 𝜓))) |
60 | 3, 6, 9, 12, 15, 59 | nnind 8894 |
. 2
⊢ (𝑥 ∈ ℕ →
∀𝑦 ∈ ℕ
(𝑦 < 𝑥 → 𝜓)) |
61 | 60, 24 | mpd 13 |
1
⊢ (𝑥 ∈ ℕ → 𝜑) |