Step | Hyp | Ref
| Expression |
1 | | cardon 8653 |
. . . . . . . . 9
⊢
(card‘𝐴)
∈ On |
2 | | eleq1 2676 |
. . . . . . . . 9
⊢
((card‘𝐴) =
𝐴 → ((card‘𝐴) ∈ On ↔ 𝐴 ∈ On)) |
3 | 1, 2 | mpbii 222 |
. . . . . . . 8
⊢
((card‘𝐴) =
𝐴 → 𝐴 ∈ On) |
4 | | alephle 8794 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → 𝐴 ⊆ (ℵ‘𝐴)) |
5 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → (ℵ‘𝑥) = (ℵ‘𝐴)) |
6 | 5 | sseq2d 3596 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝐴 ⊆ (ℵ‘𝑥) ↔ 𝐴 ⊆ (ℵ‘𝐴))) |
7 | 6 | rspcev 3282 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐴 ⊆ (ℵ‘𝐴)) → ∃𝑥 ∈ On 𝐴 ⊆ (ℵ‘𝑥)) |
8 | 4, 7 | mpdan 699 |
. . . . . . . 8
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ⊆ (ℵ‘𝑥)) |
9 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐴 |
10 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥ℵ |
11 | | nfrab1 3099 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥{𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} |
12 | 11 | nfint 4421 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} |
13 | 10, 12 | nffv 6110 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(ℵ‘∩
{𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) |
14 | 9, 13 | nfss 3561 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝐴 ⊆ (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) |
15 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = ∩
{𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} → (ℵ‘𝑥) = (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)})) |
16 | 15 | sseq2d 3596 |
. . . . . . . . 9
⊢ (𝑥 = ∩
{𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} → (𝐴 ⊆ (ℵ‘𝑥) ↔ 𝐴 ⊆ (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}))) |
17 | 14, 16 | onminsb 6891 |
. . . . . . . 8
⊢
(∃𝑥 ∈ On
𝐴 ⊆
(ℵ‘𝑥) →
𝐴 ⊆
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})) |
18 | 3, 8, 17 | 3syl 18 |
. . . . . . 7
⊢
((card‘𝐴) =
𝐴 → 𝐴 ⊆ (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)})) |
19 | 18 | a1i 11 |
. . . . . 6
⊢ (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} =
∅ → ((card‘𝐴) = 𝐴 → 𝐴 ⊆ (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}))) |
20 | | fveq2 6103 |
. . . . . . . . 9
⊢ (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} =
∅ → (ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) =
(ℵ‘∅)) |
21 | | aleph0 8772 |
. . . . . . . . 9
⊢
(ℵ‘∅) = ω |
22 | 20, 21 | syl6eq 2660 |
. . . . . . . 8
⊢ (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} =
∅ → (ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) = ω) |
23 | 22 | sseq1d 3595 |
. . . . . . 7
⊢ (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} =
∅ → ((ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ⊆ 𝐴 ↔ ω ⊆ 𝐴)) |
24 | 23 | biimprd 237 |
. . . . . 6
⊢ (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} =
∅ → (ω ⊆ 𝐴 → (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) ⊆
𝐴)) |
25 | 19, 24 | anim12d 584 |
. . . . 5
⊢ (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} =
∅ → (((card‘𝐴) = 𝐴 ∧ ω ⊆ 𝐴) → (𝐴 ⊆ (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) ∧
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ⊆ 𝐴))) |
26 | | eqss 3583 |
. . . . 5
⊢ (𝐴 = (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) ↔
(𝐴 ⊆
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ∧ (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) ⊆
𝐴)) |
27 | 25, 26 | syl6ibr 241 |
. . . 4
⊢ (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} =
∅ → (((card‘𝐴) = 𝐴 ∧ ω ⊆ 𝐴) → 𝐴 = (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}))) |
28 | 27 | com12 32 |
. . 3
⊢
(((card‘𝐴) =
𝐴 ∧ ω ⊆
𝐴) → (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} =
∅ → 𝐴 =
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))) |
29 | 28 | ancoms 468 |
. 2
⊢ ((ω
⊆ 𝐴 ∧
(card‘𝐴) = 𝐴) → (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} =
∅ → 𝐴 =
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))) |
30 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
31 | 30 | sucid 5721 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ suc 𝑦 |
32 | | eleq2 2677 |
. . . . . . . . . . 11
⊢ (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} = suc
𝑦 → (𝑦 ∈ ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} ↔
𝑦 ∈ suc 𝑦)) |
33 | 31, 32 | mpbiri 247 |
. . . . . . . . . 10
⊢ (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} = suc
𝑦 → 𝑦 ∈ ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) |
34 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (ℵ‘𝑥) = (ℵ‘𝑦)) |
35 | 34 | sseq2d 3596 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐴 ⊆ (ℵ‘𝑥) ↔ 𝐴 ⊆ (ℵ‘𝑦))) |
36 | 35 | onnminsb 6896 |
. . . . . . . . . 10
⊢ (𝑦 ∈ On → (𝑦 ∈ ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} →
¬ 𝐴 ⊆
(ℵ‘𝑦))) |
37 | 33, 36 | syl5 33 |
. . . . . . . . 9
⊢ (𝑦 ∈ On → (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} = suc
𝑦 → ¬ 𝐴 ⊆ (ℵ‘𝑦))) |
38 | 37 | imp 444 |
. . . . . . . 8
⊢ ((𝑦 ∈ On ∧ ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} = suc
𝑦) → ¬ 𝐴 ⊆ (ℵ‘𝑦)) |
39 | 38 | adantl 481 |
. . . . . . 7
⊢
(((card‘𝐴) =
𝐴 ∧ (𝑦 ∈ On ∧ ∩
{𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦)) → ¬ 𝐴 ⊆ (ℵ‘𝑦)) |
40 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} = suc
𝑦 →
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) = (ℵ‘suc 𝑦)) |
41 | | alephsuc 8774 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ On →
(ℵ‘suc 𝑦) =
(har‘(ℵ‘𝑦))) |
42 | 40, 41 | sylan9eqr 2666 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ On ∧ ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} = suc
𝑦) →
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) = (har‘(ℵ‘𝑦))) |
43 | 42 | eleq2d 2673 |
. . . . . . . . 9
⊢ ((𝑦 ∈ On ∧ ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} = suc
𝑦) → (𝐴 ∈ (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) ↔
𝐴 ∈
(har‘(ℵ‘𝑦)))) |
44 | 43 | biimpd 218 |
. . . . . . . 8
⊢ ((𝑦 ∈ On ∧ ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} = suc
𝑦) → (𝐴 ∈ (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) →
𝐴 ∈
(har‘(ℵ‘𝑦)))) |
45 | | elharval 8351 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(har‘(ℵ‘𝑦)) ↔ (𝐴 ∈ On ∧ 𝐴 ≼ (ℵ‘𝑦))) |
46 | 45 | simprbi 479 |
. . . . . . . . 9
⊢ (𝐴 ∈
(har‘(ℵ‘𝑦)) → 𝐴 ≼ (ℵ‘𝑦)) |
47 | | onenon 8658 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On → 𝐴 ∈ dom
card) |
48 | 3, 47 | syl 17 |
. . . . . . . . . . 11
⊢
((card‘𝐴) =
𝐴 → 𝐴 ∈ dom card) |
49 | | alephon 8775 |
. . . . . . . . . . . 12
⊢
(ℵ‘𝑦)
∈ On |
50 | | onenon 8658 |
. . . . . . . . . . . 12
⊢
((ℵ‘𝑦)
∈ On → (ℵ‘𝑦) ∈ dom card) |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(ℵ‘𝑦)
∈ dom card |
52 | | carddom2 8686 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom card ∧
(ℵ‘𝑦) ∈
dom card) → ((card‘𝐴) ⊆ (card‘(ℵ‘𝑦)) ↔ 𝐴 ≼ (ℵ‘𝑦))) |
53 | 48, 51, 52 | sylancl 693 |
. . . . . . . . . 10
⊢
((card‘𝐴) =
𝐴 → ((card‘𝐴) ⊆
(card‘(ℵ‘𝑦)) ↔ 𝐴 ≼ (ℵ‘𝑦))) |
54 | | sseq1 3589 |
. . . . . . . . . . 11
⊢
((card‘𝐴) =
𝐴 → ((card‘𝐴) ⊆
(card‘(ℵ‘𝑦)) ↔ 𝐴 ⊆ (card‘(ℵ‘𝑦)))) |
55 | | alephcard 8776 |
. . . . . . . . . . . 12
⊢
(card‘(ℵ‘𝑦)) = (ℵ‘𝑦) |
56 | 55 | sseq2i 3593 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆
(card‘(ℵ‘𝑦)) ↔ 𝐴 ⊆ (ℵ‘𝑦)) |
57 | 54, 56 | syl6bb 275 |
. . . . . . . . . 10
⊢
((card‘𝐴) =
𝐴 → ((card‘𝐴) ⊆
(card‘(ℵ‘𝑦)) ↔ 𝐴 ⊆ (ℵ‘𝑦))) |
58 | 53, 57 | bitr3d 269 |
. . . . . . . . 9
⊢
((card‘𝐴) =
𝐴 → (𝐴 ≼ (ℵ‘𝑦) ↔ 𝐴 ⊆ (ℵ‘𝑦))) |
59 | 46, 58 | syl5ib 233 |
. . . . . . . 8
⊢
((card‘𝐴) =
𝐴 → (𝐴 ∈ (har‘(ℵ‘𝑦)) → 𝐴 ⊆ (ℵ‘𝑦))) |
60 | 44, 59 | sylan9r 688 |
. . . . . . 7
⊢
(((card‘𝐴) =
𝐴 ∧ (𝑦 ∈ On ∧ ∩
{𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦)) → (𝐴 ∈ (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) →
𝐴 ⊆
(ℵ‘𝑦))) |
61 | 39, 60 | mtod 188 |
. . . . . 6
⊢
(((card‘𝐴) =
𝐴 ∧ (𝑦 ∈ On ∧ ∩
{𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦)) → ¬ 𝐴 ∈ (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)})) |
62 | 61 | rexlimdvaa 3014 |
. . . . 5
⊢
((card‘𝐴) =
𝐴 → (∃𝑦 ∈ On ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} = suc
𝑦 → ¬ 𝐴 ∈ (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}))) |
63 | | onintrab2 6894 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈ On
𝐴 ⊆
(ℵ‘𝑥) ↔
∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} ∈ On) |
64 | 8, 63 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On → ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} ∈
On) |
65 | | onelon 5665 |
. . . . . . . . . . . . 13
⊢ ((∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} ∈
On ∧ 𝑦 ∈ ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) →
𝑦 ∈
On) |
66 | 64, 65 | sylan 487 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) →
𝑦 ∈
On) |
67 | 36 | adantld 482 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ On → ((𝐴 ∈ On ∧ 𝑦 ∈ ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) →
¬ 𝐴 ⊆
(ℵ‘𝑦))) |
68 | 66, 67 | mpcom 37 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) →
¬ 𝐴 ⊆
(ℵ‘𝑦)) |
69 | 49 | onelssi 5753 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (ℵ‘𝑦) → 𝐴 ⊆ (ℵ‘𝑦)) |
70 | 68, 69 | nsyl 134 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) →
¬ 𝐴 ∈
(ℵ‘𝑦)) |
71 | 70 | nrexdv 2984 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → ¬
∃𝑦 ∈ ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}𝐴 ∈ (ℵ‘𝑦)) |
72 | 71 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ Lim ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) →
¬ ∃𝑦 ∈ ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}𝐴 ∈ (ℵ‘𝑦)) |
73 | | alephlim 8773 |
. . . . . . . . . . 11
⊢ ((∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} ∈
On ∧ Lim ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) → (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) =
∪ 𝑦 ∈ ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} (ℵ‘𝑦)) |
74 | 64, 73 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ Lim ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) →
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) = ∪
𝑦 ∈ ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}
(ℵ‘𝑦)) |
75 | 74 | eleq2d 2673 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ Lim ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) →
(𝐴 ∈
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ↔ 𝐴 ∈ ∪
𝑦 ∈ ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}
(ℵ‘𝑦))) |
76 | | eliun 4460 |
. . . . . . . . 9
⊢ (𝐴 ∈ ∪ 𝑦 ∈ ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} (ℵ‘𝑦) ↔ ∃𝑦 ∈ ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}𝐴 ∈ (ℵ‘𝑦)) |
77 | 75, 76 | syl6bb 275 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ Lim ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) →
(𝐴 ∈
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ↔ ∃𝑦 ∈ ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}𝐴 ∈ (ℵ‘𝑦))) |
78 | 72, 77 | mtbird 314 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ Lim ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) →
¬ 𝐴 ∈
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)})) |
79 | 78 | ex 449 |
. . . . . 6
⊢ (𝐴 ∈ On → (Lim ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} →
¬ 𝐴 ∈
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))) |
80 | 3, 79 | syl 17 |
. . . . 5
⊢
((card‘𝐴) =
𝐴 → (Lim ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} →
¬ 𝐴 ∈
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))) |
81 | 62, 80 | jaod 394 |
. . . 4
⊢
((card‘𝐴) =
𝐴 → ((∃𝑦 ∈ On ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} = suc
𝑦 ∨ Lim ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) →
¬ 𝐴 ∈
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))) |
82 | 8, 17 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ On → 𝐴 ⊆ (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)})) |
83 | | alephon 8775 |
. . . . . . 7
⊢
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ∈ On |
84 | | onsseleq 5682 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ∈ On) → (𝐴 ⊆ (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) ↔
(𝐴 ∈
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ∨ 𝐴 = (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)})))) |
85 | 83, 84 | mpan2 703 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝐴 ⊆ (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) ↔
(𝐴 ∈
(ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ∨ 𝐴 = (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)})))) |
86 | 82, 85 | mpbid 221 |
. . . . 5
⊢ (𝐴 ∈ On → (𝐴 ∈ (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) ∨
𝐴 = (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}))) |
87 | 86 | ord 391 |
. . . 4
⊢ (𝐴 ∈ On → (¬ 𝐴 ∈ (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) →
𝐴 = (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}))) |
88 | 3, 81, 87 | sylsyld 59 |
. . 3
⊢
((card‘𝐴) =
𝐴 → ((∃𝑦 ∈ On ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} = suc
𝑦 ∨ Lim ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) →
𝐴 = (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}))) |
89 | 88 | adantl 481 |
. 2
⊢ ((ω
⊆ 𝐴 ∧
(card‘𝐴) = 𝐴) → ((∃𝑦 ∈ On ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} = suc
𝑦 ∨ Lim ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}) →
𝐴 = (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}))) |
90 | | eloni 5650 |
. . . . 5
⊢ (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} ∈
On → Ord ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) |
91 | | ordzsl 6937 |
. . . . . 6
⊢ (Ord
∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} ↔ (∩
{𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ ∨ ∃𝑦 ∈ On ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} = suc
𝑦 ∨ Lim ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)})) |
92 | | 3orass 1034 |
. . . . . 6
⊢ ((∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} =
∅ ∨ ∃𝑦
∈ On ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 ∨ Lim ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}) ↔ (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} =
∅ ∨ (∃𝑦
∈ On ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 ∨ Lim ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))) |
93 | 91, 92 | bitri 263 |
. . . . 5
⊢ (Ord
∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} ↔ (∩
{𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ ∨ (∃𝑦 ∈ On ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} = suc
𝑦 ∨ Lim ∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)}))) |
94 | 90, 93 | sylib 207 |
. . . 4
⊢ (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} ∈
On → (∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = ∅ ∨ (∃𝑦 ∈ On ∩
{𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 ∨ Lim ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))) |
95 | 3, 64, 94 | 3syl 18 |
. . 3
⊢
((card‘𝐴) =
𝐴 → (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} =
∅ ∨ (∃𝑦
∈ On ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 ∨ Lim ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))) |
96 | 95 | adantl 481 |
. 2
⊢ ((ω
⊆ 𝐴 ∧
(card‘𝐴) = 𝐴) → (∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)} =
∅ ∨ (∃𝑦
∈ On ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)} = suc 𝑦 ∨ Lim ∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))) |
97 | 29, 89, 96 | mpjaod 395 |
1
⊢ ((ω
⊆ 𝐴 ∧
(card‘𝐴) = 𝐴) → 𝐴 = (ℵ‘∩ {𝑥
∈ On ∣ 𝐴 ⊆
(ℵ‘𝑥)})) |