Step | Hyp | Ref
| Expression |
1 | | onzsl 6938 |
. . . 4
⊢ (𝐴 ∈ On ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴))) |
2 | 1 | biimpi 205 |
. . 3
⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴))) |
3 | | cfom 8969 |
. . . . . . 7
⊢
(cf‘ω) = ω |
4 | | aleph0 8772 |
. . . . . . . 8
⊢
(ℵ‘∅) = ω |
5 | 4 | fveq2i 6106 |
. . . . . . 7
⊢
(cf‘(ℵ‘∅)) = (cf‘ω) |
6 | 3, 5, 4 | 3eqtr4i 2642 |
. . . . . 6
⊢
(cf‘(ℵ‘∅)) =
(ℵ‘∅) |
7 | | fveq2 6103 |
. . . . . . 7
⊢ (𝐴 = ∅ →
(ℵ‘𝐴) =
(ℵ‘∅)) |
8 | 7 | fveq2d 6107 |
. . . . . 6
⊢ (𝐴 = ∅ →
(cf‘(ℵ‘𝐴)) =
(cf‘(ℵ‘∅))) |
9 | 6, 8, 7 | 3eqtr4a 2670 |
. . . . 5
⊢ (𝐴 = ∅ →
(cf‘(ℵ‘𝐴)) = (ℵ‘𝐴)) |
10 | | fvex 6113 |
. . . . . . . . 9
⊢
(ℵ‘𝐴)
∈ V |
11 | 10 | canth2 7998 |
. . . . . . . 8
⊢
(ℵ‘𝐴)
≺ 𝒫 (ℵ‘𝐴) |
12 | 10 | pw2en 7952 |
. . . . . . . 8
⊢ 𝒫
(ℵ‘𝐴) ≈
(2𝑜 ↑𝑚 (ℵ‘𝐴)) |
13 | | sdomentr 7979 |
. . . . . . . 8
⊢
(((ℵ‘𝐴)
≺ 𝒫 (ℵ‘𝐴) ∧ 𝒫 (ℵ‘𝐴) ≈ (2𝑜
↑𝑚 (ℵ‘𝐴))) → (ℵ‘𝐴) ≺ (2𝑜
↑𝑚 (ℵ‘𝐴))) |
14 | 11, 12, 13 | mp2an 704 |
. . . . . . 7
⊢
(ℵ‘𝐴)
≺ (2𝑜 ↑𝑚 (ℵ‘𝐴)) |
15 | | alephon 8775 |
. . . . . . . . 9
⊢
(ℵ‘𝐴)
∈ On |
16 | | alephgeom 8788 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On ↔ ω
⊆ (ℵ‘𝐴)) |
17 | | omelon 8426 |
. . . . . . . . . . . 12
⊢ ω
∈ On |
18 | | 2onn 7607 |
. . . . . . . . . . . 12
⊢
2𝑜 ∈ ω |
19 | | onelss 5683 |
. . . . . . . . . . . 12
⊢ (ω
∈ On → (2𝑜 ∈ ω →
2𝑜 ⊆ ω)) |
20 | 17, 18, 19 | mp2 9 |
. . . . . . . . . . 11
⊢
2𝑜 ⊆ ω |
21 | | sstr 3576 |
. . . . . . . . . . 11
⊢
((2𝑜 ⊆ ω ∧ ω ⊆
(ℵ‘𝐴)) →
2𝑜 ⊆ (ℵ‘𝐴)) |
22 | 20, 21 | mpan 702 |
. . . . . . . . . 10
⊢ (ω
⊆ (ℵ‘𝐴)
→ 2𝑜 ⊆ (ℵ‘𝐴)) |
23 | 16, 22 | sylbi 206 |
. . . . . . . . 9
⊢ (𝐴 ∈ On →
2𝑜 ⊆ (ℵ‘𝐴)) |
24 | | ssdomg 7887 |
. . . . . . . . 9
⊢
((ℵ‘𝐴)
∈ On → (2𝑜 ⊆ (ℵ‘𝐴) → 2𝑜
≼ (ℵ‘𝐴))) |
25 | 15, 23, 24 | mpsyl 66 |
. . . . . . . 8
⊢ (𝐴 ∈ On →
2𝑜 ≼ (ℵ‘𝐴)) |
26 | | mapdom1 8010 |
. . . . . . . 8
⊢
(2𝑜 ≼ (ℵ‘𝐴) → (2𝑜
↑𝑚 (ℵ‘𝐴)) ≼ ((ℵ‘𝐴) ↑𝑚
(ℵ‘𝐴))) |
27 | 25, 26 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ On →
(2𝑜 ↑𝑚 (ℵ‘𝐴)) ≼ ((ℵ‘𝐴) ↑𝑚
(ℵ‘𝐴))) |
28 | | sdomdomtr 7978 |
. . . . . . 7
⊢
(((ℵ‘𝐴)
≺ (2𝑜 ↑𝑚 (ℵ‘𝐴)) ∧ (2𝑜
↑𝑚 (ℵ‘𝐴)) ≼ ((ℵ‘𝐴) ↑𝑚
(ℵ‘𝐴))) →
(ℵ‘𝐴) ≺
((ℵ‘𝐴)
↑𝑚 (ℵ‘𝐴))) |
29 | 14, 27, 28 | sylancr 694 |
. . . . . 6
⊢ (𝐴 ∈ On →
(ℵ‘𝐴) ≺
((ℵ‘𝐴)
↑𝑚 (ℵ‘𝐴))) |
30 | | oveq2 6557 |
. . . . . . 7
⊢
((cf‘(ℵ‘𝐴)) = (ℵ‘𝐴) → ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))) = ((ℵ‘𝐴) ↑𝑚
(ℵ‘𝐴))) |
31 | 30 | breq2d 4595 |
. . . . . 6
⊢
((cf‘(ℵ‘𝐴)) = (ℵ‘𝐴) → ((ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))) ↔ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(ℵ‘𝐴)))) |
32 | 29, 31 | syl5ibrcom 236 |
. . . . 5
⊢ (𝐴 ∈ On →
((cf‘(ℵ‘𝐴)) = (ℵ‘𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))))) |
33 | 9, 32 | syl5 33 |
. . . 4
⊢ (𝐴 ∈ On → (𝐴 = ∅ →
(ℵ‘𝐴) ≺
((ℵ‘𝐴)
↑𝑚 (cf‘(ℵ‘𝐴))))) |
34 | | alephreg 9283 |
. . . . . . 7
⊢
(cf‘(ℵ‘suc 𝑥)) = (ℵ‘suc 𝑥) |
35 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝐴 = suc 𝑥 → (ℵ‘𝐴) = (ℵ‘suc 𝑥)) |
36 | 35 | fveq2d 6107 |
. . . . . . 7
⊢ (𝐴 = suc 𝑥 → (cf‘(ℵ‘𝐴)) =
(cf‘(ℵ‘suc 𝑥))) |
37 | 34, 36, 35 | 3eqtr4a 2670 |
. . . . . 6
⊢ (𝐴 = suc 𝑥 → (cf‘(ℵ‘𝐴)) = (ℵ‘𝐴)) |
38 | 37 | rexlimivw 3011 |
. . . . 5
⊢
(∃𝑥 ∈ On
𝐴 = suc 𝑥 → (cf‘(ℵ‘𝐴)) = (ℵ‘𝐴)) |
39 | 38, 32 | syl5 33 |
. . . 4
⊢ (𝐴 ∈ On → (∃𝑥 ∈ On 𝐴 = suc 𝑥 → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))))) |
40 | | cfsmo 8976 |
. . . . . 6
⊢
((ℵ‘𝐴)
∈ On → ∃𝑓(𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) |
41 | | limelon 5705 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ∈ On) |
42 | | ffn 5958 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → 𝑓 Fn (cf‘(ℵ‘𝐴))) |
43 | | fnrnfv 6152 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 Fn
(cf‘(ℵ‘𝐴)) → ran 𝑓 = {𝑦 ∣ ∃𝑥 ∈ (cf‘(ℵ‘𝐴))𝑦 = (𝑓‘𝑥)}) |
44 | 43 | unieqd 4382 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 Fn
(cf‘(ℵ‘𝐴)) → ∪ ran
𝑓 = ∪ {𝑦
∣ ∃𝑥 ∈
(cf‘(ℵ‘𝐴))𝑦 = (𝑓‘𝑥)}) |
45 | 42, 44 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ∪ ran 𝑓 = ∪ {𝑦 ∣ ∃𝑥 ∈
(cf‘(ℵ‘𝐴))𝑦 = (𝑓‘𝑥)}) |
46 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓‘𝑥) ∈ V |
47 | 46 | dfiun2 4490 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓‘𝑥) = ∪ {𝑦 ∣ ∃𝑥 ∈
(cf‘(ℵ‘𝐴))𝑦 = (𝑓‘𝑥)} |
48 | 45, 47 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ∪ ran 𝑓 = ∪ 𝑥 ∈
(cf‘(ℵ‘𝐴))(𝑓‘𝑥)) |
49 | 48 | ad2antrl 760 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → ∪ ran
𝑓 = ∪ 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓‘𝑥)) |
50 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 Fn
(cf‘(ℵ‘𝐴)) ∧ 𝑤 ∈ (cf‘(ℵ‘𝐴))) → (𝑓‘𝑤) ∈ ran 𝑓) |
51 | 42, 50 | sylan 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑤 ∈ (cf‘(ℵ‘𝐴))) → (𝑓‘𝑤) ∈ ran 𝑓) |
52 | | sseq2 3590 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = (𝑓‘𝑤) → (𝑧 ⊆ 𝑦 ↔ 𝑧 ⊆ (𝑓‘𝑤))) |
53 | 52 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓‘𝑤) ∈ ran 𝑓 ∧ 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦) |
54 | 51, 53 | sylan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑤 ∈ (cf‘(ℵ‘𝐴))) ∧ 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦) |
55 | 54 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑤 ∈ (cf‘(ℵ‘𝐴))) → (𝑧 ⊆ (𝑓‘𝑤) → ∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦)) |
56 | 55 | rexlimdva 3013 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → (∃𝑤 ∈
(cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤) → ∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦)) |
57 | 56 | ralimdv 2946 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → (∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤) → ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦)) |
58 | 57 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤)) → ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦) |
59 | 58 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦) |
60 | | alephislim 8789 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ On ↔ Lim
(ℵ‘𝐴)) |
61 | 60 | biimpi 205 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ On → Lim
(ℵ‘𝐴)) |
62 | | frn 5966 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ran 𝑓 ⊆ (ℵ‘𝐴)) |
63 | 62 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤)) → ran 𝑓 ⊆ (ℵ‘𝐴)) |
64 | | coflim 8966 |
. . . . . . . . . . . . . . 15
⊢ ((Lim
(ℵ‘𝐴) ∧ ran
𝑓 ⊆
(ℵ‘𝐴)) →
(∪ ran 𝑓 = (ℵ‘𝐴) ↔ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦)) |
65 | 61, 63, 64 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → (∪ ran
𝑓 = (ℵ‘𝐴) ↔ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑦 ∈ ran 𝑓 𝑧 ⊆ 𝑦)) |
66 | 59, 65 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → ∪ ran
𝑓 = (ℵ‘𝐴)) |
67 | 49, 66 | eqtr3d 2646 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → ∪ 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓‘𝑥) = (ℵ‘𝐴)) |
68 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝑓‘𝑥) ∈ (ℵ‘𝐴)) |
69 | 15 | oneli 5752 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓‘𝑥) ∈ (ℵ‘𝐴) → (𝑓‘𝑥) ∈ On) |
70 | | harcard 8687 |
. . . . . . . . . . . . . . . . . . 19
⊢
(card‘(har‘(𝑓‘𝑥))) = (har‘(𝑓‘𝑥)) |
71 | | iscard 8684 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((card‘(har‘(𝑓‘𝑥))) = (har‘(𝑓‘𝑥)) ↔ ((har‘(𝑓‘𝑥)) ∈ On ∧ ∀𝑦 ∈ (har‘(𝑓‘𝑥))𝑦 ≺ (har‘(𝑓‘𝑥)))) |
72 | 71 | simprbi 479 |
. . . . . . . . . . . . . . . . . . 19
⊢
((card‘(har‘(𝑓‘𝑥))) = (har‘(𝑓‘𝑥)) → ∀𝑦 ∈ (har‘(𝑓‘𝑥))𝑦 ≺ (har‘(𝑓‘𝑥))) |
73 | 70, 72 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
∀𝑦 ∈
(har‘(𝑓‘𝑥))𝑦 ≺ (har‘(𝑓‘𝑥)) |
74 | | domrefg 7876 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓‘𝑥) ∈ V → (𝑓‘𝑥) ≼ (𝑓‘𝑥)) |
75 | 46, 74 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓‘𝑥) ≼ (𝑓‘𝑥) |
76 | | elharval 8351 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓‘𝑥) ∈ (har‘(𝑓‘𝑥)) ↔ ((𝑓‘𝑥) ∈ On ∧ (𝑓‘𝑥) ≼ (𝑓‘𝑥))) |
77 | 76 | biimpri 217 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓‘𝑥) ∈ On ∧ (𝑓‘𝑥) ≼ (𝑓‘𝑥)) → (𝑓‘𝑥) ∈ (har‘(𝑓‘𝑥))) |
78 | 75, 77 | mpan2 703 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓‘𝑥) ∈ On → (𝑓‘𝑥) ∈ (har‘(𝑓‘𝑥))) |
79 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝑓‘𝑥) → (𝑦 ≺ (har‘(𝑓‘𝑥)) ↔ (𝑓‘𝑥) ≺ (har‘(𝑓‘𝑥)))) |
80 | 79 | rspccv 3279 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑦 ∈
(har‘(𝑓‘𝑥))𝑦 ≺ (har‘(𝑓‘𝑥)) → ((𝑓‘𝑥) ∈ (har‘(𝑓‘𝑥)) → (𝑓‘𝑥) ≺ (har‘(𝑓‘𝑥)))) |
81 | 73, 78, 80 | mpsyl 66 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓‘𝑥) ∈ On → (𝑓‘𝑥) ≺ (har‘(𝑓‘𝑥))) |
82 | 68, 69, 81 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝑓‘𝑥) ≺ (har‘(𝑓‘𝑥))) |
83 | | harcl 8349 |
. . . . . . . . . . . . . . . . . . 19
⊢
(har‘(𝑓‘𝑥)) ∈ On |
84 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑥 → (𝑓‘𝑦) = (𝑓‘𝑥)) |
85 | 84 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → (har‘(𝑓‘𝑦)) = (har‘(𝑓‘𝑥))) |
86 | | pwcfsdom.1 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐻 = (𝑦 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓‘𝑦))) |
87 | 85, 86 | fvmptg 6189 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈
(cf‘(ℵ‘𝐴)) ∧ (har‘(𝑓‘𝑥)) ∈ On) → (𝐻‘𝑥) = (har‘(𝑓‘𝑥))) |
88 | 83, 87 | mpan2 703 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈
(cf‘(ℵ‘𝐴)) → (𝐻‘𝑥) = (har‘(𝑓‘𝑥))) |
89 | 88 | breq2d 4595 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈
(cf‘(ℵ‘𝐴)) → ((𝑓‘𝑥) ≺ (𝐻‘𝑥) ↔ (𝑓‘𝑥) ≺ (har‘(𝑓‘𝑥)))) |
90 | 89 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → ((𝑓‘𝑥) ≺ (𝐻‘𝑥) ↔ (𝑓‘𝑥) ≺ (har‘(𝑓‘𝑥)))) |
91 | 82, 90 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝑓‘𝑥) ≺ (𝐻‘𝑥)) |
92 | 91 | ralrimiva 2949 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ∀𝑥 ∈
(cf‘(ℵ‘𝐴))(𝑓‘𝑥) ≺ (𝐻‘𝑥)) |
93 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢
(cf‘(ℵ‘𝐴)) ∈ V |
94 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓‘𝑥) = ∪ 𝑥 ∈
(cf‘(ℵ‘𝐴))(𝑓‘𝑥) |
95 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) = X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) |
96 | 93, 94, 95 | konigth 9270 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
(cf‘(ℵ‘𝐴))(𝑓‘𝑥) ≺ (𝐻‘𝑥) → ∪
𝑥 ∈
(cf‘(ℵ‘𝐴))(𝑓‘𝑥) ≺ X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥)) |
97 | 92, 96 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ∪ 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓‘𝑥) ≺ X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥)) |
98 | 97 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → ∪ 𝑥 ∈ (cf‘(ℵ‘𝐴))(𝑓‘𝑥) ≺ X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥)) |
99 | 67, 98 | eqbrtrrd 4607 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → (ℵ‘𝐴) ≺ X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥)) |
100 | 41, 99 | sylan 487 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → (ℵ‘𝐴) ≺ X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥)) |
101 | | ovex 6577 |
. . . . . . . . . . . 12
⊢
((ℵ‘𝐴)
↑𝑚 (cf‘(ℵ‘𝐴))) ∈ V |
102 | 68 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → (𝑥 ∈ (cf‘(ℵ‘𝐴)) → (𝑓‘𝑥) ∈ (ℵ‘𝐴))) |
103 | | alephlim 8773 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) = ∪ 𝑦 ∈ 𝐴 (ℵ‘𝑦)) |
104 | 103 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ((𝑓‘𝑥) ∈ (ℵ‘𝐴) ↔ (𝑓‘𝑥) ∈ ∪
𝑦 ∈ 𝐴 (ℵ‘𝑦))) |
105 | | eliun 4460 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓‘𝑥) ∈ ∪
𝑦 ∈ 𝐴 (ℵ‘𝑦) ↔ ∃𝑦 ∈ 𝐴 (𝑓‘𝑥) ∈ (ℵ‘𝑦)) |
106 | | alephcard 8776 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(card‘(ℵ‘𝑦)) = (ℵ‘𝑦) |
107 | 106 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓‘𝑥) ∈ (card‘(ℵ‘𝑦)) ↔ (𝑓‘𝑥) ∈ (ℵ‘𝑦)) |
108 | | cardsdomelir 8682 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓‘𝑥) ∈ (card‘(ℵ‘𝑦)) → (𝑓‘𝑥) ≺ (ℵ‘𝑦)) |
109 | 107, 108 | sylbir 224 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓‘𝑥) ∈ (ℵ‘𝑦) → (𝑓‘𝑥) ≺ (ℵ‘𝑦)) |
110 | | elharval 8351 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((ℵ‘𝑦)
∈ (har‘(𝑓‘𝑥)) ↔ ((ℵ‘𝑦) ∈ On ∧ (ℵ‘𝑦) ≼ (𝑓‘𝑥))) |
111 | 110 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((ℵ‘𝑦)
∈ (har‘(𝑓‘𝑥)) → (ℵ‘𝑦) ≼ (𝑓‘𝑥)) |
112 | | domnsym 7971 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((ℵ‘𝑦)
≼ (𝑓‘𝑥) → ¬ (𝑓‘𝑥) ≺ (ℵ‘𝑦)) |
113 | 111, 112 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((ℵ‘𝑦)
∈ (har‘(𝑓‘𝑥)) → ¬ (𝑓‘𝑥) ≺ (ℵ‘𝑦)) |
114 | 113 | con2i 133 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓‘𝑥) ≺ (ℵ‘𝑦) → ¬ (ℵ‘𝑦) ∈ (har‘(𝑓‘𝑥))) |
115 | | alephon 8775 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(ℵ‘𝑦)
∈ On |
116 | | ontri1 5674 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((har‘(𝑓‘𝑥)) ∈ On ∧ (ℵ‘𝑦) ∈ On) →
((har‘(𝑓‘𝑥)) ⊆ (ℵ‘𝑦) ↔ ¬
(ℵ‘𝑦) ∈
(har‘(𝑓‘𝑥)))) |
117 | 83, 115, 116 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((har‘(𝑓‘𝑥)) ⊆ (ℵ‘𝑦) ↔ ¬ (ℵ‘𝑦) ∈ (har‘(𝑓‘𝑥))) |
118 | 114, 117 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓‘𝑥) ≺ (ℵ‘𝑦) → (har‘(𝑓‘𝑥)) ⊆ (ℵ‘𝑦)) |
119 | 109, 118 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓‘𝑥) ∈ (ℵ‘𝑦) → (har‘(𝑓‘𝑥)) ⊆ (ℵ‘𝑦)) |
120 | | alephord2i 8783 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∈ On → (𝑦 ∈ 𝐴 → (ℵ‘𝑦) ∈ (ℵ‘𝐴))) |
121 | 120 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) → (ℵ‘𝑦) ∈ (ℵ‘𝐴)) |
122 | | ontr2 5689 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((har‘(𝑓‘𝑥)) ∈ On ∧ (ℵ‘𝐴) ∈ On) →
(((har‘(𝑓‘𝑥)) ⊆ (ℵ‘𝑦) ∧ (ℵ‘𝑦) ∈ (ℵ‘𝐴)) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴))) |
123 | 83, 15, 122 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((har‘(𝑓‘𝑥)) ⊆ (ℵ‘𝑦) ∧ (ℵ‘𝑦) ∈ (ℵ‘𝐴)) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴)) |
124 | 119, 121,
123 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ On ∧ 𝑦 ∈ 𝐴) ∧ (𝑓‘𝑥) ∈ (ℵ‘𝑦)) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴)) |
125 | 124 | exp31 628 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ On → (𝑦 ∈ 𝐴 → ((𝑓‘𝑥) ∈ (ℵ‘𝑦) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴)))) |
126 | 125 | rexlimdv 3012 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ On → (∃𝑦 ∈ 𝐴 (𝑓‘𝑥) ∈ (ℵ‘𝑦) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴))) |
127 | 105, 126 | syl5bi 231 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ On → ((𝑓‘𝑥) ∈ ∪
𝑦 ∈ 𝐴 (ℵ‘𝑦) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴))) |
128 | 41, 127 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ((𝑓‘𝑥) ∈ ∪
𝑦 ∈ 𝐴 (ℵ‘𝑦) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴))) |
129 | 104, 128 | sylbid 229 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ((𝑓‘𝑥) ∈ (ℵ‘𝐴) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴))) |
130 | 102, 129 | sylan9r 688 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) → (𝑥 ∈ (cf‘(ℵ‘𝐴)) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴))) |
131 | 130 | imp 444 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (har‘(𝑓‘𝑥)) ∈ (ℵ‘𝐴)) |
132 | 85 | cbvmptv 4678 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈
(cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓‘𝑦))) = (𝑥 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓‘𝑥))) |
133 | 86, 132 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢ 𝐻 = (𝑥 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓‘𝑥))) |
134 | 131, 133 | fmptd 6292 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) → 𝐻:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) |
135 | | ffvelrn 6265 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝐻‘𝑥) ∈ (ℵ‘𝐴)) |
136 | | onelss 5683 |
. . . . . . . . . . . . . . 15
⊢
((ℵ‘𝐴)
∈ On → ((𝐻‘𝑥) ∈ (ℵ‘𝐴) → (𝐻‘𝑥) ⊆ (ℵ‘𝐴))) |
137 | 15, 135, 136 | mpsyl 66 |
. . . . . . . . . . . . . 14
⊢ ((𝐻:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ 𝑥 ∈ (cf‘(ℵ‘𝐴))) → (𝐻‘𝑥) ⊆ (ℵ‘𝐴)) |
138 | 137 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ (𝐻:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) → ∀𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ⊆ (ℵ‘𝐴)) |
139 | | ss2ixp 7807 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ⊆ (ℵ‘𝐴) → X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ⊆ X𝑥 ∈
(cf‘(ℵ‘𝐴))(ℵ‘𝐴)) |
140 | 93, 10 | ixpconst 7804 |
. . . . . . . . . . . . . 14
⊢ X𝑥 ∈
(cf‘(ℵ‘𝐴))(ℵ‘𝐴) = ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))) |
141 | 139, 140 | syl6sseq 3614 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ⊆ (ℵ‘𝐴) → X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ⊆ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) |
142 | 134, 138,
141 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) → X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ⊆ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) |
143 | | ssdomg 7887 |
. . . . . . . . . . . 12
⊢
(((ℵ‘𝐴)
↑𝑚 (cf‘(ℵ‘𝐴))) ∈ V → (X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ⊆ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))) → X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ≼ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))))) |
144 | 101, 142,
143 | mpsyl 66 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ 𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴)) → X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ≼ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) |
145 | 144 | adantrr 749 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ≼ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) |
146 | | sdomdomtr 7978 |
. . . . . . . . . 10
⊢
(((ℵ‘𝐴)
≺ X𝑥 ∈ (cf‘(ℵ‘𝐴))(𝐻‘𝑥) ∧ X𝑥 ∈
(cf‘(ℵ‘𝐴))(𝐻‘𝑥) ≼ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) |
147 | 100, 145,
146 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ Lim 𝐴) ∧ (𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤))) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) |
148 | 147 | expcom 450 |
. . . . . . . 8
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤)) → ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))))) |
149 | 148 | 3adant2 1073 |
. . . . . . 7
⊢ ((𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤)) → ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))))) |
150 | 149 | exlimiv 1845 |
. . . . . 6
⊢
(∃𝑓(𝑓:(cf‘(ℵ‘𝐴))⟶(ℵ‘𝐴) ∧ Smo 𝑓 ∧ ∀𝑧 ∈ (ℵ‘𝐴)∃𝑤 ∈ (cf‘(ℵ‘𝐴))𝑧 ⊆ (𝑓‘𝑤)) → ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))))) |
151 | 15, 40, 150 | mp2b 10 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) |
152 | 151 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ On → ((𝐴 ∈ V ∧ Lim 𝐴) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))))) |
153 | 33, 39, 152 | 3jaod 1384 |
. . 3
⊢ (𝐴 ∈ On → ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 ∈ V ∧ Lim 𝐴)) → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))))) |
154 | 2, 153 | mpd 15 |
. 2
⊢ (𝐴 ∈ On →
(ℵ‘𝐴) ≺
((ℵ‘𝐴)
↑𝑚 (cf‘(ℵ‘𝐴)))) |
155 | | alephfnon 8771 |
. . . . 5
⊢ ℵ
Fn On |
156 | | fndm 5904 |
. . . . 5
⊢ (ℵ
Fn On → dom ℵ = On) |
157 | 155, 156 | ax-mp 5 |
. . . 4
⊢ dom
ℵ = On |
158 | 157 | eleq2i 2680 |
. . 3
⊢ (𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On) |
159 | | ndmfv 6128 |
. . . 4
⊢ (¬
𝐴 ∈ dom ℵ →
(ℵ‘𝐴) =
∅) |
160 | | 1n0 7462 |
. . . . . 6
⊢
1𝑜 ≠ ∅ |
161 | | 1on 7454 |
. . . . . . . 8
⊢
1𝑜 ∈ On |
162 | 161 | elexi 3186 |
. . . . . . 7
⊢
1𝑜 ∈ V |
163 | 162 | 0sdom 7976 |
. . . . . 6
⊢ (∅
≺ 1𝑜 ↔ 1𝑜 ≠
∅) |
164 | 160, 163 | mpbir 220 |
. . . . 5
⊢ ∅
≺ 1𝑜 |
165 | | id 22 |
. . . . . 6
⊢
((ℵ‘𝐴) =
∅ → (ℵ‘𝐴) = ∅) |
166 | | fveq2 6103 |
. . . . . . . . 9
⊢
((ℵ‘𝐴) =
∅ → (cf‘(ℵ‘𝐴)) = (cf‘∅)) |
167 | | cf0 8956 |
. . . . . . . . 9
⊢
(cf‘∅) = ∅ |
168 | 166, 167 | syl6eq 2660 |
. . . . . . . 8
⊢
((ℵ‘𝐴) =
∅ → (cf‘(ℵ‘𝐴)) = ∅) |
169 | 165, 168 | oveq12d 6567 |
. . . . . . 7
⊢
((ℵ‘𝐴) =
∅ → ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))) = (∅ ↑𝑚
∅)) |
170 | | 0ex 4718 |
. . . . . . . 8
⊢ ∅
∈ V |
171 | | map0e 7781 |
. . . . . . . 8
⊢ (∅
∈ V → (∅ ↑𝑚 ∅) =
1𝑜) |
172 | 170, 171 | ax-mp 5 |
. . . . . . 7
⊢ (∅
↑𝑚 ∅) = 1𝑜 |
173 | 169, 172 | syl6eq 2660 |
. . . . . 6
⊢
((ℵ‘𝐴) =
∅ → ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))) =
1𝑜) |
174 | 165, 173 | breq12d 4596 |
. . . . 5
⊢
((ℵ‘𝐴) =
∅ → ((ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴))) ↔ ∅ ≺
1𝑜)) |
175 | 164, 174 | mpbiri 247 |
. . . 4
⊢
((ℵ‘𝐴) =
∅ → (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑𝑚
(cf‘(ℵ‘𝐴)))) |
176 | 159, 175 | syl 17 |
. . 3
⊢ (¬
𝐴 ∈ dom ℵ →
(ℵ‘𝐴) ≺
((ℵ‘𝐴)
↑𝑚 (cf‘(ℵ‘𝐴)))) |
177 | 158, 176 | sylnbir 320 |
. 2
⊢ (¬
𝐴 ∈ On →
(ℵ‘𝐴) ≺
((ℵ‘𝐴)
↑𝑚 (cf‘(ℵ‘𝐴)))) |
178 | 154, 177 | pm2.61i 175 |
1
⊢
(ℵ‘𝐴)
≺ ((ℵ‘𝐴)
↑𝑚 (cf‘(ℵ‘𝐴))) |