Theorem harn0

Description: The Hartogs number of a set is never zero.MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015)

	Ref	Expression
Assertion	harn0	⊢ ( 𝑆 ∈ 𝑉 → ( har ‘ 𝑆 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		0elon	⊢ ∅ ∈ On
2	1	a1i	⊢ ( 𝑆 ∈ 𝑉 → ∅ ∈ On )
3		0domg	⊢ ( 𝑆 ∈ 𝑉 → ∅ ≼ 𝑆 )
4		elharval	⊢ ( ∅ ∈ ( har ‘ 𝑆 ) ↔ ( ∅ ∈ On ∧ ∅ ≼ 𝑆 ) )
5	2 3 4	sylanbrc	⊢ ( 𝑆 ∈ 𝑉 → ∅ ∈ ( har ‘ 𝑆 ) )
6	5	ne0d	⊢ ( 𝑆 ∈ 𝑉 → ( har ‘ 𝑆 ) ≠ ∅ )