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 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ ( ℵ ‘ 𝐵 ) ↔ 𝐴 ≺ ( ℵ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ∈ On )
2 alephon ( ℵ ‘ 𝐵 ) ∈ On
3 onenon ( ( ℵ ‘ 𝐵 ) ∈ On → ( ℵ ‘ 𝐵 ) ∈ dom card )
4 2 3 ax-mp ( ℵ ‘ 𝐵 ) ∈ dom card
5 cardsdomel ( ( 𝐴 ∈ On ∧ ( ℵ ‘ 𝐵 ) ∈ dom card ) → ( 𝐴 ≺ ( ℵ ‘ 𝐵 ) ↔ 𝐴 ∈ ( card ‘ ( ℵ ‘ 𝐵 ) ) ) )
6 1 4 5 sylancl ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ≺ ( ℵ ‘ 𝐵 ) ↔ 𝐴 ∈ ( card ‘ ( ℵ ‘ 𝐵 ) ) ) )
7 alephcard ( card ‘ ( ℵ ‘ 𝐵 ) ) = ( ℵ ‘ 𝐵 )
8 7 eleq2i ( 𝐴 ∈ ( card ‘ ( ℵ ‘ 𝐵 ) ) ↔ 𝐴 ∈ ( ℵ ‘ 𝐵 ) )
9 6 8 bitr2di ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ ( ℵ ‘ 𝐵 ) ↔ 𝐴 ≺ ( ℵ ‘ 𝐵 ) ) )