Step | Hyp | Ref
| Expression |
1 | | dfnn2 7697 |
. . . . . 6
⊢ ℕ =
∩ {x ∣ (1
∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} |
2 | 1 | eleq2i 2101 |
. . . . 5
⊢ (A ∈ ℕ ↔
A ∈ ∩ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}) |
3 | | elintg 3614 |
. . . . 5
⊢ (A ∈ ℕ →
(A ∈
∩ {x ∣ (1
∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} ↔
∀z
∈ {x
∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}A ∈ z)) |
4 | 2, 3 | syl5bb 181 |
. . . 4
⊢ (A ∈ ℕ →
(A ∈
ℕ ↔ ∀z ∈ {x ∣ (1 ∈
x ∧ ∀y ∈ x (y + 1) ∈ x)}A ∈ z)) |
5 | 4 | ibi 165 |
. . 3
⊢ (A ∈ ℕ →
∀z
∈ {x
∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}A ∈ z) |
6 | | vex 2554 |
. . . . . . . 8
⊢ z ∈
V |
7 | | eleq2 2098 |
. . . . . . . . 9
⊢ (x = z → (1
∈ x
↔ 1 ∈ z)) |
8 | | eleq2 2098 |
. . . . . . . . . 10
⊢ (x = z →
((y + 1) ∈ x ↔
(y + 1) ∈
z)) |
9 | 8 | raleqbi1dv 2507 |
. . . . . . . . 9
⊢ (x = z →
(∀y
∈ x
(y + 1) ∈
x ↔ ∀y ∈ z (y + 1) ∈ z)) |
10 | 7, 9 | anbi12d 442 |
. . . . . . . 8
⊢ (x = z → ((1
∈ x ∧ ∀y ∈ x (y + 1) ∈ x) ↔ (1
∈ z ∧ ∀y ∈ z (y + 1) ∈ z))) |
11 | 6, 10 | elab 2681 |
. . . . . . 7
⊢ (z ∈ {x ∣ (1 ∈
x ∧ ∀y ∈ x (y + 1) ∈ x)} ↔ (1 ∈
z ∧ ∀y ∈ z (y + 1) ∈ z)) |
12 | 11 | simprbi 260 |
. . . . . 6
⊢ (z ∈ {x ∣ (1 ∈
x ∧ ∀y ∈ x (y + 1) ∈ x)} → ∀y ∈ z (y + 1) ∈ z) |
13 | | oveq1 5462 |
. . . . . . . 8
⊢ (y = A →
(y + 1) = (A + 1)) |
14 | 13 | eleq1d 2103 |
. . . . . . 7
⊢ (y = A →
((y + 1) ∈ z ↔
(A + 1) ∈
z)) |
15 | 14 | rspcva 2648 |
. . . . . 6
⊢
((A ∈ z ∧ ∀y ∈ z (y + 1) ∈ z) →
(A + 1) ∈
z) |
16 | 12, 15 | sylan2 270 |
. . . . 5
⊢
((A ∈ z ∧ z ∈ {x ∣ (1
∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}) →
(A + 1) ∈
z) |
17 | 16 | expcom 109 |
. . . 4
⊢ (z ∈ {x ∣ (1 ∈
x ∧ ∀y ∈ x (y + 1) ∈ x)} → (A
∈ z
→ (A + 1) ∈ z)) |
18 | 17 | ralimia 2376 |
. . 3
⊢ (∀z ∈ {x ∣ (1
∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}A ∈ z → ∀z ∈ {x ∣ (1
∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} (A + 1) ∈ z) |
19 | 5, 18 | syl 14 |
. 2
⊢ (A ∈ ℕ →
∀z
∈ {x
∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} (A + 1)
∈ z) |
20 | | nnre 7702 |
. . . 4
⊢ (A ∈ ℕ →
A ∈
ℝ) |
21 | | 1red 6840 |
. . . 4
⊢ (A ∈ ℕ →
1 ∈ ℝ) |
22 | 20, 21 | readdcld 6852 |
. . 3
⊢ (A ∈ ℕ →
(A + 1) ∈
ℝ) |
23 | 1 | eleq2i 2101 |
. . . 4
⊢
((A + 1) ∈ ℕ ↔ (A + 1) ∈ ∩ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}) |
24 | | elintg 3614 |
. . . 4
⊢
((A + 1) ∈ ℝ → ((A + 1) ∈ ∩ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} ↔
∀z
∈ {x
∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} (A + 1)
∈ z)) |
25 | 23, 24 | syl5bb 181 |
. . 3
⊢
((A + 1) ∈ ℝ → ((A + 1) ∈ ℕ
↔ ∀z ∈ {x ∣ (1 ∈
x ∧ ∀y ∈ x (y + 1) ∈ x)} (A + 1)
∈ z)) |
26 | 22, 25 | syl 14 |
. 2
⊢ (A ∈ ℕ →
((A + 1) ∈ ℕ ↔ ∀z ∈ {x ∣ (1
∈ x ∧ ∀y ∈ x (y + 1) ∈ x)} (A + 1) ∈ z)) |
27 | 19, 26 | mpbird 156 |
1
⊢ (A ∈ ℕ →
(A + 1) ∈
ℕ) |