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 (/)