Step | Hyp | Ref
| Expression |
1 | | bi2 121 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → ((𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → 𝑥 ∈ 𝐴)) |
2 | | ax-io 630 |
. . . . . 6
⊢ (((𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → 𝑥 ∈ 𝐴) ↔ ((𝑥 = ∅ → 𝑥 ∈ 𝐴) ∧ (∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴))) |
3 | 2 | biimpi 113 |
. . . . 5
⊢ (((𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → 𝑥 ∈ 𝐴) → ((𝑥 = ∅ → 𝑥 ∈ 𝐴) ∧ (∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴))) |
4 | | simpl 102 |
. . . . . 6
⊢ (((𝑥 = ∅ → 𝑥 ∈ 𝐴) ∧ (∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴)) → (𝑥 = ∅ → 𝑥 ∈ 𝐴)) |
5 | | eleq1 2100 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑥 ∈ 𝐴 ↔ ∅ ∈ 𝐴)) |
6 | 4, 5 | mpbidi 140 |
. . . . 5
⊢ (((𝑥 = ∅ → 𝑥 ∈ 𝐴) ∧ (∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴)) → (𝑥 = ∅ → ∅ ∈ 𝐴)) |
7 | 1, 3, 6 | 3syl 17 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → (𝑥 = ∅ → ∅ ∈ 𝐴)) |
8 | 7 | alimi 1344 |
. . 3
⊢
(∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → ∀𝑥(𝑥 = ∅ → ∅ ∈ 𝐴)) |
9 | | exim 1490 |
. . 3
⊢
(∀𝑥(𝑥 = ∅ → ∅ ∈
𝐴) → (∃𝑥 𝑥 = ∅ → ∃𝑥∅ ∈ 𝐴)) |
10 | | 0ex 3884 |
. . . . . 6
⊢ ∅
∈ V |
11 | 10 | isseti 2563 |
. . . . 5
⊢
∃𝑥 𝑥 = ∅ |
12 | | pm2.27 35 |
. . . . 5
⊢
(∃𝑥 𝑥 = ∅ → ((∃𝑥 𝑥 = ∅ → ∃𝑥∅ ∈ 𝐴) → ∃𝑥∅ ∈ 𝐴)) |
13 | 11, 12 | ax-mp 7 |
. . . 4
⊢
((∃𝑥 𝑥 = ∅ → ∃𝑥∅ ∈ 𝐴) → ∃𝑥∅ ∈ 𝐴) |
14 | | bj-ex 9902 |
. . . 4
⊢
(∃𝑥∅
∈ 𝐴 → ∅
∈ 𝐴) |
15 | 13, 14 | syl 14 |
. . 3
⊢
((∃𝑥 𝑥 = ∅ → ∃𝑥∅ ∈ 𝐴) → ∅ ∈ 𝐴) |
16 | 8, 9, 15 | 3syl 17 |
. 2
⊢
(∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → ∅ ∈ 𝐴) |
17 | 3 | simprd 107 |
. . . . . 6
⊢ (((𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴)) |
18 | 1, 17 | syl 14 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → (∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴)) |
19 | 18 | alimi 1344 |
. . . 4
⊢
(∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → ∀𝑥(∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴)) |
20 | | eqid 2040 |
. . . . 5
⊢ suc 𝑧 = suc 𝑧 |
21 | | suceq 4139 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧) |
22 | 21 | eqeq2d 2051 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (suc 𝑧 = suc 𝑦 ↔ suc 𝑧 = suc 𝑧)) |
23 | 22 | rspcev 2656 |
. . . . 5
⊢ ((𝑧 ∈ 𝐴 ∧ suc 𝑧 = suc 𝑧) → ∃𝑦 ∈ 𝐴 suc 𝑧 = suc 𝑦) |
24 | 20, 23 | mpan2 401 |
. . . 4
⊢ (𝑧 ∈ 𝐴 → ∃𝑦 ∈ 𝐴 suc 𝑧 = suc 𝑦) |
25 | | vex 2560 |
. . . . . 6
⊢ 𝑧 ∈ V |
26 | 25 | bj-sucex 10043 |
. . . . 5
⊢ suc 𝑧 ∈ V |
27 | | eqeq1 2046 |
. . . . . . 7
⊢ (𝑥 = suc 𝑧 → (𝑥 = suc 𝑦 ↔ suc 𝑧 = suc 𝑦)) |
28 | 27 | rexbidv 2327 |
. . . . . 6
⊢ (𝑥 = suc 𝑧 → (∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 ↔ ∃𝑦 ∈ 𝐴 suc 𝑧 = suc 𝑦)) |
29 | | eleq1 2100 |
. . . . . 6
⊢ (𝑥 = suc 𝑧 → (𝑥 ∈ 𝐴 ↔ suc 𝑧 ∈ 𝐴)) |
30 | 28, 29 | imbi12d 223 |
. . . . 5
⊢ (𝑥 = suc 𝑧 → ((∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴) ↔ (∃𝑦 ∈ 𝐴 suc 𝑧 = suc 𝑦 → suc 𝑧 ∈ 𝐴))) |
31 | 26, 30 | spcv 2646 |
. . . 4
⊢
(∀𝑥(∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 suc 𝑧 = suc 𝑦 → suc 𝑧 ∈ 𝐴)) |
32 | 19, 24, 31 | syl2im 34 |
. . 3
⊢
(∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → (𝑧 ∈ 𝐴 → suc 𝑧 ∈ 𝐴)) |
33 | 32 | ralrimiv 2391 |
. 2
⊢
(∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → ∀𝑧 ∈ 𝐴 suc 𝑧 ∈ 𝐴) |
34 | | df-bj-ind 10051 |
. 2
⊢ (Ind
𝐴 ↔ (∅ ∈
𝐴 ∧ ∀𝑧 ∈ 𝐴 suc 𝑧 ∈ 𝐴)) |
35 | 16, 33, 34 | sylanbrc 394 |
1
⊢
(∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → Ind 𝐴) |