Step | Hyp | Ref
| Expression |
1 | | df-nn 11831 |
. . 3
⊢ ℕ =
(rec((𝑛 ∈ V ↦
(𝑛 + 1)), 1) “
ω) |
2 | | df-ima 5564 |
. . 3
⊢
(rec((𝑛 ∈ V
↦ (𝑛 + 1)), 1)
“ ω) = ran (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω) |
3 | 1, 2 | eqtri 2765 |
. 2
⊢ ℕ =
ran (rec((𝑛 ∈ V
↦ (𝑛 + 1)), 1)
↾ ω) |
4 | | frfnom 8170 |
. . . . 5
⊢
(rec((𝑛 ∈ V
↦ (𝑛 + 1)), 1)
↾ ω) Fn ω |
5 | 4 | a1i 11 |
. . . 4
⊢ ((1
∈ 𝐴 ∧
∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω) Fn
ω) |
6 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑦 = ∅ → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾
ω)‘𝑦) =
((rec((𝑛 ∈ V ↦
(𝑛 + 1)), 1) ↾
ω)‘∅)) |
7 | 6 | eleq1d 2822 |
. . . . . . 7
⊢ (𝑦 = ∅ → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾
ω)‘𝑦) ∈
𝐴 ↔ ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾
ω)‘∅) ∈ 𝐴)) |
8 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑦) = ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑧)) |
9 | 8 | eleq1d 2822 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑦) ∈ 𝐴 ↔ ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑧) ∈ 𝐴)) |
10 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑦 = suc 𝑧 → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑦) = ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘suc 𝑧)) |
11 | 10 | eleq1d 2822 |
. . . . . . 7
⊢ (𝑦 = suc 𝑧 → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑦) ∈ 𝐴 ↔ ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘suc 𝑧) ∈ 𝐴)) |
12 | | ax-1cn 10787 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
13 | | fr0g 8171 |
. . . . . . . . 9
⊢ (1 ∈
ℂ → ((rec((𝑛
∈ V ↦ (𝑛 + 1)),
1) ↾ ω)‘∅) = 1) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . 8
⊢
((rec((𝑛 ∈ V
↦ (𝑛 + 1)), 1)
↾ ω)‘∅) = 1 |
15 | | simpl 486 |
. . . . . . . 8
⊢ ((1
∈ 𝐴 ∧
∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → 1 ∈ 𝐴) |
16 | 14, 15 | eqeltrid 2842 |
. . . . . . 7
⊢ ((1
∈ 𝐴 ∧
∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘∅)
∈ 𝐴) |
17 | | oveq1 7220 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑧) → (𝑥 + 1) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑧) + 1)) |
18 | 17 | eleq1d 2822 |
. . . . . . . . . . 11
⊢ (𝑥 = ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑧) → ((𝑥 + 1) ∈ 𝐴 ↔ (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑧) + 1) ∈ 𝐴)) |
19 | 18 | rspccv 3534 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 (𝑥 + 1) ∈ 𝐴 → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑧) ∈ 𝐴 → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑧) + 1) ∈ 𝐴)) |
20 | 19 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((1
∈ 𝐴 ∧
∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) ∧ 𝑧 ∈ ω) → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾
ω)‘𝑧) ∈
𝐴 → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾
ω)‘𝑧) + 1)
∈ 𝐴)) |
21 | | ovex 7246 |
. . . . . . . . . . . 12
⊢
(((rec((𝑛 ∈ V
↦ (𝑛 + 1)), 1)
↾ ω)‘𝑧) +
1) ∈ V |
22 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(rec((𝑛 ∈ V
↦ (𝑛 + 1)), 1)
↾ ω) = (rec((𝑛
∈ V ↦ (𝑛 + 1)),
1) ↾ ω) |
23 | | oveq1 7220 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑛 → (𝑦 + 1) = (𝑛 + 1)) |
24 | | oveq1 7220 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑧) → (𝑦 + 1) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑧) + 1)) |
25 | 22, 23, 24 | frsucmpt2 8176 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ω ∧
(((rec((𝑛 ∈ V ↦
(𝑛 + 1)), 1) ↾
ω)‘𝑧) + 1)
∈ V) → ((rec((𝑛
∈ V ↦ (𝑛 + 1)),
1) ↾ ω)‘suc 𝑧) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑧) + 1)) |
26 | 21, 25 | mpan2 691 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ω →
((rec((𝑛 ∈ V ↦
(𝑛 + 1)), 1) ↾
ω)‘suc 𝑧) =
(((rec((𝑛 ∈ V ↦
(𝑛 + 1)), 1) ↾
ω)‘𝑧) +
1)) |
27 | 26 | eleq1d 2822 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ω →
(((rec((𝑛 ∈ V ↦
(𝑛 + 1)), 1) ↾
ω)‘suc 𝑧)
∈ 𝐴 ↔
(((rec((𝑛 ∈ V ↦
(𝑛 + 1)), 1) ↾
ω)‘𝑧) + 1)
∈ 𝐴)) |
28 | 27 | adantl 485 |
. . . . . . . . 9
⊢ (((1
∈ 𝐴 ∧
∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) ∧ 𝑧 ∈ ω) → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾
ω)‘suc 𝑧)
∈ 𝐴 ↔
(((rec((𝑛 ∈ V ↦
(𝑛 + 1)), 1) ↾
ω)‘𝑧) + 1)
∈ 𝐴)) |
29 | 20, 28 | sylibrd 262 |
. . . . . . . 8
⊢ (((1
∈ 𝐴 ∧
∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) ∧ 𝑧 ∈ ω) → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾
ω)‘𝑧) ∈
𝐴 → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾
ω)‘suc 𝑧)
∈ 𝐴)) |
30 | 29 | expcom 417 |
. . . . . . 7
⊢ (𝑧 ∈ ω → ((1
∈ 𝐴 ∧
∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑧) ∈ 𝐴 → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘suc 𝑧) ∈ 𝐴))) |
31 | 7, 9, 11, 16, 30 | finds2 7678 |
. . . . . 6
⊢ (𝑦 ∈ ω → ((1
∈ 𝐴 ∧
∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑦) ∈ 𝐴)) |
32 | 31 | com12 32 |
. . . . 5
⊢ ((1
∈ 𝐴 ∧
∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → (𝑦 ∈ ω → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾
ω)‘𝑦) ∈
𝐴)) |
33 | 32 | ralrimiv 3104 |
. . . 4
⊢ ((1
∈ 𝐴 ∧
∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → ∀𝑦 ∈ ω ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)‘𝑦) ∈ 𝐴) |
34 | | ffnfv 6935 |
. . . 4
⊢
((rec((𝑛 ∈ V
↦ (𝑛 + 1)), 1)
↾ ω):ω⟶𝐴 ↔ ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω) Fn ω ∧
∀𝑦 ∈ ω
((rec((𝑛 ∈ V ↦
(𝑛 + 1)), 1) ↾
ω)‘𝑦) ∈
𝐴)) |
35 | 5, 33, 34 | sylanbrc 586 |
. . 3
⊢ ((1
∈ 𝐴 ∧
∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾
ω):ω⟶𝐴) |
36 | 35 | frnd 6553 |
. 2
⊢ ((1
∈ 𝐴 ∧
∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → ran (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω) ⊆ 𝐴) |
37 | 3, 36 | eqsstrid 3949 |
1
⊢ ((1
∈ 𝐴 ∧
∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → ℕ ⊆ 𝐴) |