Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Infinity
Cardinal numbers
alephfplem2
Next ⟩
alephfplem3
Metamath Proof Explorer
Ascii
Unicode
Theorem
alephfplem2
Description:
Lemma for
alephfp
.
(Contributed by
NM
, 6-Nov-2004)
Ref
Expression
Hypothesis
alephfplem.1
⊢
H
=
rec
⁡
ℵ
ω
↾
ω
Assertion
alephfplem2
⊢
w
∈
ω
→
H
⁡
suc
⁡
w
=
ℵ
⁡
H
⁡
w
Proof
Step
Hyp
Ref
Expression
1
alephfplem.1
⊢
H
=
rec
⁡
ℵ
ω
↾
ω
2
frsuc
⊢
w
∈
ω
→
rec
⁡
ℵ
ω
↾
ω
⁡
suc
⁡
w
=
ℵ
⁡
rec
⁡
ℵ
ω
↾
ω
⁡
w
3
1
fveq1i
⊢
H
⁡
suc
⁡
w
=
rec
⁡
ℵ
ω
↾
ω
⁡
suc
⁡
w
4
1
fveq1i
⊢
H
⁡
w
=
rec
⁡
ℵ
ω
↾
ω
⁡
w
5
4
fveq2i
⊢
ℵ
⁡
H
⁡
w
=
ℵ
⁡
rec
⁡
ℵ
ω
↾
ω
⁡
w
6
2
3
5
3eqtr4g
⊢
w
∈
ω
→
H
⁡
suc
⁡
w
=
ℵ
⁡
H
⁡
w