Theorem alephordilem1

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

	Ref	Expression
Assertion	alephordilem1	$$⊢A\in \mathrm{On}\to \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		alephon	$$⊢\aleph \left(A\right)\in \mathrm{On}$$
2		onenon	$$⊢\aleph \left(A\right)\in \mathrm{On}\to \aleph \left(A\right)\in \mathrm{dom}\mathrm{card}$$
3		harsdom	$$⊢\aleph \left(A\right)\in \mathrm{dom}\mathrm{card}\to \aleph \left(A\right)\prec \mathrm{har}\left(\aleph \left(A\right)\right)$$
4	1 2 3	mp2b	$$⊢\aleph \left(A\right)\prec \mathrm{har}\left(\aleph \left(A\right)\right)$$
5		alephsuc	$$⊢A\in \mathrm{On}\to \aleph \left(\mathrm{suc}A\right)=\mathrm{har}\left(\aleph \left(A\right)\right)$$
6	4 5	breqtrrid	$$⊢A\in \mathrm{On}\to \aleph \left(A\right)\prec \aleph \left(\mathrm{suc}A\right)$$