Step |
Hyp |
Ref |
Expression |
1 |
|
alephfplem.1 |
⊢ 𝐻 = ( rec ( ℵ , ω ) ↾ ω ) |
2 |
|
fveq2 |
⊢ ( 𝑣 = ∅ → ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ ∅ ) ) |
3 |
2
|
eleq1d |
⊢ ( 𝑣 = ∅ → ( ( 𝐻 ‘ 𝑣 ) ∈ ran ℵ ↔ ( 𝐻 ‘ ∅ ) ∈ ran ℵ ) ) |
4 |
|
fveq2 |
⊢ ( 𝑣 = 𝑤 → ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) ) |
5 |
4
|
eleq1d |
⊢ ( 𝑣 = 𝑤 → ( ( 𝐻 ‘ 𝑣 ) ∈ ran ℵ ↔ ( 𝐻 ‘ 𝑤 ) ∈ ran ℵ ) ) |
6 |
|
fveq2 |
⊢ ( 𝑣 = suc 𝑤 → ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ suc 𝑤 ) ) |
7 |
6
|
eleq1d |
⊢ ( 𝑣 = suc 𝑤 → ( ( 𝐻 ‘ 𝑣 ) ∈ ran ℵ ↔ ( 𝐻 ‘ suc 𝑤 ) ∈ ran ℵ ) ) |
8 |
1
|
alephfplem1 |
⊢ ( 𝐻 ‘ ∅ ) ∈ ran ℵ |
9 |
|
alephfnon |
⊢ ℵ Fn On |
10 |
|
alephsson |
⊢ ran ℵ ⊆ On |
11 |
10
|
sseli |
⊢ ( ( 𝐻 ‘ 𝑤 ) ∈ ran ℵ → ( 𝐻 ‘ 𝑤 ) ∈ On ) |
12 |
|
fnfvelrn |
⊢ ( ( ℵ Fn On ∧ ( 𝐻 ‘ 𝑤 ) ∈ On ) → ( ℵ ‘ ( 𝐻 ‘ 𝑤 ) ) ∈ ran ℵ ) |
13 |
9 11 12
|
sylancr |
⊢ ( ( 𝐻 ‘ 𝑤 ) ∈ ran ℵ → ( ℵ ‘ ( 𝐻 ‘ 𝑤 ) ) ∈ ran ℵ ) |
14 |
1
|
alephfplem2 |
⊢ ( 𝑤 ∈ ω → ( 𝐻 ‘ suc 𝑤 ) = ( ℵ ‘ ( 𝐻 ‘ 𝑤 ) ) ) |
15 |
14
|
eleq1d |
⊢ ( 𝑤 ∈ ω → ( ( 𝐻 ‘ suc 𝑤 ) ∈ ran ℵ ↔ ( ℵ ‘ ( 𝐻 ‘ 𝑤 ) ) ∈ ran ℵ ) ) |
16 |
13 15
|
syl5ibr |
⊢ ( 𝑤 ∈ ω → ( ( 𝐻 ‘ 𝑤 ) ∈ ran ℵ → ( 𝐻 ‘ suc 𝑤 ) ∈ ran ℵ ) ) |
17 |
3 5 7 8 16
|
finds1 |
⊢ ( 𝑣 ∈ ω → ( 𝐻 ‘ 𝑣 ) ∈ ran ℵ ) |