Step | Hyp | Ref
| Expression |
1 | | bi2 121 |
. . . . 5
⊢
((x ∈ A ↔
(x = ∅
∨ ∃y ∈ A x = suc
y)) → ((x = ∅ ∨ ∃y ∈ A x = suc y)
→ x ∈ A)) |
2 | | ax-io 629 |
. . . . . 6
⊢
(((x = ∅ ∨ ∃y ∈ A x = suc
y) → x ∈ A) ↔ ((x =
∅ → x ∈ A) ∧ (∃y ∈ A x = suc
y → x ∈ A))) |
3 | 2 | biimpi 113 |
. . . . 5
⊢
(((x = ∅ ∨ ∃y ∈ A x = suc
y) → x ∈ A) → ((x =
∅ → x ∈ A) ∧ (∃y ∈ A x = suc
y → x ∈ A))) |
4 | | simpl 102 |
. . . . . 6
⊢
(((x = ∅ → x ∈ A) ∧ (∃y ∈ A x = suc y →
x ∈
A)) → (x = ∅ → x ∈ A)) |
5 | | eleq1 2097 |
. . . . . 6
⊢ (x = ∅ → (x ∈ A ↔ ∅ ∈
A)) |
6 | 4, 5 | mpbidi 140 |
. . . . 5
⊢
(((x = ∅ → x ∈ A) ∧ (∃y ∈ A x = suc y →
x ∈
A)) → (x = ∅ → ∅ ∈ A)) |
7 | 1, 3, 6 | 3syl 17 |
. . . 4
⊢
((x ∈ A ↔
(x = ∅
∨ ∃y ∈ A x = suc
y)) → (x = ∅ → ∅ ∈ A)) |
8 | 7 | alimi 1341 |
. . 3
⊢ (∀x(x ∈ A ↔ (x =
∅ ∨ ∃y ∈ A x = suc y))
→ ∀x(x = ∅
→ ∅ ∈ A)) |
9 | | exim 1487 |
. . 3
⊢ (∀x(x = ∅ → ∅ ∈ A) →
(∃x
x = ∅ → ∃x∅
∈ A)) |
10 | | 0ex 3875 |
. . . . . 6
⊢ ∅
∈ V |
11 | 10 | isseti 2557 |
. . . . 5
⊢ ∃x x = ∅ |
12 | | pm2.27 35 |
. . . . 5
⊢ (∃x x = ∅ → ((∃x x = ∅ → ∃x∅
∈ A)
→ ∃x∅ ∈
A)) |
13 | 11, 12 | ax-mp 7 |
. . . 4
⊢ ((∃x x = ∅ → ∃x∅
∈ A)
→ ∃x∅ ∈
A) |
14 | | bj-ex 9237 |
. . . 4
⊢ (∃x∅
∈ A
→ ∅ ∈ A) |
15 | 13, 14 | syl 14 |
. . 3
⊢ ((∃x x = ∅ → ∃x∅
∈ A)
→ ∅ ∈ A) |
16 | 8, 9, 15 | 3syl 17 |
. 2
⊢ (∀x(x ∈ A ↔ (x =
∅ ∨ ∃y ∈ A x = suc y))
→ ∅ ∈ A) |
17 | 3 | simprd 107 |
. . . . . 6
⊢
(((x = ∅ ∨ ∃y ∈ A x = suc
y) → x ∈ A) → (∃y ∈ A x = suc y →
x ∈
A)) |
18 | 1, 17 | syl 14 |
. . . . 5
⊢
((x ∈ A ↔
(x = ∅
∨ ∃y ∈ A x = suc
y)) → (∃y ∈ A x = suc y →
x ∈
A)) |
19 | 18 | alimi 1341 |
. . . 4
⊢ (∀x(x ∈ A ↔ (x =
∅ ∨ ∃y ∈ A x = suc y))
→ ∀x(∃y ∈ A x = suc
y → x ∈ A)) |
20 | | eqid 2037 |
. . . . 5
⊢ suc
z = suc z |
21 | | suceq 4105 |
. . . . . . 7
⊢ (y = z → suc
y = suc z) |
22 | 21 | eqeq2d 2048 |
. . . . . 6
⊢ (y = z →
(suc z = suc y ↔ suc z =
suc z)) |
23 | 22 | rspcev 2650 |
. . . . 5
⊢
((z ∈ A ∧ suc z = suc
z) → ∃y ∈ A suc
z = suc y) |
24 | 20, 23 | mpan2 401 |
. . . 4
⊢ (z ∈ A → ∃y ∈ A suc
z = suc y) |
25 | | vex 2554 |
. . . . . 6
⊢ z ∈
V |
26 | 25 | bj-sucex 9378 |
. . . . 5
⊢ suc
z ∈
V |
27 | | eqeq1 2043 |
. . . . . . 7
⊢ (x = suc z →
(x = suc y ↔ suc z =
suc y)) |
28 | 27 | rexbidv 2321 |
. . . . . 6
⊢ (x = suc z →
(∃y
∈ A
x = suc y ↔ ∃y ∈ A suc
z = suc y)) |
29 | | eleq1 2097 |
. . . . . 6
⊢ (x = suc z →
(x ∈
A ↔ suc z ∈ A)) |
30 | 28, 29 | imbi12d 223 |
. . . . 5
⊢ (x = suc z →
((∃y
∈ A
x = suc y → x ∈ A) ↔
(∃y
∈ A suc
z = suc y → suc z
∈ A))) |
31 | 26, 30 | spcv 2640 |
. . . 4
⊢ (∀x(∃y ∈ A x = suc y →
x ∈
A) → (∃y ∈ A suc
z = suc y → suc z
∈ A)) |
32 | 19, 24, 31 | syl2im 34 |
. . 3
⊢ (∀x(x ∈ A ↔ (x =
∅ ∨ ∃y ∈ A x = suc y))
→ (z ∈ A → suc
z ∈
A)) |
33 | 32 | ralrimiv 2385 |
. 2
⊢ (∀x(x ∈ A ↔ (x =
∅ ∨ ∃y ∈ A x = suc y))
→ ∀z ∈ A suc z ∈ A) |
34 | | df-bj-ind 9386 |
. 2
⊢ (Ind
A ↔ (∅ ∈ A ∧ ∀z ∈ A suc z ∈ A)) |
35 | 16, 33, 34 | sylanbrc 394 |
1
⊢ (∀x(x ∈ A ↔ (x =
∅ ∨ ∃y ∈ A x = suc y))
→ Ind A) |