Step | Hyp | Ref
| Expression |
1 | | elnn0 9130 |
. 2
⊢ (𝐴 ∈ ℕ0
↔ (𝐴 ∈ ℕ
∨ 𝐴 =
0)) |
2 | | dfsbcq2 2958 |
. . . 4
⊢ (𝑧 = 1 → ([𝑧 / 𝑥]𝜑 ↔ [1 / 𝑥]𝜑)) |
3 | | nfv 1521 |
. . . . 5
⊢
Ⅎ𝑥𝜒 |
4 | | nn0ind-raph.2 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
5 | 3, 4 | sbhypf 2779 |
. . . 4
⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ 𝜒)) |
6 | | nfv 1521 |
. . . . 5
⊢
Ⅎ𝑥𝜃 |
7 | | nn0ind-raph.3 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) |
8 | 6, 7 | sbhypf 2779 |
. . . 4
⊢ (𝑧 = (𝑦 + 1) → ([𝑧 / 𝑥]𝜑 ↔ 𝜃)) |
9 | | nfv 1521 |
. . . . 5
⊢
Ⅎ𝑥𝜏 |
10 | | nn0ind-raph.4 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) |
11 | 9, 10 | sbhypf 2779 |
. . . 4
⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝜑 ↔ 𝜏)) |
12 | | nfsbc1v 2973 |
. . . . 5
⊢
Ⅎ𝑥[1 /
𝑥]𝜑 |
13 | | 1ex 7908 |
. . . . 5
⊢ 1 ∈
V |
14 | | c0ex 7907 |
. . . . . . 7
⊢ 0 ∈
V |
15 | | 0nn0 9143 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 |
16 | | eleq1a 2242 |
. . . . . . . . . . . 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 167 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 0 → 𝜑) |
21 | | eqeq2 2180 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 0 → (𝑥 = 𝑦 ↔ 𝑥 = 0)) |
22 | 21, 4 | syl6bir 163 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 0 → (𝑥 = 0 → (𝜑 ↔ 𝜒))) |
23 | 22 | pm5.74d 181 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 0 → ((𝑥 = 0 → 𝜑) ↔ (𝑥 = 0 → 𝜒))) |
24 | 20, 23 | mpbii 147 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 0 → (𝑥 = 0 → 𝜒)) |
25 | 24 | com12 30 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → (𝑦 = 0 → 𝜒)) |
26 | 14, 25 | vtocle 2804 |
. . . . . . . . . . 11
⊢ (𝑦 = 0 → 𝜒) |
27 | | nn0ind-raph.6 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ (𝜒 → 𝜃)) |
28 | 17, 26, 27 | sylc 62 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → 𝜃) |
29 | 28 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑦 = 0 ∧ 𝑥 = 1) → 𝜃) |
30 | | oveq1 5858 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 0 → (𝑦 + 1) = (0 + 1)) |
31 | | 0p1e1 8985 |
. . . . . . . . . . . . 13
⊢ (0 + 1) =
1 |
32 | 30, 31 | eqtrdi 2219 |
. . . . . . . . . . . 12
⊢ (𝑦 = 0 → (𝑦 + 1) = 1) |
33 | 32 | eqeq2d 2182 |
. . . . . . . . . . 11
⊢ (𝑦 = 0 → (𝑥 = (𝑦 + 1) ↔ 𝑥 = 1)) |
34 | 33, 7 | syl6bir 163 |
. . . . . . . . . 10
⊢ (𝑦 = 0 → (𝑥 = 1 → (𝜑 ↔ 𝜃))) |
35 | 34 | imp 123 |
. . . . . . . . 9
⊢ ((𝑦 = 0 ∧ 𝑥 = 1) → (𝜑 ↔ 𝜃)) |
36 | 29, 35 | mpbird 166 |
. . . . . . . 8
⊢ ((𝑦 = 0 ∧ 𝑥 = 1) → 𝜑) |
37 | 36 | ex 114 |
. . . . . . 7
⊢ (𝑦 = 0 → (𝑥 = 1 → 𝜑)) |
38 | 14, 37 | vtocle 2804 |
. . . . . 6
⊢ (𝑥 = 1 → 𝜑) |
39 | | sbceq1a 2964 |
. . . . . 6
⊢ (𝑥 = 1 → (𝜑 ↔ [1 / 𝑥]𝜑)) |
40 | 38, 39 | mpbid 146 |
. . . . 5
⊢ (𝑥 = 1 → [1 / 𝑥]𝜑) |
41 | 12, 13, 40 | vtoclef 2803 |
. . . 4
⊢ [1
/ 𝑥]𝜑 |
42 | | nnnn0 9135 |
. . . . 5
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
43 | 42, 27 | syl 14 |
. . . 4
⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃)) |
44 | 2, 5, 8, 11, 41, 43 | nnind 8887 |
. . 3
⊢ (𝐴 ∈ ℕ → 𝜏) |
45 | | nfv 1521 |
. . . . 5
⊢
Ⅎ𝑥(0 = 𝐴 → 𝜏) |
46 | | eqeq1 2177 |
. . . . . 6
⊢ (𝑥 = 0 → (𝑥 = 𝐴 ↔ 0 = 𝐴)) |
47 | 19 | bicomd 140 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝜓 ↔ 𝜑)) |
48 | 47, 10 | sylan9bb 459 |
. . . . . . . 8
⊢ ((𝑥 = 0 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜏)) |
49 | 18, 48 | mpbii 147 |
. . . . . . 7
⊢ ((𝑥 = 0 ∧ 𝑥 = 𝐴) → 𝜏) |
50 | 49 | ex 114 |
. . . . . 6
⊢ (𝑥 = 0 → (𝑥 = 𝐴 → 𝜏)) |
51 | 46, 50 | sylbird 169 |
. . . . 5
⊢ (𝑥 = 0 → (0 = 𝐴 → 𝜏)) |
52 | 45, 14, 51 | vtoclef 2803 |
. . . 4
⊢ (0 =
𝐴 → 𝜏) |
53 | 52 | eqcoms 2173 |
. . 3
⊢ (𝐴 = 0 → 𝜏) |
54 | 44, 53 | jaoi 711 |
. 2
⊢ ((𝐴 ∈ ℕ ∨ 𝐴 = 0) → 𝜏) |
55 | 1, 54 | sylbi 120 |
1
⊢ (𝐴 ∈ ℕ0
→ 𝜏) |