| Step | Hyp | Ref
| Expression |
| 1 | | elnn0 12528 |
. 2
⊢ (𝐴 ∈ ℕ0
↔ (𝐴 ∈ ℕ
∨ 𝐴 =
0)) |
| 2 | | dfsbcq2 3791 |
. . . 4
⊢ (𝑧 = 1 → ([𝑧 / 𝑥]𝜑 ↔ [1 / 𝑥]𝜑)) |
| 3 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑥𝜒 |
| 4 | | nn0ind-raph.2 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
| 5 | 3, 4 | sbhypf 3544 |
. . . 4
⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ 𝜒)) |
| 6 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑥𝜃 |
| 7 | | nn0ind-raph.3 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) |
| 8 | 6, 7 | sbhypf 3544 |
. . . 4
⊢ (𝑧 = (𝑦 + 1) → ([𝑧 / 𝑥]𝜑 ↔ 𝜃)) |
| 9 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑥𝜏 |
| 10 | | nn0ind-raph.4 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) |
| 11 | 9, 10 | sbhypf 3544 |
. . . 4
⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝜑 ↔ 𝜏)) |
| 12 | | nfsbc1v 3808 |
. . . . 5
⊢
Ⅎ𝑥[1 /
𝑥]𝜑 |
| 13 | | 1ex 11257 |
. . . . 5
⊢ 1 ∈
V |
| 14 | | c0ex 11255 |
. . . . . . 7
⊢ 0 ∈
V |
| 15 | | 0nn0 12541 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 |
| 16 | | eleq1a 2836 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℕ0 → (𝑦 = 0 → 𝑦 ∈
ℕ0)) |
| 17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑦 = 0 → 𝑦 ∈ ℕ0) |
| 18 | | nn0ind-raph.5 |
. . . . . . . . . . . . . . 15
⊢ 𝜓 |
| 19 | | nn0ind-raph.1 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 0 → (𝜑 ↔ 𝜓)) |
| 20 | 18, 19 | mpbiri 258 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 0 → 𝜑) |
| 21 | | eqeq2 2749 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 0 → (𝑥 = 𝑦 ↔ 𝑥 = 0)) |
| 22 | 21, 4 | biimtrrdi 254 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 0 → (𝑥 = 0 → (𝜑 ↔ 𝜒))) |
| 23 | 22 | pm5.74d 273 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 0 → ((𝑥 = 0 → 𝜑) ↔ (𝑥 = 0 → 𝜒))) |
| 24 | 20, 23 | mpbii 233 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 0 → (𝑥 = 0 → 𝜒)) |
| 25 | 24 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → (𝑦 = 0 → 𝜒)) |
| 26 | 14, 25 | vtocle 3555 |
. . . . . . . . . . 11
⊢ (𝑦 = 0 → 𝜒) |
| 27 | | nn0ind-raph.6 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ (𝜒 → 𝜃)) |
| 28 | 17, 26, 27 | sylc 65 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → 𝜃) |
| 29 | 28 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑦 = 0 ∧ 𝑥 = 1) → 𝜃) |
| 30 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 0 → (𝑦 + 1) = (0 + 1)) |
| 31 | | 0p1e1 12388 |
. . . . . . . . . . . . 13
⊢ (0 + 1) =
1 |
| 32 | 30, 31 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝑦 = 0 → (𝑦 + 1) = 1) |
| 33 | 32 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑦 = 0 → (𝑥 = (𝑦 + 1) ↔ 𝑥 = 1)) |
| 34 | 33, 7 | biimtrrdi 254 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → (𝑥 = 1 → (𝜑 ↔ 𝜃))) |
| 35 | 34 | imp 406 |
. . . . . . . . 9
⊢ ((𝑦 = 0 ∧ 𝑥 = 1) → (𝜑 ↔ 𝜃)) |
| 36 | 29, 35 | mpbird 257 |
. . . . . . . 8
⊢ ((𝑦 = 0 ∧ 𝑥 = 1) → 𝜑) |
| 37 | 36 | ex 412 |
. . . . . . 7
⊢ (𝑦 = 0 → (𝑥 = 1 → 𝜑)) |
| 38 | 14, 37 | vtocle 3555 |
. . . . . 6
⊢ (𝑥 = 1 → 𝜑) |
| 39 | | sbceq1a 3799 |
. . . . . 6
⊢ (𝑥 = 1 → (𝜑 ↔ [1 / 𝑥]𝜑)) |
| 40 | 38, 39 | mpbid 232 |
. . . . 5
⊢ (𝑥 = 1 → [1 / 𝑥]𝜑) |
| 41 | 12, 13, 40 | vtoclef 3563 |
. . . 4
⊢ [1
/ 𝑥]𝜑 |
| 42 | | nnnn0 12533 |
. . . . 5
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
| 43 | 42, 27 | syl 17 |
. . . 4
⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃)) |
| 44 | 2, 5, 8, 11, 41, 43 | nnind 12284 |
. . 3
⊢ (𝐴 ∈ ℕ → 𝜏) |
| 45 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑥(0 = 𝐴 → 𝜏) |
| 46 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑥 = 0 → (𝑥 = 𝐴 ↔ 0 = 𝐴)) |
| 47 | 19 | bicomd 223 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝜓 ↔ 𝜑)) |
| 48 | 47, 10 | sylan9bb 509 |
. . . . . . . 8
⊢ ((𝑥 = 0 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜏)) |
| 49 | 18, 48 | mpbii 233 |
. . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑥 = 𝐴) → 𝜏) |
| 50 | 49 | ex 412 |
. . . . . 6
⊢ (𝑥 = 0 → (𝑥 = 𝐴 → 𝜏)) |
| 51 | 46, 50 | sylbird 260 |
. . . . 5
⊢ (𝑥 = 0 → (0 = 𝐴 → 𝜏)) |
| 52 | 45, 14, 51 | vtoclef 3563 |
. . . 4
⊢ (0 =
𝐴 → 𝜏) |
| 53 | 52 | eqcoms 2745 |
. . 3
⊢ (𝐴 = 0 → 𝜏) |
| 54 | 44, 53 | jaoi 858 |
. 2
⊢ ((𝐴 ∈ ℕ ∨ 𝐴 = 0) → 𝜏) |
| 55 | 1, 54 | sylbi 217 |
1
⊢ (𝐴 ∈ ℕ0
→ 𝜏) |