This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∅