Metamath Proof Explorer

Theorem onenon

Description: Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion onenon 
|- ( A e. On -> A e. dom card )

Proof

Step Hyp Ref Expression
1 enrefg 
 |-  ( A e. On -> A ~~ A )
2 isnumi 
 |-  ( ( A e. On /\ A ~~ A ) -> A e. dom card )
3 1 2 mpdan 
 |-  ( A e. On -> A e. dom card )