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