Step |
Hyp |
Ref |
Expression |
1 |
|
nnindf.x |
⊢ Ⅎ 𝑦 𝜑 |
2 |
|
nnindf.1 |
⊢ ( 𝑥 = 1 → ( 𝜑 ↔ 𝜓 ) ) |
3 |
|
nnindf.2 |
⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) ) |
4 |
|
nnindf.3 |
⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) ) |
5 |
|
nnindf.4 |
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) ) |
6 |
|
nnindf.5 |
⊢ 𝜓 |
7 |
|
nnindf.6 |
⊢ ( 𝑦 ∈ ℕ → ( 𝜒 → 𝜃 ) ) |
8 |
|
1nn |
⊢ 1 ∈ ℕ |
9 |
2
|
elrab |
⊢ ( 1 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( 1 ∈ ℕ ∧ 𝜓 ) ) |
10 |
8 6 9
|
mpbir2an |
⊢ 1 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } |
11 |
|
elrabi |
⊢ ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → 𝑦 ∈ ℕ ) |
12 |
|
peano2nn |
⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℕ ) |
13 |
12
|
a1d |
⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℕ ) ) |
14 |
13 7
|
anim12d |
⊢ ( 𝑦 ∈ ℕ → ( ( 𝑦 ∈ ℕ ∧ 𝜒 ) → ( ( 𝑦 + 1 ) ∈ ℕ ∧ 𝜃 ) ) ) |
15 |
3
|
elrab |
⊢ ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( 𝑦 ∈ ℕ ∧ 𝜒 ) ) |
16 |
4
|
elrab |
⊢ ( ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( ( 𝑦 + 1 ) ∈ ℕ ∧ 𝜃 ) ) |
17 |
14 15 16
|
3imtr4g |
⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ) ) |
18 |
11 17
|
mpcom |
⊢ ( 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } → ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ) |
19 |
18
|
rgen |
⊢ ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } |
20 |
|
nfcv |
⊢ Ⅎ 𝑦 ℕ |
21 |
1 20
|
nfrabw |
⊢ Ⅎ 𝑦 { 𝑥 ∈ ℕ ∣ 𝜑 } |
22 |
|
nfcv |
⊢ Ⅎ 𝑤 { 𝑥 ∈ ℕ ∣ 𝜑 } |
23 |
|
nfv |
⊢ Ⅎ 𝑤 ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } |
24 |
21
|
nfel2 |
⊢ Ⅎ 𝑦 ( 𝑤 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } |
25 |
|
oveq1 |
⊢ ( 𝑦 = 𝑤 → ( 𝑦 + 1 ) = ( 𝑤 + 1 ) ) |
26 |
25
|
eleq1d |
⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( 𝑤 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ) ) |
27 |
21 22 23 24 26
|
cbvralfw |
⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ( 𝑦 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ∀ 𝑤 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ( 𝑤 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ) |
28 |
19 27
|
mpbi |
⊢ ∀ 𝑤 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ( 𝑤 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } |
29 |
|
peano5nni |
⊢ ( ( 1 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ∧ ∀ 𝑤 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ( 𝑤 + 1 ) ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ) → ℕ ⊆ { 𝑥 ∈ ℕ ∣ 𝜑 } ) |
30 |
10 28 29
|
mp2an |
⊢ ℕ ⊆ { 𝑥 ∈ ℕ ∣ 𝜑 } |
31 |
30
|
sseli |
⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ) |
32 |
5
|
elrab |
⊢ ( 𝐴 ∈ { 𝑥 ∈ ℕ ∣ 𝜑 } ↔ ( 𝐴 ∈ ℕ ∧ 𝜏 ) ) |
33 |
31 32
|
sylib |
⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ∈ ℕ ∧ 𝜏 ) ) |
34 |
33
|
simprd |
⊢ ( 𝐴 ∈ ℕ → 𝜏 ) |