Step | Hyp | Ref
| Expression |
1 | | eqeq1 2147 |
. . 3
⊢ (𝑦 = 𝐴 → (𝑦 = ∅ ↔ 𝐴 = ∅)) |
2 | | eqeq1 2147 |
. . . 4
⊢ (𝑦 = 𝐴 → (𝑦 = suc 𝑥 ↔ 𝐴 = suc 𝑥)) |
3 | 2 | rexeqbi1dv 2638 |
. . 3
⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥 ↔ ∃𝑥 ∈ 𝐴 𝐴 = suc 𝑥)) |
4 | 1, 3 | orbi12d 783 |
. 2
⊢ (𝑦 = 𝐴 → ((𝑦 = ∅ ∨ ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥) ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ 𝐴 𝐴 = suc 𝑥))) |
5 | | tru 1336 |
. . 3
⊢
⊤ |
6 | | a1tru 1348 |
. . . 4
⊢ (⊤
→ ⊤) |
7 | 6 | rgenw 2490 |
. . 3
⊢
∀𝑧 ∈
ω (⊤ → ⊤) |
8 | | bdeq0 13236 |
. . . . 5
⊢
BOUNDED 𝑦 = ∅ |
9 | | bdeqsuc 13250 |
. . . . . 6
⊢
BOUNDED 𝑦 = suc 𝑥 |
10 | 9 | ax-bdex 13188 |
. . . . 5
⊢
BOUNDED ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥 |
11 | 8, 10 | ax-bdor 13185 |
. . . 4
⊢
BOUNDED (𝑦 = ∅ ∨ ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥) |
12 | | nfv 1509 |
. . . 4
⊢
Ⅎ𝑦⊤ |
13 | | orc 702 |
. . . . 5
⊢ (𝑦 = ∅ → (𝑦 = ∅ ∨ ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥)) |
14 | 13 | a1d 22 |
. . . 4
⊢ (𝑦 = ∅ → (⊤
→ (𝑦 = ∅ ∨
∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥))) |
15 | | a1tru 1348 |
. . . . 5
⊢ (¬
(𝑦 = 𝑧 → ¬ (𝑦 = ∅ ∨ ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥)) → ⊤) |
16 | 15 | expi 628 |
. . . 4
⊢ (𝑦 = 𝑧 → ((𝑦 = ∅ ∨ ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥) → ⊤)) |
17 | | vex 2692 |
. . . . . . . . 9
⊢ 𝑧 ∈ V |
18 | 17 | sucid 4347 |
. . . . . . . 8
⊢ 𝑧 ∈ suc 𝑧 |
19 | | eleq2 2204 |
. . . . . . . 8
⊢ (𝑦 = suc 𝑧 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ suc 𝑧)) |
20 | 18, 19 | mpbiri 167 |
. . . . . . 7
⊢ (𝑦 = suc 𝑧 → 𝑧 ∈ 𝑦) |
21 | | suceq 4332 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧) |
22 | 21 | eqeq2d 2152 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑦 = suc 𝑥 ↔ 𝑦 = suc 𝑧)) |
23 | 22 | rspcev 2793 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 = suc 𝑧) → ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥) |
24 | 20, 23 | mpancom 419 |
. . . . . 6
⊢ (𝑦 = suc 𝑧 → ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥) |
25 | 24 | olcd 724 |
. . . . 5
⊢ (𝑦 = suc 𝑧 → (𝑦 = ∅ ∨ ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥)) |
26 | 25 | a1d 22 |
. . . 4
⊢ (𝑦 = suc 𝑧 → (⊤ → (𝑦 = ∅ ∨ ∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥))) |
27 | 11, 12, 12, 12, 14, 16, 26 | bj-bdfindis 13316 |
. . 3
⊢
((⊤ ∧ ∀𝑧 ∈ ω (⊤ → ⊤))
→ ∀𝑦 ∈
ω (𝑦 = ∅ ∨
∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥)) |
28 | 5, 7, 27 | mp2an 423 |
. 2
⊢
∀𝑦 ∈
ω (𝑦 = ∅ ∨
∃𝑥 ∈ 𝑦 𝑦 = suc 𝑥) |
29 | 4, 28 | vtoclri 2764 |
1
⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ 𝐴 𝐴 = suc 𝑥)) |