Description: The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | smo0 | |- Smo (/) |
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 (/) |