Theorem omhf

Description: Finite ordinals are hereditarily finite sets. (Contributed by Eric Schmidt, 26-Sep-2026)

	Ref	Expression
Assertion	omhf	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ HF )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ HF ↔ ∅ ∈ HF ) )
2		eleq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ HF ↔ 𝑦 ∈ HF ) )
3		eleq1	⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 ∈ HF ↔ suc 𝑦 ∈ HF ) )
4		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ HF ↔ 𝐴 ∈ HF ) )
5		0hf	⊢ ∅ ∈ HF
6		df-suc	⊢ suc 𝑦 = ( 𝑦 ∪ { 𝑦 } )
7		hfadj	⊢ ( ( 𝑦 ∈ HF ∧ 𝑦 ∈ HF ) → ( 𝑦 ∪ { 𝑦 } ) ∈ HF )
8	7	anidms	⊢ ( 𝑦 ∈ HF → ( 𝑦 ∪ { 𝑦 } ) ∈ HF )
9	6 8	eqeltrid	⊢ ( 𝑦 ∈ HF → suc 𝑦 ∈ HF )
10	9	a1i	⊢ ( 𝑦 ∈ ω → ( 𝑦 ∈ HF → suc 𝑦 ∈ HF ) )
11	1 2 3 4 5 10	finds	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ HF )