Theorem smodm 7041

Description: The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011.)

Assertion

Ref	Expression
smodm

Proof of Theorem smodm

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-smo 7036	. 2
2	1	simp2bi 1012	1

Syntax hints:  ->wi 4  e.wcel 1818  A.wral 2807  Ordword 4882  con0 4883  domcdm 5004  -->wf 5589  `cfv 5593  Smowsmo 7035

This theorem is referenced by:  smores2  7044  smodm2  7045  smoel  7050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-smo 7036