Metamath Proof Explorer

Theorem alephsdom

Description: If an ordinal is smaller than an initial ordinal, it is strictly dominated by it. (Contributed by Jeff Hankins, 24-Oct-2009) (Proof shortened by Mario Carneiro, 20-Sep-2014)

Ref Expression
Assertion alephsdom ⊢ A ∈ On ∧ B ∈ On → A ∈ ℵ ⁡ B ↔ A ≺ ℵ ⁡ B

Proof

Step Hyp Ref Expression
1 simpl ⊢ A ∈ On ∧ B ∈ On → A ∈ On
2 alephon ⊢ ℵ ⁡ B ∈ On
3 onenon ⊢ ℵ ⁡ B ∈ On → ℵ ⁡ B ∈ dom ⁡ card
4 2 3 ax-mp ⊢ ℵ ⁡ B ∈ dom ⁡ card
5 cardsdomel ⊢ A ∈ On ∧ ℵ ⁡ B ∈ dom ⁡ card → A ≺ ℵ ⁡ B ↔ A ∈ card ⁡ ℵ ⁡ B
6 1 4 5 sylancl ⊢ A ∈ On ∧ B ∈ On → A ≺ ℵ ⁡ B ↔ A ∈ card ⁡ ℵ ⁡ B
7 alephcard ⊢ card ⁡ ℵ ⁡ B = ℵ ⁡ B
8 7 eleq2i ⊢ A ∈ card ⁡ ℵ ⁡ B ↔ A ∈ ℵ ⁡ B
9 6 8 bitr2di ⊢ A ∈ On ∧ B ∈ On → A ∈ ℵ ⁡ B ↔ A ≺ ℵ ⁡ B