Theorem harndom

Description: The Hartogs number of a set does not inject into that set. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	harndom	$$⊢\neg \mathrm{har}\left(X\right)\preccurlyeq X$$

Proof

Step	Hyp	Ref	Expression
1		harcl	$$⊢\mathrm{har}\left(X\right)\in \mathrm{On}$$
2	1	onirri	$$⊢\neg \mathrm{har}\left(X\right)\in \mathrm{har}\left(X\right)$$
3		elharval	$$⊢\mathrm{har}\left(X\right)\in \mathrm{har}\left(X\right)\leftrightarrow \left(\mathrm{har}\left(X\right)\in \mathrm{On}\wedge \mathrm{har}\left(X\right)\preccurlyeq X\right)$$
4	1 3	mpbiran	$$⊢\mathrm{har}\left(X\right)\in \mathrm{har}\left(X\right)\leftrightarrow \mathrm{har}\left(X\right)\preccurlyeq X$$
5	2 4	mtbi	$$⊢\neg \mathrm{har}\left(X\right)\preccurlyeq X$$