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 ∅