Step | Hyp | Ref
| Expression |
1 | | winacard 10448 |
. . . 4
⊢ (𝐴 ∈ Inaccw →
(card‘𝐴) = 𝐴) |
2 | | winainf 10450 |
. . . . 5
⊢ (𝐴 ∈ Inaccw →
ω ⊆ 𝐴) |
3 | | cardalephex 9846 |
. . . . 5
⊢ (ω
⊆ 𝐴 →
((card‘𝐴) = 𝐴 ↔ ∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥))) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (𝐴 ∈ Inaccw →
((card‘𝐴) = 𝐴 ↔ ∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥))) |
5 | 1, 4 | mpbid 231 |
. . 3
⊢ (𝐴 ∈ Inaccw →
∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥)) |
6 | 5 | adantr 481 |
. 2
⊢ ((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) →
∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥)) |
7 | | df-rex 3070 |
. . 3
⊢
(∃𝑥 ∈ On
𝐴 = (ℵ‘𝑥) ↔ ∃𝑥(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) |
8 | | simprr 770 |
. . . . . . 7
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → 𝐴 = (ℵ‘𝑥)) |
9 | 8 | eqcomd 2744 |
. . . . . 6
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → (ℵ‘𝑥) = 𝐴) |
10 | | simprl 768 |
. . . . . . . 8
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → 𝑥 ∈ On) |
11 | | onzsl 7693 |
. . . . . . . 8
⊢ (𝑥 ∈ On ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦 ∨ (𝑥 ∈ V ∧ Lim 𝑥))) |
12 | 10, 11 | sylib 217 |
. . . . . . 7
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦 ∨ (𝑥 ∈ V ∧ Lim 𝑥))) |
13 | | simplr 766 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → 𝐴 ≠ ω) |
14 | | fveq2 6774 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ∅ →
(ℵ‘𝑥) =
(ℵ‘∅)) |
15 | | aleph0 9822 |
. . . . . . . . . . . . . 14
⊢
(ℵ‘∅) = ω |
16 | 14, 15 | eqtrdi 2794 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ →
(ℵ‘𝑥) =
ω) |
17 | | eqtr 2761 |
. . . . . . . . . . . . 13
⊢ ((𝐴 = (ℵ‘𝑥) ∧ (ℵ‘𝑥) = ω) → 𝐴 = ω) |
18 | 16, 17 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((𝐴 = (ℵ‘𝑥) ∧ 𝑥 = ∅) → 𝐴 = ω) |
19 | 18 | ex 413 |
. . . . . . . . . . 11
⊢ (𝐴 = (ℵ‘𝑥) → (𝑥 = ∅ → 𝐴 = ω)) |
20 | 19 | necon3ad 2956 |
. . . . . . . . . 10
⊢ (𝐴 = (ℵ‘𝑥) → (𝐴 ≠ ω → ¬ 𝑥 = ∅)) |
21 | 8, 13, 20 | sylc 65 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ¬ 𝑥 = ∅) |
22 | 21 | pm2.21d 121 |
. . . . . . . 8
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → (𝑥 = ∅ → Lim 𝑥)) |
23 | | breq1 5077 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (ℵ‘𝑦) → (𝑧 ≺ 𝑤 ↔ (ℵ‘𝑦) ≺ 𝑤)) |
24 | 23 | rexbidv 3226 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (ℵ‘𝑦) → (∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤 ↔ ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤)) |
25 | | elwina 10442 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Inaccw ↔
(𝐴 ≠ ∅ ∧
(cf‘𝐴) = 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤)) |
26 | 25 | simp3bi 1146 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Inaccw →
∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤) |
27 | 26 | ad3antrrr 727 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤) |
28 | | suceloni 7659 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) |
29 | | vex 3436 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
30 | 29 | sucid 6345 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ suc 𝑦 |
31 | | alephord2i 9833 |
. . . . . . . . . . . . . . . 16
⊢ (suc
𝑦 ∈ On → (𝑦 ∈ suc 𝑦 → (ℵ‘𝑦) ∈ (ℵ‘suc 𝑦))) |
32 | 28, 30, 31 | mpisyl 21 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ On →
(ℵ‘𝑦) ∈
(ℵ‘suc 𝑦)) |
33 | 32 | ad2antrl 725 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (ℵ‘𝑦) ∈ (ℵ‘suc 𝑦)) |
34 | | simplrr 775 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → 𝐴 = (ℵ‘𝑥)) |
35 | | fveq2 6774 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = suc 𝑦 → (ℵ‘𝑥) = (ℵ‘suc 𝑦)) |
36 | 35 | ad2antll 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (ℵ‘𝑥) = (ℵ‘suc 𝑦)) |
37 | 34, 36 | eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → 𝐴 = (ℵ‘suc 𝑦)) |
38 | 33, 37 | eleqtrrd 2842 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (ℵ‘𝑦) ∈ 𝐴) |
39 | 24, 27, 38 | rspcdva 3562 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤) |
40 | 39 | expr 457 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ 𝑦 ∈ On) → (𝑥 = suc 𝑦 → ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤)) |
41 | | iscard 9733 |
. . . . . . . . . . . . . . . . . . 19
⊢
((card‘𝐴) =
𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑤 ∈ 𝐴 𝑤 ≺ 𝐴)) |
42 | 41 | simprbi 497 |
. . . . . . . . . . . . . . . . . 18
⊢
((card‘𝐴) =
𝐴 → ∀𝑤 ∈ 𝐴 𝑤 ≺ 𝐴) |
43 | | rsp 3131 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑤 ∈
𝐴 𝑤 ≺ 𝐴 → (𝑤 ∈ 𝐴 → 𝑤 ≺ 𝐴)) |
44 | 1, 42, 43 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ Inaccw →
(𝑤 ∈ 𝐴 → 𝑤 ≺ 𝐴)) |
45 | 44 | ad3antrrr 727 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ∈ 𝐴 → 𝑤 ≺ 𝐴)) |
46 | 37 | breq2d 5086 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ≺ 𝐴 ↔ 𝑤 ≺ (ℵ‘suc 𝑦))) |
47 | 45, 46 | sylibd 238 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ∈ 𝐴 → 𝑤 ≺ (ℵ‘suc 𝑦))) |
48 | | alephnbtwn2 9828 |
. . . . . . . . . . . . . . . 16
⊢ ¬
((ℵ‘𝑦) ≺
𝑤 ∧ 𝑤 ≺ (ℵ‘suc 𝑦)) |
49 | | pm3.21 472 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ≺ (ℵ‘suc
𝑦) →
((ℵ‘𝑦) ≺
𝑤 →
((ℵ‘𝑦) ≺
𝑤 ∧ 𝑤 ≺ (ℵ‘suc 𝑦)))) |
50 | 48, 49 | mtoi 198 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ≺ (ℵ‘suc
𝑦) → ¬
(ℵ‘𝑦) ≺
𝑤) |
51 | 47, 50 | syl6 35 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ∈ 𝐴 → ¬ (ℵ‘𝑦) ≺ 𝑤)) |
52 | 51 | imp 407 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
Inaccw ∧ 𝐴
≠ ω) ∧ (𝑥
∈ On ∧ 𝐴 =
(ℵ‘𝑥))) ∧
(𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) ∧ 𝑤 ∈ 𝐴) → ¬ (ℵ‘𝑦) ≺ 𝑤) |
53 | 52 | nrexdv 3198 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → ¬ ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤) |
54 | 53 | expr 457 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ 𝑦 ∈ On) → (𝑥 = suc 𝑦 → ¬ ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤)) |
55 | 40, 54 | pm2.65d 195 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ 𝑦 ∈ On) → ¬ 𝑥 = suc 𝑦) |
56 | 55 | nrexdv 3198 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ¬ ∃𝑦 ∈ On 𝑥 = suc 𝑦) |
57 | 56 | pm2.21d 121 |
. . . . . . . 8
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → (∃𝑦 ∈ On 𝑥 = suc 𝑦 → Lim 𝑥)) |
58 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → Lim 𝑥) |
59 | 58 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ((𝑥 ∈ V ∧ Lim 𝑥) → Lim 𝑥)) |
60 | 22, 57, 59 | 3jaod 1427 |
. . . . . . 7
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ((𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦 ∨ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim 𝑥)) |
61 | 12, 60 | mpd 15 |
. . . . . 6
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → Lim 𝑥) |
62 | 9, 61 | jca 512 |
. . . . 5
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥)) |
63 | 62 | ex 413 |
. . . 4
⊢ ((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) →
((𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥)) → ((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥))) |
64 | 63 | eximdv 1920 |
. . 3
⊢ ((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) →
(∃𝑥(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥)) → ∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥))) |
65 | 7, 64 | syl5bi 241 |
. 2
⊢ ((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) →
(∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥) → ∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥))) |
66 | 6, 65 | mpd 15 |
1
⊢ ((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) →
∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥)) |