Step | Hyp | Ref
| Expression |
1 | | biimpr 129 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → ((𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → 𝑥 ∈ 𝐴)) |
2 | | jaob 700 |
. . . . . 6
⊢ (((𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → 𝑥 ∈ 𝐴) ↔ ((𝑥 = ∅ → 𝑥 ∈ 𝐴) ∧ (∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴))) |
3 | 2 | biimpi 119 |
. . . . 5
⊢ (((𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → 𝑥 ∈ 𝐴) → ((𝑥 = ∅ → 𝑥 ∈ 𝐴) ∧ (∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴))) |
4 | | simpl 108 |
. . . . . 6
⊢ (((𝑥 = ∅ → 𝑥 ∈ 𝐴) ∧ (∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴)) → (𝑥 = ∅ → 𝑥 ∈ 𝐴)) |
5 | | eleq1 2220 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑥 ∈ 𝐴 ↔ ∅ ∈ 𝐴)) |
6 | 4, 5 | mpbidi 150 |
. . . . 5
⊢ (((𝑥 = ∅ → 𝑥 ∈ 𝐴) ∧ (∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴)) → (𝑥 = ∅ → ∅ ∈ 𝐴)) |
7 | 1, 3, 6 | 3syl 17 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → (𝑥 = ∅ → ∅ ∈ 𝐴)) |
8 | 7 | alimi 1435 |
. . 3
⊢
(∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → ∀𝑥(𝑥 = ∅ → ∅ ∈ 𝐴)) |
9 | | exim 1579 |
. . 3
⊢
(∀𝑥(𝑥 = ∅ → ∅ ∈
𝐴) → (∃𝑥 𝑥 = ∅ → ∃𝑥∅ ∈ 𝐴)) |
10 | | 0ex 4091 |
. . . . . 6
⊢ ∅
∈ V |
11 | 10 | isseti 2720 |
. . . . 5
⊢
∃𝑥 𝑥 = ∅ |
12 | | pm2.27 40 |
. . . . 5
⊢
(∃𝑥 𝑥 = ∅ → ((∃𝑥 𝑥 = ∅ → ∃𝑥∅ ∈ 𝐴) → ∃𝑥∅ ∈ 𝐴)) |
13 | 11, 12 | ax-mp 5 |
. . . 4
⊢
((∃𝑥 𝑥 = ∅ → ∃𝑥∅ ∈ 𝐴) → ∃𝑥∅ ∈ 𝐴) |
14 | | bj-ex 13336 |
. . . 4
⊢
(∃𝑥∅
∈ 𝐴 → ∅
∈ 𝐴) |
15 | 13, 14 | syl 14 |
. . 3
⊢
((∃𝑥 𝑥 = ∅ → ∃𝑥∅ ∈ 𝐴) → ∅ ∈ 𝐴) |
16 | 8, 9, 15 | 3syl 17 |
. 2
⊢
(∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → ∅ ∈ 𝐴) |
17 | 3 | simprd 113 |
. . . . . 6
⊢ (((𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦) → 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴)) |
18 | 1, 17 | syl 14 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → (∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴)) |
19 | 18 | alimi 1435 |
. . . 4
⊢
(∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → ∀𝑥(∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴)) |
20 | | eqid 2157 |
. . . . 5
⊢ suc 𝑧 = suc 𝑧 |
21 | | suceq 4362 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧) |
22 | 21 | eqeq2d 2169 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (suc 𝑧 = suc 𝑦 ↔ suc 𝑧 = suc 𝑧)) |
23 | 22 | rspcev 2816 |
. . . . 5
⊢ ((𝑧 ∈ 𝐴 ∧ suc 𝑧 = suc 𝑧) → ∃𝑦 ∈ 𝐴 suc 𝑧 = suc 𝑦) |
24 | 20, 23 | mpan2 422 |
. . . 4
⊢ (𝑧 ∈ 𝐴 → ∃𝑦 ∈ 𝐴 suc 𝑧 = suc 𝑦) |
25 | | vex 2715 |
. . . . . 6
⊢ 𝑧 ∈ V |
26 | 25 | bj-sucex 13498 |
. . . . 5
⊢ suc 𝑧 ∈ V |
27 | | eqeq1 2164 |
. . . . . . 7
⊢ (𝑥 = suc 𝑧 → (𝑥 = suc 𝑦 ↔ suc 𝑧 = suc 𝑦)) |
28 | 27 | rexbidv 2458 |
. . . . . 6
⊢ (𝑥 = suc 𝑧 → (∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 ↔ ∃𝑦 ∈ 𝐴 suc 𝑧 = suc 𝑦)) |
29 | | eleq1 2220 |
. . . . . 6
⊢ (𝑥 = suc 𝑧 → (𝑥 ∈ 𝐴 ↔ suc 𝑧 ∈ 𝐴)) |
30 | 28, 29 | imbi12d 233 |
. . . . 5
⊢ (𝑥 = suc 𝑧 → ((∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴) ↔ (∃𝑦 ∈ 𝐴 suc 𝑧 = suc 𝑦 → suc 𝑧 ∈ 𝐴))) |
31 | 26, 30 | spcv 2806 |
. . . 4
⊢
(∀𝑥(∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦 → 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 suc 𝑧 = suc 𝑦 → suc 𝑧 ∈ 𝐴)) |
32 | 19, 24, 31 | syl2im 38 |
. . 3
⊢
(∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → (𝑧 ∈ 𝐴 → suc 𝑧 ∈ 𝐴)) |
33 | 32 | ralrimiv 2529 |
. 2
⊢
(∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → ∀𝑧 ∈ 𝐴 suc 𝑧 ∈ 𝐴) |
34 | | df-bj-ind 13502 |
. 2
⊢ (Ind
𝐴 ↔ (∅ ∈
𝐴 ∧ ∀𝑧 ∈ 𝐴 suc 𝑧 ∈ 𝐴)) |
35 | 16, 33, 34 | sylanbrc 414 |
1
⊢
(∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ 𝐴 𝑥 = suc 𝑦)) → Ind 𝐴) |