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 ~~ _om

Proof

Step	Hyp	Ref	Expression
1		dfhf2	|- HF = ( R1 ` _om )
2		omina	|- _om e. Inacc
3		inar1	|- ( _om e. Inacc -> ( R1 ` _om ) ~~ _om )
4	2 3	ax-mp	|- ( R1 ` _om ) ~~ _om
5	1 4	eqbrtri	|- HF ~~ _om