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 SmoI
3 res0 I=
4 smoeq I=SmoISmo
5 3 4 ax-mp SmoISmo
6 2 5 mpbi Smo