This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem alephordilem1

Description: Lemma for alephordi . (Contributed by NM, 23-Oct-2009) (Revised by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion alephordilem1 ⊢ A ∈ On → ℵ ⁡ A ≺ ℵ ⁡ suc ⁡ A

Proof

Step Hyp Ref Expression
1 alephon ⊢ ℵ ⁡ A ∈ On
2 onenon ⊢ ℵ ⁡ A ∈ On → ℵ ⁡ A ∈ dom ⁡ card
3 harsdom ⊢ ℵ ⁡ A ∈ dom ⁡ card → ℵ ⁡ A ≺ har ⁡ ℵ ⁡ A
4 1 2 3 mp2b ⊢ ℵ ⁡ A ≺ har ⁡ ℵ ⁡ A
5 alephsuc ⊢ A ∈ On → ℵ ⁡ suc ⁡ A = har ⁡ ℵ ⁡ A
6 4 5 breqtrrid ⊢ A ∈ On → ℵ ⁡ A ≺ ℵ ⁡ suc ⁡ A