| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ssv |
⊢ ran ℵ ⊆ V |
| 2 |
|
sseq2 |
⊢ ( GCH = V → ( ran ℵ ⊆ GCH ↔ ran ℵ ⊆ V ) ) |
| 3 |
1 2
|
mpbiri |
⊢ ( GCH = V → ran ℵ ⊆ GCH ) |
| 4 |
|
cardidm |
⊢ ( card ‘ ( card ‘ 𝑥 ) ) = ( card ‘ 𝑥 ) |
| 5 |
|
iscard3 |
⊢ ( ( card ‘ ( card ‘ 𝑥 ) ) = ( card ‘ 𝑥 ) ↔ ( card ‘ 𝑥 ) ∈ ( ω ∪ ran ℵ ) ) |
| 6 |
4 5
|
mpbi |
⊢ ( card ‘ 𝑥 ) ∈ ( ω ∪ ran ℵ ) |
| 7 |
|
elun |
⊢ ( ( card ‘ 𝑥 ) ∈ ( ω ∪ ran ℵ ) ↔ ( ( card ‘ 𝑥 ) ∈ ω ∨ ( card ‘ 𝑥 ) ∈ ran ℵ ) ) |
| 8 |
6 7
|
mpbi |
⊢ ( ( card ‘ 𝑥 ) ∈ ω ∨ ( card ‘ 𝑥 ) ∈ ran ℵ ) |
| 9 |
|
fingch |
⊢ Fin ⊆ GCH |
| 10 |
|
nnfi |
⊢ ( ( card ‘ 𝑥 ) ∈ ω → ( card ‘ 𝑥 ) ∈ Fin ) |
| 11 |
9 10
|
sselid |
⊢ ( ( card ‘ 𝑥 ) ∈ ω → ( card ‘ 𝑥 ) ∈ GCH ) |
| 12 |
11
|
a1i |
⊢ ( ran ℵ ⊆ GCH → ( ( card ‘ 𝑥 ) ∈ ω → ( card ‘ 𝑥 ) ∈ GCH ) ) |
| 13 |
|
ssel |
⊢ ( ran ℵ ⊆ GCH → ( ( card ‘ 𝑥 ) ∈ ran ℵ → ( card ‘ 𝑥 ) ∈ GCH ) ) |
| 14 |
12 13
|
jaod |
⊢ ( ran ℵ ⊆ GCH → ( ( ( card ‘ 𝑥 ) ∈ ω ∨ ( card ‘ 𝑥 ) ∈ ran ℵ ) → ( card ‘ 𝑥 ) ∈ GCH ) ) |
| 15 |
8 14
|
mpi |
⊢ ( ran ℵ ⊆ GCH → ( card ‘ 𝑥 ) ∈ GCH ) |
| 16 |
|
vex |
⊢ 𝑥 ∈ V |
| 17 |
|
alephon |
⊢ ( ℵ ‘ suc 𝑥 ) ∈ On |
| 18 |
|
simpr |
⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → 𝑥 ∈ On ) |
| 19 |
|
simpl |
⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → ran ℵ ⊆ GCH ) |
| 20 |
|
alephfnon |
⊢ ℵ Fn On |
| 21 |
|
fnfvelrn |
⊢ ( ( ℵ Fn On ∧ 𝑥 ∈ On ) → ( ℵ ‘ 𝑥 ) ∈ ran ℵ ) |
| 22 |
20 18 21
|
sylancr |
⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → ( ℵ ‘ 𝑥 ) ∈ ran ℵ ) |
| 23 |
19 22
|
sseldd |
⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → ( ℵ ‘ 𝑥 ) ∈ GCH ) |
| 24 |
|
suceloni |
⊢ ( 𝑥 ∈ On → suc 𝑥 ∈ On ) |
| 25 |
24
|
adantl |
⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → suc 𝑥 ∈ On ) |
| 26 |
|
fnfvelrn |
⊢ ( ( ℵ Fn On ∧ suc 𝑥 ∈ On ) → ( ℵ ‘ suc 𝑥 ) ∈ ran ℵ ) |
| 27 |
20 25 26
|
sylancr |
⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → ( ℵ ‘ suc 𝑥 ) ∈ ran ℵ ) |
| 28 |
19 27
|
sseldd |
⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → ( ℵ ‘ suc 𝑥 ) ∈ GCH ) |
| 29 |
|
gchaleph2 |
⊢ ( ( 𝑥 ∈ On ∧ ( ℵ ‘ 𝑥 ) ∈ GCH ∧ ( ℵ ‘ suc 𝑥 ) ∈ GCH ) → ( ℵ ‘ suc 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) ) |
| 30 |
18 23 28 29
|
syl3anc |
⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → ( ℵ ‘ suc 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) ) |
| 31 |
|
isnumi |
⊢ ( ( ( ℵ ‘ suc 𝑥 ) ∈ On ∧ ( ℵ ‘ suc 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) ) → 𝒫 ( ℵ ‘ 𝑥 ) ∈ dom card ) |
| 32 |
17 30 31
|
sylancr |
⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → 𝒫 ( ℵ ‘ 𝑥 ) ∈ dom card ) |
| 33 |
32
|
ralrimiva |
⊢ ( ran ℵ ⊆ GCH → ∀ 𝑥 ∈ On 𝒫 ( ℵ ‘ 𝑥 ) ∈ dom card ) |
| 34 |
|
dfac12 |
⊢ ( CHOICE ↔ ∀ 𝑥 ∈ On 𝒫 ( ℵ ‘ 𝑥 ) ∈ dom card ) |
| 35 |
33 34
|
sylibr |
⊢ ( ran ℵ ⊆ GCH → CHOICE ) |
| 36 |
|
dfac10 |
⊢ ( CHOICE ↔ dom card = V ) |
| 37 |
35 36
|
sylib |
⊢ ( ran ℵ ⊆ GCH → dom card = V ) |
| 38 |
16 37
|
eleqtrrid |
⊢ ( ran ℵ ⊆ GCH → 𝑥 ∈ dom card ) |
| 39 |
|
cardid2 |
⊢ ( 𝑥 ∈ dom card → ( card ‘ 𝑥 ) ≈ 𝑥 ) |
| 40 |
|
engch |
⊢ ( ( card ‘ 𝑥 ) ≈ 𝑥 → ( ( card ‘ 𝑥 ) ∈ GCH ↔ 𝑥 ∈ GCH ) ) |
| 41 |
38 39 40
|
3syl |
⊢ ( ran ℵ ⊆ GCH → ( ( card ‘ 𝑥 ) ∈ GCH ↔ 𝑥 ∈ GCH ) ) |
| 42 |
15 41
|
mpbid |
⊢ ( ran ℵ ⊆ GCH → 𝑥 ∈ GCH ) |
| 43 |
16
|
a1i |
⊢ ( ran ℵ ⊆ GCH → 𝑥 ∈ V ) |
| 44 |
42 43
|
2thd |
⊢ ( ran ℵ ⊆ GCH → ( 𝑥 ∈ GCH ↔ 𝑥 ∈ V ) ) |
| 45 |
44
|
eqrdv |
⊢ ( ran ℵ ⊆ GCH → GCH = V ) |
| 46 |
3 45
|
impbii |
⊢ ( GCH = V ↔ ran ℵ ⊆ GCH ) |