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	⊢ ( 𝐴 ∈ dom card → 𝐴 ≺ ( har ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		harndom	⊢ ¬ ( har ‘ 𝐴 ) ≼ 𝐴
2		harcl	⊢ ( har ‘ 𝐴 ) ∈ On
3		onenon	⊢ ( ( har ‘ 𝐴 ) ∈ On → ( har ‘ 𝐴 ) ∈ dom card )
4	2 3	ax-mp	⊢ ( har ‘ 𝐴 ) ∈ dom card
5		domtri2	⊢ ( ( ( har ‘ 𝐴 ) ∈ dom card ∧ 𝐴 ∈ dom card ) → ( ( har ‘ 𝐴 ) ≼ 𝐴 ↔ ¬ 𝐴 ≺ ( har ‘ 𝐴 ) ) )
6	5	con2bid	⊢ ( ( ( har ‘ 𝐴 ) ∈ dom card ∧ 𝐴 ∈ dom card ) → ( 𝐴 ≺ ( har ‘ 𝐴 ) ↔ ¬ ( har ‘ 𝐴 ) ≼ 𝐴 ) )
7	4 6	mpan	⊢ ( 𝐴 ∈ dom card → ( 𝐴 ≺ ( har ‘ 𝐴 ) ↔ ¬ ( har ‘ 𝐴 ) ≼ 𝐴 ) )
8	1 7	mpbiri	⊢ ( 𝐴 ∈ dom card → 𝐴 ≺ ( har ‘ 𝐴 ) )