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	⊢ ¬ ( har ‘ 𝑋 ) ≼ 𝑋

Proof

Step	Hyp	Ref	Expression
1		harcl	⊢ ( har ‘ 𝑋 ) ∈ On
2	1	onirri	⊢ ¬ ( har ‘ 𝑋 ) ∈ ( har ‘ 𝑋 )
3		elharval	⊢ ( ( har ‘ 𝑋 ) ∈ ( har ‘ 𝑋 ) ↔ ( ( har ‘ 𝑋 ) ∈ On ∧ ( har ‘ 𝑋 ) ≼ 𝑋 ) )
4	1 3	mpbiran	⊢ ( ( har ‘ 𝑋 ) ∈ ( har ‘ 𝑋 ) ↔ ( har ‘ 𝑋 ) ≼ 𝑋 )
5	2 4	mtbi	⊢ ¬ ( har ‘ 𝑋 ) ≼ 𝑋