Step | Hyp | Ref
| Expression |
1 | | ax-inf2 13971 |
. . 3
⊢
∃𝑎∀𝑦(𝑦 ∈ 𝑎 ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ 𝑎 𝑦 = suc 𝑧)) |
2 | | vex 2733 |
. . . . 5
⊢ 𝑎 ∈ V |
3 | | bdcv 13843 |
. . . . . 6
⊢
BOUNDED 𝑎 |
4 | 3 | bj-inf2vn 13969 |
. . . . 5
⊢ (𝑎 ∈ V → (∀𝑦(𝑦 ∈ 𝑎 ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ 𝑎 𝑦 = suc 𝑧)) → 𝑎 = ω)) |
5 | 2, 4 | ax-mp 5 |
. . . 4
⊢
(∀𝑦(𝑦 ∈ 𝑎 ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ 𝑎 𝑦 = suc 𝑧)) → 𝑎 = ω) |
6 | | eleq2 2234 |
. . . . . . 7
⊢ (𝑎 = ω → (𝑦 ∈ 𝑎 ↔ 𝑦 ∈ ω)) |
7 | | rexeq 2666 |
. . . . . . . 8
⊢ (𝑎 = ω → (∃𝑧 ∈ 𝑎 𝑦 = suc 𝑧 ↔ ∃𝑧 ∈ ω 𝑦 = suc 𝑧)) |
8 | 7 | orbi2d 785 |
. . . . . . 7
⊢ (𝑎 = ω → ((𝑦 = ∅ ∨ ∃𝑧 ∈ 𝑎 𝑦 = suc 𝑧) ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ ω 𝑦 = suc 𝑧))) |
9 | 6, 8 | bibi12d 234 |
. . . . . 6
⊢ (𝑎 = ω → ((𝑦 ∈ 𝑎 ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ 𝑎 𝑦 = suc 𝑧)) ↔ (𝑦 ∈ ω ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ ω 𝑦 = suc 𝑧)))) |
10 | 9 | albidv 1817 |
. . . . 5
⊢ (𝑎 = ω → (∀𝑦(𝑦 ∈ 𝑎 ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ 𝑎 𝑦 = suc 𝑧)) ↔ ∀𝑦(𝑦 ∈ ω ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ ω 𝑦 = suc 𝑧)))) |
11 | | nfcv 2312 |
. . . . . . . 8
⊢
Ⅎ𝑦𝐴 |
12 | | nfv 1521 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) |
13 | | eleq1 2233 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝑦 ∈ ω ↔ 𝐴 ∈ ω)) |
14 | | eqeq1 2177 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → (𝑦 = ∅ ↔ 𝐴 = ∅)) |
15 | | suceq 4385 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → suc 𝑧 = suc 𝑥) |
16 | 15 | eqeq2d 2182 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → (𝑦 = suc 𝑧 ↔ 𝑦 = suc 𝑥)) |
17 | 16 | cbvrexv 2697 |
. . . . . . . . . . . 12
⊢
(∃𝑧 ∈
ω 𝑦 = suc 𝑧 ↔ ∃𝑥 ∈ ω 𝑦 = suc 𝑥) |
18 | | eqeq1 2177 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝐴 → (𝑦 = suc 𝑥 ↔ 𝐴 = suc 𝑥)) |
19 | 18 | rexbidv 2471 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ ω 𝑦 = suc 𝑥 ↔ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) |
20 | 17, 19 | syl5bb 191 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → (∃𝑧 ∈ ω 𝑦 = suc 𝑧 ↔ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) |
21 | 14, 20 | orbi12d 788 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → ((𝑦 = ∅ ∨ ∃𝑧 ∈ ω 𝑦 = suc 𝑧) ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥))) |
22 | 13, 21 | bibi12d 234 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → ((𝑦 ∈ ω ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ ω 𝑦 = suc 𝑧)) ↔ (𝐴 ∈ ω ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)))) |
23 | | biimp 117 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ω ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) → (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥))) |
24 | 22, 23 | syl6bi 162 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → ((𝑦 ∈ ω ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ ω 𝑦 = suc 𝑧)) → (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)))) |
25 | 11, 12, 24 | spcimgf 2810 |
. . . . . . 7
⊢ (𝐴 ∈ ω →
(∀𝑦(𝑦 ∈ ω ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ ω 𝑦 = suc 𝑧)) → (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)))) |
26 | 25 | pm2.43b 52 |
. . . . . 6
⊢
(∀𝑦(𝑦 ∈ ω ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ ω 𝑦 = suc 𝑧)) → (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥))) |
27 | | peano1 4576 |
. . . . . . . 8
⊢ ∅
∈ ω |
28 | | eleq1 2233 |
. . . . . . . 8
⊢ (𝐴 = ∅ → (𝐴 ∈ ω ↔ ∅
∈ ω)) |
29 | 27, 28 | mpbiri 167 |
. . . . . . 7
⊢ (𝐴 = ∅ → 𝐴 ∈
ω) |
30 | | bj-peano2 13934 |
. . . . . . . . 9
⊢ (𝑥 ∈ ω → suc 𝑥 ∈
ω) |
31 | | eleq1a 2242 |
. . . . . . . . . 10
⊢ (suc
𝑥 ∈ ω →
(𝐴 = suc 𝑥 → 𝐴 ∈ ω)) |
32 | 31 | imp 123 |
. . . . . . . . 9
⊢ ((suc
𝑥 ∈ ω ∧
𝐴 = suc 𝑥) → 𝐴 ∈ ω) |
33 | 30, 32 | sylan 281 |
. . . . . . . 8
⊢ ((𝑥 ∈ ω ∧ 𝐴 = suc 𝑥) → 𝐴 ∈ ω) |
34 | 33 | rexlimiva 2582 |
. . . . . . 7
⊢
(∃𝑥 ∈
ω 𝐴 = suc 𝑥 → 𝐴 ∈ ω) |
35 | 29, 34 | jaoi 711 |
. . . . . 6
⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥) → 𝐴 ∈ ω) |
36 | 26, 35 | impbid1 141 |
. . . . 5
⊢
(∀𝑦(𝑦 ∈ ω ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ ω 𝑦 = suc 𝑧)) → (𝐴 ∈ ω ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥))) |
37 | 10, 36 | syl6bi 162 |
. . . 4
⊢ (𝑎 = ω → (∀𝑦(𝑦 ∈ 𝑎 ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ 𝑎 𝑦 = suc 𝑧)) → (𝐴 ∈ ω ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)))) |
38 | 5, 37 | mpcom 36 |
. . 3
⊢
(∀𝑦(𝑦 ∈ 𝑎 ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ 𝑎 𝑦 = suc 𝑧)) → (𝐴 ∈ ω ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥))) |
39 | 1, 38 | eximii 1595 |
. 2
⊢
∃𝑎(𝐴 ∈ ω ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) |
40 | | bj-ex 13756 |
. 2
⊢
(∃𝑎(𝐴 ∈ ω ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) → (𝐴 ∈ ω ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥))) |
41 | 39, 40 | ax-mp 5 |
1
⊢ (𝐴 ∈ ω ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥)) |