Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-smo Structured version   Unicode version

Definition df-smo 7073
 Description: Definition of a strictly monotone ordinal function. Definition 7.46 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 15-Nov-2011.)
Assertion
Ref Expression
df-smo
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-smo
StepHypRef Expression
1 cA . . 3
21wsmo 7072 . 2
31cdm 4854 . . . 4
4 con0 5442 . . . 4
53, 4, 1wf 5597 . . 3
63word 5441 . . 3
7 vx . . . . . . 7
8 vy . . . . . . 7
97, 8wel 1871 . . . . . 6
107cv 1436 . . . . . . . 8
1110, 1cfv 5601 . . . . . . 7
128cv 1436 . . . . . . . 8
1312, 1cfv 5601 . . . . . . 7
1411, 13wcel 1870 . . . . . 6
159, 14wi 4 . . . . 5
1615, 8, 3wral 2782 . . . 4
1716, 7, 3wral 2782 . . 3
185, 6, 17w3a 982 . 2
192, 18wb 187 1
 Colors of variables: wff setvar class This definition is referenced by:  dfsmo2  7074  issmo  7075  smoeq  7077  smodm  7078  smores  7079  smofvon  7086  smoel  7087  smoiso  7089
 Copyright terms: Public domain W3C validator