Step |
Hyp |
Ref |
Expression |
1 |
|
nn0ind-raph.1 |
⊢ ( 𝑥 = 0 → ( 𝜑 ↔ 𝜓 ) ) |
2 |
|
nn0ind-raph.2 |
⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) ) |
3 |
|
nn0ind-raph.3 |
⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) ) |
4 |
|
nn0ind-raph.4 |
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) ) |
5 |
|
nn0ind-raph.5 |
⊢ 𝜓 |
6 |
|
nn0ind-raph.6 |
⊢ ( 𝑦 ∈ ℕ0 → ( 𝜒 → 𝜃 ) ) |
7 |
|
elnn0 |
⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) ) |
8 |
|
dfsbcq2 |
⊢ ( 𝑧 = 1 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 1 / 𝑥 ] 𝜑 ) ) |
9 |
|
nfv |
⊢ Ⅎ 𝑥 𝜒 |
10 |
9 2
|
sbhypf |
⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜒 ) ) |
11 |
|
nfv |
⊢ Ⅎ 𝑥 𝜃 |
12 |
11 3
|
sbhypf |
⊢ ( 𝑧 = ( 𝑦 + 1 ) → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜃 ) ) |
13 |
|
nfv |
⊢ Ⅎ 𝑥 𝜏 |
14 |
13 4
|
sbhypf |
⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜏 ) ) |
15 |
|
nfsbc1v |
⊢ Ⅎ 𝑥 [ 1 / 𝑥 ] 𝜑 |
16 |
|
1ex |
⊢ 1 ∈ V |
17 |
|
c0ex |
⊢ 0 ∈ V |
18 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
19 |
|
eleq1a |
⊢ ( 0 ∈ ℕ0 → ( 𝑦 = 0 → 𝑦 ∈ ℕ0 ) ) |
20 |
18 19
|
ax-mp |
⊢ ( 𝑦 = 0 → 𝑦 ∈ ℕ0 ) |
21 |
5 1
|
mpbiri |
⊢ ( 𝑥 = 0 → 𝜑 ) |
22 |
|
eqeq2 |
⊢ ( 𝑦 = 0 → ( 𝑥 = 𝑦 ↔ 𝑥 = 0 ) ) |
23 |
22 2
|
syl6bir |
⊢ ( 𝑦 = 0 → ( 𝑥 = 0 → ( 𝜑 ↔ 𝜒 ) ) ) |
24 |
23
|
pm5.74d |
⊢ ( 𝑦 = 0 → ( ( 𝑥 = 0 → 𝜑 ) ↔ ( 𝑥 = 0 → 𝜒 ) ) ) |
25 |
21 24
|
mpbii |
⊢ ( 𝑦 = 0 → ( 𝑥 = 0 → 𝜒 ) ) |
26 |
25
|
com12 |
⊢ ( 𝑥 = 0 → ( 𝑦 = 0 → 𝜒 ) ) |
27 |
17 26
|
vtocle |
⊢ ( 𝑦 = 0 → 𝜒 ) |
28 |
20 27 6
|
sylc |
⊢ ( 𝑦 = 0 → 𝜃 ) |
29 |
28
|
adantr |
⊢ ( ( 𝑦 = 0 ∧ 𝑥 = 1 ) → 𝜃 ) |
30 |
|
oveq1 |
⊢ ( 𝑦 = 0 → ( 𝑦 + 1 ) = ( 0 + 1 ) ) |
31 |
|
0p1e1 |
⊢ ( 0 + 1 ) = 1 |
32 |
30 31
|
eqtrdi |
⊢ ( 𝑦 = 0 → ( 𝑦 + 1 ) = 1 ) |
33 |
32
|
eqeq2d |
⊢ ( 𝑦 = 0 → ( 𝑥 = ( 𝑦 + 1 ) ↔ 𝑥 = 1 ) ) |
34 |
33 3
|
syl6bir |
⊢ ( 𝑦 = 0 → ( 𝑥 = 1 → ( 𝜑 ↔ 𝜃 ) ) ) |
35 |
34
|
imp |
⊢ ( ( 𝑦 = 0 ∧ 𝑥 = 1 ) → ( 𝜑 ↔ 𝜃 ) ) |
36 |
29 35
|
mpbird |
⊢ ( ( 𝑦 = 0 ∧ 𝑥 = 1 ) → 𝜑 ) |
37 |
36
|
ex |
⊢ ( 𝑦 = 0 → ( 𝑥 = 1 → 𝜑 ) ) |
38 |
17 37
|
vtocle |
⊢ ( 𝑥 = 1 → 𝜑 ) |
39 |
|
sbceq1a |
⊢ ( 𝑥 = 1 → ( 𝜑 ↔ [ 1 / 𝑥 ] 𝜑 ) ) |
40 |
38 39
|
mpbid |
⊢ ( 𝑥 = 1 → [ 1 / 𝑥 ] 𝜑 ) |
41 |
15 16 40
|
vtoclef |
⊢ [ 1 / 𝑥 ] 𝜑 |
42 |
|
nnnn0 |
⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℕ0 ) |
43 |
42 6
|
syl |
⊢ ( 𝑦 ∈ ℕ → ( 𝜒 → 𝜃 ) ) |
44 |
8 10 12 14 41 43
|
nnind |
⊢ ( 𝐴 ∈ ℕ → 𝜏 ) |
45 |
|
nfv |
⊢ Ⅎ 𝑥 ( 0 = 𝐴 → 𝜏 ) |
46 |
|
eqeq1 |
⊢ ( 𝑥 = 0 → ( 𝑥 = 𝐴 ↔ 0 = 𝐴 ) ) |
47 |
1
|
bicomd |
⊢ ( 𝑥 = 0 → ( 𝜓 ↔ 𝜑 ) ) |
48 |
47 4
|
sylan9bb |
⊢ ( ( 𝑥 = 0 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜏 ) ) |
49 |
5 48
|
mpbii |
⊢ ( ( 𝑥 = 0 ∧ 𝑥 = 𝐴 ) → 𝜏 ) |
50 |
49
|
ex |
⊢ ( 𝑥 = 0 → ( 𝑥 = 𝐴 → 𝜏 ) ) |
51 |
46 50
|
sylbird |
⊢ ( 𝑥 = 0 → ( 0 = 𝐴 → 𝜏 ) ) |
52 |
45 17 51
|
vtoclef |
⊢ ( 0 = 𝐴 → 𝜏 ) |
53 |
52
|
eqcoms |
⊢ ( 𝐴 = 0 → 𝜏 ) |
54 |
44 53
|
jaoi |
⊢ ( ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) → 𝜏 ) |
55 |
7 54
|
sylbi |
⊢ ( 𝐴 ∈ ℕ0 → 𝜏 ) |