Step | Hyp | Ref
| Expression |
1 | | onzsl 7424 |
. . . 4
⊢ (𝐴 ∈ On ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴))) |
2 | 1 | biimpi 217 |
. . 3
⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴))) |
3 | | cfom 9539 |
. . . . . . 7
⊢
(cf‘ω) = ω |
4 | | aleph0 9345 |
. . . . . . . 8
⊢
(ℵ‘∅) = ω |
5 | 4 | fveq2i 6548 |
. . . . . . 7
⊢
(cf‘(ℵ‘∅)) = (cf‘ω) |
6 | 3, 5, 4 | 3eqtr4i 2831 |
. . . . . 6
⊢
(cf‘(ℵ‘∅)) =
(ℵ‘∅) |
7 | | 2fveq3 6550 |
. . . . . 6
⊢ (𝐴 = ∅ →
(cf‘(ℵ‘𝐴)) =
(cf‘(ℵ‘∅))) |
8 | | fveq2 6545 |
. . . . . 6
⊢ (𝐴 = ∅ →
(ℵ‘𝐴) =
(ℵ‘∅)) |
9 | 6, 7, 8 | 3eqtr4a 2859 |
. . . . 5
⊢ (𝐴 = ∅ →
(cf‘(ℵ‘𝐴)) = (ℵ‘𝐴)) |
10 | | fvex 6558 |
. . . . . . . . 9
⊢
(ℵ‘𝐴)
∈ V |
11 | 10 | canth2 8524 |
. . . . . . . 8
⊢
(ℵ‘𝐴)
≺ 𝒫 (ℵ‘𝐴) |
12 | 10 | pw2en 8478 |
. . . . . . . 8
⊢ 𝒫
(ℵ‘𝐴) ≈
(2o ↑𝑚 (ℵ‘𝐴)) |
13 | | sdomentr 8505 |
. . . . . . . 8
⊢
(((ℵ‘𝐴)
≺ 𝒫 (ℵ‘𝐴) ∧ 𝒫 (ℵ‘𝐴) ≈ (2o
↑𝑚 (ℵ‘𝐴))) → (ℵ‘𝐴) ≺ (2o
↑𝑚 (ℵ‘𝐴))) |
14 | 11, 12, 13 | mp2an 688 |
. . . . . . 7
⊢
(ℵ‘𝐴)
≺ (2o ↑𝑚 (ℵ‘𝐴)) |
15 | | alephon 9348 |
. . . . . . . . 9
⊢
(ℵ‘𝐴)
∈ On |
16 | | alephgeom 9361 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On ↔ ω
⊆ (ℵ‘𝐴)) |
17 | | omelon 8962 |
. . . . . . . . . . . 12
⊢ ω
∈ On |
18 | | 2onn 8123 |
. . . . . . . . . . . 12
⊢
2o ∈ ω |
19 | | onelss 6115 |
. . . . . . . . . . . 12
⊢ (ω
∈ On → (2o ∈ ω → 2o ⊆
ω)) |
20 | 17, 18, 19 | mp2 9 |
. . . . . . . . . . 11
⊢
2o ⊆ ω |
21 | | sstr 3903 |
. . . . . . . . . . 11
⊢
((2o ⊆ ω ∧ ω ⊆
(ℵ‘𝐴)) →
2o ⊆ (ℵ‘𝐴)) |
22 | 20, 21 | mpan 686 |
. . . . . . . . . 10
⊢ (ω
⊆ (ℵ‘𝐴)
→ 2o ⊆ (ℵ‘𝐴)) |
23 | 16, 22 | sylbi 218 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → 2o
⊆ (ℵ‘𝐴)) |
24 | | ssdomg 8410 |
. . . . . . . . 9
⊢
((ℵ‘𝐴)
∈ On → (2o ⊆ (ℵ‘𝐴) → 2o ≼
(ℵ‘𝐴))) |
25 | 15, 23, 24 | mpsyl 68 |
. . . . . . . 8
⊢ (𝐴 ∈ On → 2o
≼ (ℵ‘𝐴)) |
26 | | mapdom1 8536 |
. . . . . . . 8
⊢
(2o ≼ (ℵ‘𝐴) → (2o
↑𝑚 (ℵ‘𝐴)) ≼ ((ℵ‘𝐴) ↑𝑚
(ℵ‘𝐴))) |
27 | 25, 26 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ On → (2o
↑𝑚 (ℵ‘𝐴)) ≼ ((ℵ‘𝐴) ↑𝑚
(ℵ‘𝐴))) |
28 | | sdomdomtr 8504 |
. . . . . . 7
⊢
(((ℵ‘𝐴)
≺ (2o ↑𝑚 (ℵ‘𝐴)) ∧ (2o
↑𝑚 (ℵ‘𝐴)) ≼ ((ℵ‘𝐴) ↑𝑚
(ℵ‘𝐴))) →
(ℵ‘𝐴) ≺
((ℵ‘𝐴)
↑𝑚 (ℵ‘𝐴))) |
29 | 14, 27, 28 | sylancr 587 |
. . . . . 6
⊢ (𝐴 ∈ On →
(ℵ‘𝐴) ≺
((ℵ‘𝐴)
↑𝑚 (ℵ‘𝐴))) |
30 | | oveq2 7031 |
. . . . . . 7
⊢
((cf‘(ℵ‘𝐴)) = (ℵ‘𝐴) → ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))) = ((ℵ‘𝐴) ↑𝑚
(ℵ‘𝐴))) |
31 | 30 | breq2d 4980 |
. . . . . 6
⊢
((cf‘(ℵ‘𝐴)) = (ℵ‘𝐴) → ((ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))) ↔ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(ℵ‘𝐴)))) |
32 | 29, 31 | syl5ibrcom 248 |
. . . . 5
⊢ (𝐴 ∈ On →
((cf‘(ℵ‘𝐴)) = (ℵ‘𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))))) |
33 | 9, 32 | syl5 34 |
. . . 4
⊢ (𝐴 ∈ On → (𝐴 = ∅ →
(ℵ‘𝐴) ≺
((ℵ‘𝐴)
↑𝑚 (cf‘(ℵ‘𝐴))))) |
34 | | alephreg 9857 |
. . . . . . 7
⊢
(cf‘(ℵ‘suc 𝑥)) = (ℵ‘suc 𝑥) |
35 | | 2fveq3 6550 |
. . . . . . 7
⊢ (𝐴 = suc 𝑥 → (cf‘(ℵ‘𝐴)) =
(cf‘(ℵ‘suc 𝑥))) |
36 | | fveq2 6545 |
. . . . . . 7
⊢ (𝐴 = suc 𝑥 → (ℵ‘𝐴) = (ℵ‘suc 𝑥)) |
37 | 34, 35, 36 | 3eqtr4a 2859 |
. . . . . 6
⊢ (𝐴 = suc 𝑥 → (cf‘(ℵ‘𝐴)) = (ℵ‘𝐴)) |
38 | 37 | rexlimivw 3247 |
. . . . 5
⊢
(∃𝑥 ∈ On
𝐴 = suc 𝑥 → (cf‘(ℵ‘𝐴)) = (ℵ‘𝐴)) |
39 | 38, 32 | syl5 34 |
. . . 4
⊢ (𝐴 ∈ On → (∃𝑥 ∈ On 𝐴 = suc 𝑥 → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))))) |
40 | | cfsmo 9546 |
. . . . . 6
⊢
((ℵ‘𝐴)
∈ On → ∃𝑓(𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) |
41 | | limelon 6136 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ∈ On) |
42 | | ffn 6389 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → 𝑓 Fn (cf‘(ℵ‘𝐴))) |
43 | | fnrnfv 6600 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 Fn
(cf‘(ℵ‘𝐴)) → ran 𝑓 = {𝑦 ∣ ∃𝑥 ∈ (cf‘(ℵ‘𝐴))𝑦 = (𝑓‘𝑥)}) |
44 | 43 | unieqd 4761 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 Fn
(cf‘(ℵ‘𝐴)) → ∪ ran
𝑓 = ∪ {𝑦
∣ ∃𝑥 ∈
(cf‘(ℵ‘𝐴))𝑦 = (𝑓‘𝑥)}) |
45 | 42, 44 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ∪ ran 𝑓 = ∪ {𝑦 ∣ ∃𝑥 ∈
(cf‘(ℵ‘𝐴))𝑦 = (𝑓‘𝑥)}) |
46 | | fvex 6558 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓‘𝑥) ∈ V |
47 | 46 | dfiun2 4867 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓‘𝑥) = ∪ {𝑦 ∣ ∃𝑥 ∈
(cf‘(ℵ‘𝐴))𝑦 = (𝑓‘𝑥)} |
48 | 45, 47 | syl6eqr 2851 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ∪ ran 𝑓 = ∪ 𝑥 ∈
(cf‘(ℵ‘𝐴))(𝑓‘𝑥)) |
49 | 48 | ad2antrl 724 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → ∪ ran
𝑓 = ∪ 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓‘𝑥)) |
50 | | fnfvelrn 6720 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 Fn
(cf‘(ℵ‘𝐴)) ∧ 𝑤 ∈ (cf‘(ℵ‘𝐴))) → (𝑓‘𝑤) ∈ ran 𝑓) |
51 | 42, 50 | sylan 580 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑤 ∈ (cf‘(ℵ‘𝐴))) → (𝑓‘𝑤) ∈ ran 𝑓) |
52 | | sseq2 3920 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑓‘𝑤) → (𝑧 ⊆ 𝑦 ↔ 𝑧 ⊆ (𝑓‘𝑤))) |
53 | 52 | rspcev 3561 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓‘𝑤) ∈ ran 𝑓 ∧ 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦) |
54 | 51, 53 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑤 ∈ (cf‘(ℵ‘𝐴))) ∧ 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦) |
55 | 54 | rexlimdva2 3252 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → (∃𝑤 ∈
(cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤) → ∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦)) |
56 | 55 | ralimdv 3147 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → (∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤) → ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦)) |
57 | 56 | imp 407 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤)) → ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦) |
58 | 57 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦) |
59 | | alephislim 9362 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ On ↔ Lim
(ℵ‘𝐴)) |
60 | 59 | biimpi 217 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ On → Lim
(ℵ‘𝐴)) |
61 | | frn 6395 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ran 𝑓 ⊆ (ℵ‘𝐴)) |
62 | 61 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤)) → ran 𝑓 ⊆ (ℵ‘𝐴)) |
63 | | coflim 9536 |
. . . . . . . . . . . . . . 15
⊢ ((Lim
(ℵ‘𝐴) ∧ ran
𝑓 ⊆
(ℵ‘𝐴)) →
(∪ ran 𝑓 = (ℵ‘𝐴) ↔ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦)) |
64 | 60, 62, 63 | syl2an 595 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → (∪ ran
𝑓 = (ℵ‘𝐴) ↔ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦)) |
65 | 58, 64 | mpbird 258 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → ∪ ran
𝑓 = (ℵ‘𝐴)) |
66 | 49, 65 | eqtr3d 2835 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → ∪ 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓‘𝑥) = (ℵ‘𝐴)) |
67 | | ffvelrn 6721 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝑓‘𝑥) ∈ (ℵ‘𝐴)) |
68 | 15 | oneli 6180 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓‘𝑥) ∈ (ℵ‘𝐴) → (𝑓‘𝑥) ∈ On) |
69 | | harcard 9260 |
. . . . . . . . . . . . . . . . . . 19
⊢
(card‘(har‘(𝑓‘𝑥))) = (har‘(𝑓‘𝑥)) |
70 | | iscard 9257 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((card‘(har‘(𝑓‘𝑥))) = (har‘(𝑓‘𝑥)) ↔ ((har‘(𝑓‘𝑥)) ∈ On ∧ ∀𝑦 ∈ (har‘(𝑓‘𝑥))𝑦 ≺ (har‘(𝑓‘𝑥)))) |
71 | 70 | simprbi 497 |
. . . . . . . . . . . . . . . . . . 19
⊢
((card‘(har‘(𝑓‘𝑥))) = (har‘(𝑓‘𝑥)) → ∀𝑦 ∈ (har‘(𝑓‘𝑥))𝑦 ≺ (har‘(𝑓‘𝑥))) |
72 | 69, 71 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
∀𝑦 ∈
(har‘(𝑓‘𝑥))𝑦 ≺ (har‘(𝑓‘𝑥)) |
73 | | domrefg 8399 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓‘𝑥) ∈ V → (𝑓‘𝑥) ≼ (𝑓‘𝑥)) |
74 | 46, 73 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓‘𝑥) ≼ (𝑓‘𝑥) |
75 | | elharval 8880 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓‘𝑥) ∈ (har‘(𝑓‘𝑥)) ↔ ((𝑓‘𝑥) ∈ On ∧ (𝑓‘𝑥) ≼ (𝑓‘𝑥))) |
76 | 75 | biimpri 229 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓‘𝑥) ∈ On ∧ (𝑓‘𝑥) ≼ (𝑓‘𝑥)) → (𝑓‘𝑥) ∈ (har‘(𝑓‘𝑥))) |
77 | 74, 76 | mpan2 687 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓‘𝑥) ∈ On → (𝑓‘𝑥) ∈ (har‘(𝑓‘𝑥))) |
78 | | breq1 4971 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝑓‘𝑥) → (𝑦 ≺ (har‘(𝑓‘𝑥)) ↔ (𝑓‘𝑥) ≺ (har‘(𝑓‘𝑥)))) |
79 | 78 | rspccv 3558 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑦 ∈
(har‘(𝑓‘𝑥))𝑦 ≺ (har‘(𝑓‘𝑥)) → ((𝑓‘𝑥) ∈ (har‘(𝑓‘𝑥)) → (𝑓‘𝑥) ≺ (har‘(𝑓‘𝑥)))) |
80 | 72, 77, 79 | mpsyl 68 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓‘𝑥) ∈ On → (𝑓‘𝑥) ≺ (har‘(𝑓‘𝑥))) |
81 | 67, 68, 80 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝑓‘𝑥) ≺ (har‘(𝑓‘𝑥))) |
82 | | harcl 8878 |
. . . . . . . . . . . . . . . . . . 19
⊢
(har‘(𝑓‘𝑥)) ∈ On |
83 | | 2fveq3 6550 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → (har‘(𝑓‘𝑦)) = (har‘(𝑓‘𝑥))) |
84 | | pwcfsdom.1 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐻 = (𝑦 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓‘𝑦))) |
85 | 83, 84 | fvmptg 6640 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈
(cf‘(ℵ‘𝐴)) ∧ (har‘(𝑓‘𝑥)) ∈ On) → (𝐻‘𝑥) = (har‘(𝑓‘𝑥))) |
86 | 82, 85 | mpan2 687 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈
(cf‘(ℵ‘𝐴)) → (𝐻‘𝑥) = (har‘(𝑓‘𝑥))) |
87 | 86 | breq2d 4980 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈
(cf‘(ℵ‘𝐴)) → ((𝑓‘𝑥) ≺ (𝐻‘𝑥) ↔ (𝑓‘𝑥) ≺ (har‘(𝑓‘𝑥)))) |
88 | 87 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → ((𝑓‘𝑥) ≺ (𝐻‘𝑥) ↔ (𝑓‘𝑥) ≺ (har‘(𝑓‘𝑥)))) |
89 | 81, 88 | mpbird 258 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝑓‘𝑥) ≺ (𝐻‘𝑥)) |
90 | 89 | ralrimiva 3151 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ∀𝑥 ∈
(cf‘(ℵ‘𝐴))(𝑓‘𝑥) ≺ (𝐻‘𝑥)) |
91 | | fvex 6558 |
. . . . . . . . . . . . . . 15
⊢
(cf‘(ℵ‘𝐴)) ∈ V |
92 | | eqid 2797 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓‘𝑥) = ∪ 𝑥 ∈
(cf‘(ℵ‘𝐴))(𝑓‘𝑥) |
93 | | eqid 2797 |
. . . . . . . . . . . . . . 15
⊢ X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) = X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) |
94 | 91, 92, 93 | konigth 9844 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
(cf‘(ℵ‘𝐴))(𝑓‘𝑥) ≺ (𝐻‘𝑥) → ∪
𝑥 ∈
(cf‘(ℵ‘𝐴))(𝑓‘𝑥) ≺ X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥)) |
95 | 90, 94 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ∪ 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓‘𝑥) ≺ X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥)) |
96 | 95 | ad2antrl 724 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → ∪ 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓‘𝑥) ≺ X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥)) |
97 | 66, 96 | eqbrtrrd 4992 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → (ℵ‘𝐴) ≺ X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥)) |
98 | 41, 97 | sylan 580 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → (ℵ‘𝐴) ≺ X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥)) |
99 | | ovex 7055 |
. . . . . . . . . . . 12
⊢
((ℵ‘𝐴)
↑𝑚 (cf‘(ℵ‘𝐴))) ∈ V |
100 | 67 | ex 413 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → (𝑥 ∈ (cf‘(ℵ‘𝐴)) → (𝑓‘𝑥) ∈ (ℵ‘𝐴))) |
101 | | alephlim 9346 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) = ∪ 𝑦 ∈ 𝐴 (ℵ‘𝑦)) |
102 | 101 | eleq2d 2870 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ((𝑓‘𝑥) ∈ (ℵ‘𝐴) ↔ (𝑓‘𝑥) ∈ ∪
𝑦 ∈ 𝐴 (ℵ‘𝑦))) |
103 | | eliun 4835 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓‘𝑥) ∈ ∪
𝑦 ∈ 𝐴 (ℵ‘𝑦) ↔ ∃𝑦 ∈ 𝐴 (𝑓‘𝑥) ∈ (ℵ‘𝑦)) |
104 | | alephcard 9349 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(card‘(ℵ‘𝑦)) = (ℵ‘𝑦) |
105 | 104 | eleq2i 2876 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓‘𝑥) ∈ (card‘(ℵ‘𝑦)) ↔ (𝑓‘𝑥) ∈ (ℵ‘𝑦)) |
106 | | cardsdomelir 9255 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓‘𝑥) ∈ (card‘(ℵ‘𝑦)) → (𝑓‘𝑥) ≺ (ℵ‘𝑦)) |
107 | 105, 106 | sylbir 236 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓‘𝑥) ∈ (ℵ‘𝑦) → (𝑓‘𝑥) ≺ (ℵ‘𝑦)) |
108 | | elharval 8880 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((ℵ‘𝑦)
∈ (har‘(𝑓‘𝑥)) ↔ ((ℵ‘𝑦) ∈ On ∧ (ℵ‘𝑦) ≼ (𝑓‘𝑥))) |
109 | 108 | simprbi 497 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((ℵ‘𝑦)
∈ (har‘(𝑓‘𝑥)) → (ℵ‘𝑦) ≼ (𝑓‘𝑥)) |
110 | | domnsym 8497 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((ℵ‘𝑦)
≼ (𝑓‘𝑥) → ¬ (𝑓‘𝑥) ≺ (ℵ‘𝑦)) |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((ℵ‘𝑦)
∈ (har‘(𝑓‘𝑥)) → ¬ (𝑓‘𝑥) ≺ (ℵ‘𝑦)) |
112 | 111 | con2i 141 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓‘𝑥) ≺ (ℵ‘𝑦) → ¬ (ℵ‘𝑦) ∈ (har‘(𝑓‘𝑥))) |
113 | | alephon 9348 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(ℵ‘𝑦)
∈ On |
114 | | ontri1 6107 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((har‘(𝑓‘𝑥)) ∈ On ∧ (ℵ‘𝑦) ∈ On) →
((har‘(𝑓‘𝑥)) ⊆ (ℵ‘𝑦) ↔ ¬
(ℵ‘𝑦) ∈
(har‘(𝑓‘𝑥)))) |
115 | 82, 113, 114 | mp2an 688 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((har‘(𝑓‘𝑥)) ⊆ (ℵ‘𝑦) ↔ ¬ (ℵ‘𝑦) ∈ (har‘(𝑓‘𝑥))) |
116 | 112, 115 | sylibr 235 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓‘𝑥) ≺ (ℵ‘𝑦) → (har‘(𝑓‘𝑥)) ⊆ (ℵ‘𝑦)) |
117 | 107, 116 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓‘𝑥) ∈ (ℵ‘𝑦) → (har‘(𝑓‘𝑥)) ⊆ (ℵ‘𝑦)) |
118 | | alephord2i 9356 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ On → (𝑦 ∈ 𝐴 → (ℵ‘𝑦) ∈ (ℵ‘𝐴))) |
119 | 118 | imp 407 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → (ℵ‘𝑦) ∈ (ℵ‘𝐴)) |
120 | | ontr2 6120 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((har‘(𝑓‘𝑥)) ∈ On ∧ (ℵ‘𝐴) ∈ On) →
(((har‘(𝑓‘𝑥)) ⊆ (ℵ‘𝑦) ∧ (ℵ‘𝑦) ∈ (ℵ‘𝐴)) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴))) |
121 | 82, 15, 120 | mp2an 688 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((har‘(𝑓‘𝑥)) ⊆ (ℵ‘𝑦) ∧ (ℵ‘𝑦) ∈ (ℵ‘𝐴)) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴)) |
122 | 117, 119,
121 | syl2anr 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ (𝑓‘𝑥) ∈ (ℵ‘𝑦)) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴)) |
123 | 122 | rexlimdva2 3252 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ On → (∃𝑦 ∈ 𝐴 (𝑓‘𝑥) ∈ (ℵ‘𝑦) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴))) |
124 | 103, 123 | syl5bi 243 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ On → ((𝑓‘𝑥) ∈ ∪
𝑦 ∈ 𝐴 (ℵ‘𝑦) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴))) |
125 | 41, 124 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ((𝑓‘𝑥) ∈ ∪
𝑦 ∈ 𝐴 (ℵ‘𝑦) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴))) |
126 | 102, 125 | sylbid 241 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ((𝑓‘𝑥) ∈ (ℵ‘𝐴) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴))) |
127 | 100, 126 | sylan9r 509 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) → (𝑥 ∈ (cf‘(ℵ‘𝐴)) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴))) |
128 | 127 | imp 407 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴)) |
129 | 83 | cbvmptv 5068 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈
(cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓‘𝑦))) = (𝑥 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓‘𝑥))) |
130 | 84, 129 | eqtri 2821 |
. . . . . . . . . . . . . 14
⊢ 𝐻 = (𝑥 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓‘𝑥))) |
131 | 128, 130 | fmptd 6748 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) → 𝐻:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) |
132 | | ffvelrn 6721 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝐻‘𝑥) ∈ (ℵ‘𝐴)) |
133 | | onelss 6115 |
. . . . . . . . . . . . . . 15
⊢
((ℵ‘𝐴)
∈ On → ((𝐻‘𝑥) ∈ (ℵ‘𝐴) → (𝐻‘𝑥) ⊆ (ℵ‘𝐴))) |
134 | 15, 132, 133 | mpsyl 68 |
. . . . . . . . . . . . . 14
⊢ ((𝐻:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝐻‘𝑥) ⊆ (ℵ‘𝐴)) |
135 | 134 | ralrimiva 3151 |
. . . . . . . . . . . . 13
⊢ (𝐻:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ∀𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ⊆ (ℵ‘𝐴)) |
136 | | ss2ixp 8330 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ⊆ (ℵ‘𝐴) → X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ⊆ X𝑥 ∈
(cf‘(ℵ‘𝐴))(ℵ‘𝐴)) |
137 | 91, 10 | ixpconst 8327 |
. . . . . . . . . . . . . 14
⊢ X𝑥 ∈
(cf‘(ℵ‘𝐴))(ℵ‘𝐴) = ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))) |
138 | 136, 137 | syl6sseq 3944 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ⊆ (ℵ‘𝐴) → X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ⊆ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) |
139 | 131, 135,
138 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) → X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ⊆ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) |
140 | | ssdomg 8410 |
. . . . . . . . . . . 12
⊢
(((ℵ‘𝐴)
↑𝑚 (cf‘(ℵ‘𝐴))) ∈ V → (X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ⊆ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))) → X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ≼ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))))) |
141 | 99, 139, 140 | mpsyl 68 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) → X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ≼ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) |
142 | 141 | adantrr 713 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ≼ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) |
143 | | sdomdomtr 8504 |
. . . . . . . . . 10
⊢
(((ℵ‘𝐴)
≺ X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻‘𝑥) ∧ X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ≼ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) |
144 | 98, 142, 143 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) |
145 | 144 | expcom 414 |
. . . . . . . 8
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤)) → ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))))) |
146 | 145 | 3adant2 1124 |
. . . . . . 7
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤)) → ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))))) |
147 | 146 | exlimiv 1912 |
. . . . . 6
⊢
(∃𝑓(𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤)) → ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))))) |
148 | 15, 40, 147 | mp2b 10 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) |
149 | 148 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ On → ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))))) |
150 | 33, 39, 149 | 3jaod 1421 |
. . 3
⊢ (𝐴 ∈ On → ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴)) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))))) |
151 | 2, 150 | mpd 15 |
. 2
⊢ (𝐴 ∈ On →
(ℵ‘𝐴) ≺
((ℵ‘𝐴)
↑𝑚 (cf‘(ℵ‘𝐴)))) |
152 | | alephfnon 9344 |
. . . . 5
⊢ ℵ
Fn On |
153 | | fndm 6332 |
. . . . 5
⊢ (ℵ
Fn On → dom ℵ = On) |
154 | 152, 153 | ax-mp 5 |
. . . 4
⊢ dom
ℵ = On |
155 | 154 | eleq2i 2876 |
. . 3
⊢ (𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On) |
156 | | ndmfv 6575 |
. . . 4
⊢ (¬
𝐴 ∈ dom ℵ →
(ℵ‘𝐴) =
∅) |
157 | | 1n0 7977 |
. . . . . 6
⊢
1o ≠ ∅ |
158 | | 1oex 7968 |
. . . . . . 7
⊢
1o ∈ V |
159 | 158 | 0sdom 8502 |
. . . . . 6
⊢ (∅
≺ 1o ↔ 1o ≠ ∅) |
160 | 157, 159 | mpbir 232 |
. . . . 5
⊢ ∅
≺ 1o |
161 | | id 22 |
. . . . . 6
⊢
((ℵ‘𝐴) =
∅ → (ℵ‘𝐴) = ∅) |
162 | | fveq2 6545 |
. . . . . . . . 9
⊢
((ℵ‘𝐴) =
∅ → (cf‘(ℵ‘𝐴)) = (cf‘∅)) |
163 | | cf0 9526 |
. . . . . . . . 9
⊢
(cf‘∅) = ∅ |
164 | 162, 163 | syl6eq 2849 |
. . . . . . . 8
⊢
((ℵ‘𝐴) =
∅ → (cf‘(ℵ‘𝐴)) = ∅) |
165 | 161, 164 | oveq12d 7041 |
. . . . . . 7
⊢
((ℵ‘𝐴) =
∅ → ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))) = (∅ ↑𝑚
∅)) |
166 | | 0ex 5109 |
. . . . . . . 8
⊢ ∅
∈ V |
167 | | map0e 8303 |
. . . . . . . 8
⊢ (∅
∈ V → (∅ ↑𝑚 ∅) =
1o) |
168 | 166, 167 | ax-mp 5 |
. . . . . . 7
⊢ (∅
↑𝑚 ∅) = 1o |
169 | 165, 168 | syl6eq 2849 |
. . . . . 6
⊢
((ℵ‘𝐴) =
∅ → ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))) = 1o) |
170 | 161, 169 | breq12d 4981 |
. . . . 5
⊢
((ℵ‘𝐴) =
∅ → ((ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))) ↔ ∅ ≺
1o)) |
171 | 160, 170 | mpbiri 259 |
. . . 4
⊢
((ℵ‘𝐴) =
∅ → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) |
172 | 156, 171 | syl 17 |
. . 3
⊢ (¬
𝐴 ∈ dom ℵ →
(ℵ‘𝐴) ≺
((ℵ‘𝐴)
↑𝑚 (cf‘(ℵ‘𝐴)))) |
173 | 155, 172 | sylnbir 332 |
. 2
⊢ (¬
𝐴 ∈ On →
(ℵ‘𝐴) ≺
((ℵ‘𝐴)
↑𝑚 (cf‘(ℵ‘𝐴)))) |
174 | 151, 173 | pm2.61i 183 |
1
⊢
(ℵ‘𝐴)
≺ ((ℵ‘𝐴)
↑𝑚 (cf‘(ℵ‘𝐴))) |