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
|- ( R1 ` _om ) ~~ _om

Proof

Step Hyp Ref Expression
1 omina
 |-  _om e. Inacc
2 inar1
 |-  ( _om e. Inacc -> ( R1 ` _om ) ~~ _om )
3 1 2 ax-mp
 |-  ( R1 ` _om ) ~~ _om