This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: Value of the ordinal injection function. (Contributed by Stefan O'Rear, 18-Jan-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dnnumch.f | ||
| dnnumch.a | |||
| dnnumch.g | |||
| Assertion | dnnumch3lem |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dnnumch.f | ||
| 2 | dnnumch.a | ||
| 3 | dnnumch.g | ||
| 4 | eqid | ||
| 5 | sneq | ||
| 6 | 5 | imaeq2d | |
| 7 | 6 | inteqd | |
| 8 | simpr | ||
| 9 | cnvimass | ||
| 10 | 1 | tfr1 | |
| 11 | 10 | fndmi | |
| 12 | 9 11 | sseqtri | |
| 13 | 1 2 3 | dnnumch2 | |
| 14 | 13 | sselda | |
| 15 | inisegn0 | ||
| 16 | 14 15 | sylib | |
| 17 | oninton | ||
| 18 | 12 16 17 | sylancr | |
| 19 | 4 7 8 18 | fvmptd3 |