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 ‘ ω ) ≈ ω |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | omina | ⊢ ω ∈ Inacc | |
2 | inar1 | ⊢ ( ω ∈ Inacc → ( 𝑅1 ‘ ω ) ≈ ω ) | |
3 | 1 2 | ax-mp | ⊢ ( 𝑅1 ‘ ω ) ≈ ω |