Theorem hfomALT

Description: Alternate proof of hfom , shorter as a consequence of inar1 , but requiring AC. (Contributed by Mario Carneiro, 27-May-2013) Restate using the defined HF symbol. (Revised by Eric Schmidt, 24-Sep-2026) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	hfomALT	⊢ HF ≈ ω

Proof

Step	Hyp	Ref	Expression
1		dfhf2	⊢ HF = ( 𝑅1 ‘ ω )
2		omina	⊢ ω ∈ Inacc
3		inar1	⊢ ( ω ∈ Inacc → ( 𝑅1 ‘ ω ) ≈ ω )
4	2 3	ax-mp	⊢ ( 𝑅1 ‘ ω ) ≈ ω
5	1 4	eqbrtri	⊢ HF ≈ ω