Step | Hyp | Ref
| Expression |
1 | | eqeq1 2101 |
. . 3
⊢ (𝑦 = 𝐴 → (𝑦 = ∅ ↔ 𝐴 = ∅)) |
2 | | eqeq1 2101 |
. . . 4
⊢ (𝑦 = 𝐴 → (𝑦 = suc 𝑥 ↔ 𝐴 = suc 𝑥)) |
3 | 2 | rexeqbi1dv 2585 |
. . 3
⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥 ↔ ∃𝑥 ∈ 𝐴 𝐴 = suc 𝑥)) |
4 | 1, 3 | orbi12d 745 |
. 2
⊢ (𝑦 = 𝐴 → ((𝑦 = ∅ ∨ ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥) ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ 𝐴 𝐴 = suc 𝑥))) |
5 | | tru 1300 |
. . 3
⊢
⊤ |
6 | | a1tru 1312 |
. . . 4
⊢ (⊤
→ ⊤) |
7 | 6 | rgenw 2441 |
. . 3
⊢
∀𝑧 ∈
ω (⊤ → ⊤) |
8 | | bdeq0 12466 |
. . . . 5
⊢
BOUNDED 𝑦 = ∅ |
9 | | bdeqsuc 12480 |
. . . . . 6
⊢
BOUNDED 𝑦 = suc 𝑥 |
10 | 9 | ax-bdex 12418 |
. . . . 5
⊢
BOUNDED ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥 |
11 | 8, 10 | ax-bdor 12415 |
. . . 4
⊢
BOUNDED (𝑦 = ∅ ∨ ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥) |
12 | | nfv 1473 |
. . . 4
⊢
Ⅎ𝑦⊤ |
13 | | orc 671 |
. . . . 5
⊢ (𝑦 = ∅ → (𝑦 = ∅ ∨ ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥)) |
14 | 13 | a1d 22 |
. . . 4
⊢ (𝑦 = ∅ → (⊤
→ (𝑦 = ∅ ∨
∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥))) |
15 | | a1tru 1312 |
. . . . 5
⊢ (¬
(𝑦 = 𝑧 → ¬ (𝑦 = ∅ ∨ ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥)) → ⊤) |
16 | 15 | expi 605 |
. . . 4
⊢ (𝑦 = 𝑧 → ((𝑦 = ∅ ∨ ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥) → ⊤)) |
17 | | vex 2636 |
. . . . . . . . 9
⊢ 𝑧 ∈ V |
18 | 17 | sucid 4268 |
. . . . . . . 8
⊢ 𝑧 ∈ suc 𝑧 |
19 | | eleq2 2158 |
. . . . . . . 8
⊢ (𝑦 = suc 𝑧 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ suc 𝑧)) |
20 | 18, 19 | mpbiri 167 |
. . . . . . 7
⊢ (𝑦 = suc 𝑧 → 𝑧 ∈ 𝑦) |
21 | | suceq 4253 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧) |
22 | 21 | eqeq2d 2106 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑦 = suc 𝑥 ↔ 𝑦 = suc 𝑧)) |
23 | 22 | rspcev 2736 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 = suc 𝑧) → ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥) |
24 | 20, 23 | mpancom 414 |
. . . . . 6
⊢ (𝑦 = suc 𝑧 → ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥) |
25 | 24 | olcd 691 |
. . . . 5
⊢ (𝑦 = suc 𝑧 → (𝑦 = ∅ ∨ ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥)) |
26 | 25 | a1d 22 |
. . . 4
⊢ (𝑦 = suc 𝑧 → (⊤ → (𝑦 = ∅ ∨ ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥))) |
27 | 11, 12, 12, 12, 14, 16, 26 | bj-bdfindis 12550 |
. . 3
⊢
((⊤ ∧ ∀𝑧 ∈ ω (⊤ → ⊤))
→ ∀𝑦 ∈
ω (𝑦 = ∅ ∨
∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥)) |
28 | 5, 7, 27 | mp2an 418 |
. 2
⊢
∀𝑦 ∈
ω (𝑦 = ∅ ∨
∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥) |
29 | 4, 28 | vtoclri 2708 |
1
⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ 𝐴 𝐴 = suc 𝑥)) |