Metamath Proof Explorer

Theorem har2o

Description: The least cardinal greater than 2 is 3. (Contributed by RP, 5-Nov-2023)

Ref Expression
Assertion har2o 
|- ( har ` 2o ) = 3o

Proof

Step Hyp Ref Expression
1 2onn 
 |-  2o e. _om
2 harsucnn 
 |-  ( 2o e. _om -> ( har ` 2o ) = suc 2o )
3 1 2 ax-mp 
 |-  ( har ` 2o ) = suc 2o
4 df-3o 
 |-  3o = suc 2o
5 3 4 eqtr4i 
 |-  ( har ` 2o ) = 3o