Theorem r1omALT

Description: Alternate proof of r1om , shorter as a consequence of inar1 , but requiring AC. (Contributed by Mario Carneiro, 27-May-2013) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	r1omALT	$$⊢R_1\left(\mathrm{\omega }\right)\approx \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		omina	$$⊢\mathrm{\omega }\in \mathrm{Inacc}$$
2		inar1	$$⊢\mathrm{\omega }\in \mathrm{Inacc}\to R_1\left(\mathrm{\omega }\right)\approx \mathrm{\omega }$$
3	1 2	ax-mp	$$⊢R_1\left(\mathrm{\omega }\right)\approx \mathrm{\omega }$$