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 e. dom card -> A ~< ( har ` A ) )

Proof

Step	Hyp	Ref	Expression
1		harndom	|- -. ( har ` A ) ~<_ A
2		harcl	|- ( har ` A ) e. On
3		onenon	|- ( ( har ` A ) e. On -> ( har ` A ) e. dom card )
4	2 3	ax-mp	|- ( har ` A ) e. dom card
5		domtri2	|- ( ( ( har ` A ) e. dom card /\ A e. dom card ) -> ( ( har ` A ) ~<_ A <-> -. A ~< ( har ` A ) ) )
6	5	con2bid	|- ( ( ( har ` A ) e. dom card /\ A e. dom card ) -> ( A ~< ( har ` A ) <-> -. ( har ` A ) ~<_ A ) )
7	4 6	mpan	|- ( A e. dom card -> ( A ~< ( har ` A ) <-> -. ( har ` A ) ~<_ A ) )
8	1 7	mpbiri	|- ( A e. dom card -> A ~< ( har ` A ) )