Metamath Proof Explorer


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 ( 𝑅1 ‘ ω ) ≈ ω

Proof

Step Hyp Ref Expression
1 omina ω ∈ Inacc
2 inar1 ( ω ∈ Inacc → ( 𝑅1 ‘ ω ) ≈ ω )
3 1 2 ax-mp ( 𝑅1 ‘ ω ) ≈ ω