Metamath Proof Explorer


Theorem smo0

Description: The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011)

Ref Expression
Assertion smo0
|- Smo (/)

Proof

Step Hyp Ref Expression
1 ord0
 |-  Ord (/)
2 1 iordsmo
 |-  Smo ( _I |` (/) )
3 res0
 |-  ( _I |` (/) ) = (/)
4 smoeq
 |-  ( ( _I |` (/) ) = (/) -> ( Smo ( _I |` (/) ) <-> Smo (/) ) )
5 3 4 ax-mp
 |-  ( Smo ( _I |` (/) ) <-> Smo (/) )
6 2 5 mpbi
 |-  Smo (/)