Theorem alephordilem1

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

	Ref	Expression
Assertion	alephordilem1	⊢ ( 𝐴 ∈ On → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝐴 ) )

Proof

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