Theorem harsdom

Description: The Hartogs number of a well-orderable set strictly dominates the set. (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	harsdom	$$⊢A\in \mathrm{dom}\mathrm{card}\to A\prec \mathrm{har}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		harndom	$$⊢\neg \mathrm{har}\left(A\right)\preccurlyeq A$$
2		harcl	$$⊢\mathrm{har}\left(A\right)\in \mathrm{On}$$
3		onenon	$$⊢\mathrm{har}\left(A\right)\in \mathrm{On}\to \mathrm{har}\left(A\right)\in \mathrm{dom}\mathrm{card}$$
4	2 3	ax-mp	$$⊢\mathrm{har}\left(A\right)\in \mathrm{dom}\mathrm{card}$$
5		domtri2	$$⊢\left(\mathrm{har}\left(A\right)\in \mathrm{dom}\mathrm{card}\wedge A\in \mathrm{dom}\mathrm{card}\right)\to \left(\mathrm{har}\left(A\right)\preccurlyeq A\leftrightarrow \neg A\prec \mathrm{har}\left(A\right)\right)$$
6	5	con2bid	$$⊢\left(\mathrm{har}\left(A\right)\in \mathrm{dom}\mathrm{card}\wedge A\in \mathrm{dom}\mathrm{card}\right)\to \left(A\prec \mathrm{har}\left(A\right)\leftrightarrow \neg \mathrm{har}\left(A\right)\preccurlyeq A\right)$$
7	4 6	mpan	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(A\prec \mathrm{har}\left(A\right)\leftrightarrow \neg \mathrm{har}\left(A\right)\preccurlyeq A\right)$$
8	1 7	mpbiri	$$⊢A\in \mathrm{dom}\mathrm{card}\to A\prec \mathrm{har}\left(A\right)$$