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

Definition df-smo 6249
 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 6248 . 2
31cdm 4580 . . . 4
4 con0 4285 . . . 4
53, 4, 1wf 4588 . . 3
63word 4284 . . 3
7 vx . . . . . . 7
8 vy . . . . . . 7
97, 8wel 1622 . . . . . 6
107cv 1618 . . . . . . . 8
1110, 1cfv 4592 . . . . . . 7
128cv 1618 . . . . . . . 8
1312, 1cfv 4592 . . . . . . 7
1411, 13wcel 1621 . . . . . 6
159, 14wi 6 . . . . 5
1615, 8, 3wral 2509 . . . 4
1716, 7, 3wral 2509 . . 3
185, 6, 17w3a 939 . 2
192, 18wb 178 1
 Colors of variables: wff set class This definition is referenced by:  dfsmo2  6250  issmo  6251  smoeq  6253  smodm  6254  smores  6255  smofvon  6262  smoel  6263  smoiso  6265
 Copyright terms: Public domain W3C validator