Step | Hyp | Ref
| Expression |
1 | | winacard 9514 |
. . . 4
⊢ (𝐴 ∈ Inaccw →
(card‘𝐴) = 𝐴) |
2 | | winainf 9516 |
. . . . 5
⊢ (𝐴 ∈ Inaccw →
ω ⊆ 𝐴) |
3 | | cardalephex 8913 |
. . . . 5
⊢ (ω
⊆ 𝐴 →
((card‘𝐴) = 𝐴 ↔ ∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥))) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (𝐴 ∈ Inaccw →
((card‘𝐴) = 𝐴 ↔ ∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥))) |
5 | 1, 4 | mpbid 222 |
. . 3
⊢ (𝐴 ∈ Inaccw →
∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥)) |
6 | 5 | adantr 481 |
. 2
⊢ ((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) →
∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥)) |
7 | | df-rex 2918 |
. . 3
⊢
(∃𝑥 ∈ On
𝐴 = (ℵ‘𝑥) ↔ ∃𝑥(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) |
8 | | simprr 796 |
. . . . . . 7
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → 𝐴 = (ℵ‘𝑥)) |
9 | 8 | eqcomd 2628 |
. . . . . 6
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → (ℵ‘𝑥) = 𝐴) |
10 | | simprl 794 |
. . . . . . . 8
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → 𝑥 ∈ On) |
11 | | onzsl 7046 |
. . . . . . . 8
⊢ (𝑥 ∈ On ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦 ∨ (𝑥 ∈ V ∧ Lim 𝑥))) |
12 | 10, 11 | sylib 208 |
. . . . . . 7
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦 ∨ (𝑥 ∈ V ∧ Lim 𝑥))) |
13 | | simplr 792 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → 𝐴 ≠ ω) |
14 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ∅ →
(ℵ‘𝑥) =
(ℵ‘∅)) |
15 | | aleph0 8889 |
. . . . . . . . . . . . . 14
⊢
(ℵ‘∅) = ω |
16 | 14, 15 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ →
(ℵ‘𝑥) =
ω) |
17 | | eqtr 2641 |
. . . . . . . . . . . . 13
⊢ ((𝐴 = (ℵ‘𝑥) ∧ (ℵ‘𝑥) = ω) → 𝐴 = ω) |
18 | 16, 17 | sylan2 491 |
. . . . . . . . . . . 12
⊢ ((𝐴 = (ℵ‘𝑥) ∧ 𝑥 = ∅) → 𝐴 = ω) |
19 | 18 | ex 450 |
. . . . . . . . . . 11
⊢ (𝐴 = (ℵ‘𝑥) → (𝑥 = ∅ → 𝐴 = ω)) |
20 | 19 | necon3ad 2807 |
. . . . . . . . . 10
⊢ (𝐴 = (ℵ‘𝑥) → (𝐴 ≠ ω → ¬ 𝑥 = ∅)) |
21 | 8, 13, 20 | sylc 65 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ¬ 𝑥 = ∅) |
22 | 21 | pm2.21d 118 |
. . . . . . . 8
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → (𝑥 = ∅ → Lim 𝑥)) |
23 | | suceloni 7013 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) |
24 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
25 | 24 | sucid 5804 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ suc 𝑦 |
26 | | alephord2i 8900 |
. . . . . . . . . . . . . . . 16
⊢ (suc
𝑦 ∈ On → (𝑦 ∈ suc 𝑦 → (ℵ‘𝑦) ∈ (ℵ‘suc 𝑦))) |
27 | 23, 25, 26 | mpisyl 21 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ On →
(ℵ‘𝑦) ∈
(ℵ‘suc 𝑦)) |
28 | 27 | ad2antrl 764 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (ℵ‘𝑦) ∈ (ℵ‘suc 𝑦)) |
29 | | simplrr 801 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → 𝐴 = (ℵ‘𝑥)) |
30 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = suc 𝑦 → (ℵ‘𝑥) = (ℵ‘suc 𝑦)) |
31 | 30 | ad2antll 765 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (ℵ‘𝑥) = (ℵ‘suc 𝑦)) |
32 | 29, 31 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → 𝐴 = (ℵ‘suc 𝑦)) |
33 | 28, 32 | eleqtrrd 2704 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (ℵ‘𝑦) ∈ 𝐴) |
34 | | elwina 9508 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Inaccw ↔
(𝐴 ≠ ∅ ∧
(cf‘𝐴) = 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤)) |
35 | 34 | simp3bi 1078 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Inaccw →
∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤) |
36 | 35 | ad3antrrr 766 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤) |
37 | | breq1 4656 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (ℵ‘𝑦) → (𝑧 ≺ 𝑤 ↔ (ℵ‘𝑦) ≺ 𝑤)) |
38 | 37 | rexbidv 3052 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (ℵ‘𝑦) → (∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤 ↔ ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤)) |
39 | 38 | rspcva 3307 |
. . . . . . . . . . . . 13
⊢
(((ℵ‘𝑦)
∈ 𝐴 ∧
∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤) → ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤) |
40 | 33, 36, 39 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤) |
41 | 40 | expr 643 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ 𝑦 ∈ On) → (𝑥 = suc 𝑦 → ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤)) |
42 | | iscard 8801 |
. . . . . . . . . . . . . . . . . . 19
⊢
((card‘𝐴) =
𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑤 ∈ 𝐴 𝑤 ≺ 𝐴)) |
43 | 42 | simprbi 480 |
. . . . . . . . . . . . . . . . . 18
⊢
((card‘𝐴) =
𝐴 → ∀𝑤 ∈ 𝐴 𝑤 ≺ 𝐴) |
44 | | rsp 2929 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑤 ∈
𝐴 𝑤 ≺ 𝐴 → (𝑤 ∈ 𝐴 → 𝑤 ≺ 𝐴)) |
45 | 1, 43, 44 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ Inaccw →
(𝑤 ∈ 𝐴 → 𝑤 ≺ 𝐴)) |
46 | 45 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ∈ 𝐴 → 𝑤 ≺ 𝐴)) |
47 | 32 | breq2d 4665 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ≺ 𝐴 ↔ 𝑤 ≺ (ℵ‘suc 𝑦))) |
48 | 46, 47 | sylibd 229 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ∈ 𝐴 → 𝑤 ≺ (ℵ‘suc 𝑦))) |
49 | | alephnbtwn2 8895 |
. . . . . . . . . . . . . . . 16
⊢ ¬
((ℵ‘𝑦) ≺
𝑤 ∧ 𝑤 ≺ (ℵ‘suc 𝑦)) |
50 | | pm3.21 464 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ≺ (ℵ‘suc
𝑦) →
((ℵ‘𝑦) ≺
𝑤 →
((ℵ‘𝑦) ≺
𝑤 ∧ 𝑤 ≺ (ℵ‘suc 𝑦)))) |
51 | 49, 50 | mtoi 190 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ≺ (ℵ‘suc
𝑦) → ¬
(ℵ‘𝑦) ≺
𝑤) |
52 | 48, 51 | syl6 35 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ∈ 𝐴 → ¬ (ℵ‘𝑦) ≺ 𝑤)) |
53 | 52 | imp 445 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
Inaccw ∧ 𝐴
≠ ω) ∧ (𝑥
∈ On ∧ 𝐴 =
(ℵ‘𝑥))) ∧
(𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) ∧ 𝑤 ∈ 𝐴) → ¬ (ℵ‘𝑦) ≺ 𝑤) |
54 | 53 | nrexdv 3001 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → ¬ ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤) |
55 | 54 | expr 643 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ 𝑦 ∈ On) → (𝑥 = suc 𝑦 → ¬ ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤)) |
56 | 41, 55 | pm2.65d 187 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ 𝑦 ∈ On) → ¬ 𝑥 = suc 𝑦) |
57 | 56 | nrexdv 3001 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ¬ ∃𝑦 ∈ On 𝑥 = suc 𝑦) |
58 | 57 | pm2.21d 118 |
. . . . . . . 8
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → (∃𝑦 ∈ On 𝑥 = suc 𝑦 → Lim 𝑥)) |
59 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → Lim 𝑥) |
60 | 59 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ((𝑥 ∈ V ∧ Lim 𝑥) → Lim 𝑥)) |
61 | 22, 58, 60 | 3jaod 1392 |
. . . . . . 7
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ((𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦 ∨ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim 𝑥)) |
62 | 12, 61 | mpd 15 |
. . . . . 6
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → Lim 𝑥) |
63 | 9, 62 | jca 554 |
. . . . 5
⊢ (((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) ∧
(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥)) |
64 | 63 | ex 450 |
. . . 4
⊢ ((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) →
((𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥)) → ((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥))) |
65 | 64 | eximdv 1846 |
. . 3
⊢ ((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) →
(∃𝑥(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥)) → ∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥))) |
66 | 7, 65 | syl5bi 232 |
. 2
⊢ ((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) →
(∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥) → ∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥))) |
67 | 6, 66 | mpd 15 |
1
⊢ ((𝐴 ∈ Inaccw ∧
𝐴 ≠ ω) →
∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥)) |