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	Could not format assertion : No typesetting found for |- HF ~~ _om with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dfhf2	Could not format HF = ( R1 ` _om ) : No typesetting found for |- HF = ( R1 ` _om ) with typecode |-
2		omina	$$⊢\mathrm{\omega }\in \mathrm{Inacc}$$
3		inar1	$$⊢\mathrm{\omega }\in \mathrm{Inacc}\to R_1\left(\mathrm{\omega }\right)\approx \mathrm{\omega }$$
4	2 3	ax-mp	$$⊢R_1\left(\mathrm{\omega }\right)\approx \mathrm{\omega }$$
5	1 4	eqbrtri	Could not format HF ~~ _om : No typesetting found for |- HF ~~ _om with typecode |-