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

Definition df-smo 7036
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 7035 . 2
31cdm 5004 . . . 4
4 con0 4883 . . . 4
53, 4, 1wf 5589 . . 3
63word 4882 . . 3
7 vx . . . . . . 7
8 vy . . . . . . 7
97, 8wel 1819 . . . . . 6
107cv 1394 . . . . . . . 8
1110, 1cfv 5593 . . . . . . 7
128cv 1394 . . . . . . . 8
1312, 1cfv 5593 . . . . . . 7
1411, 13wcel 1818 . . . . . 6
159, 14wi 4 . . . . 5
1615, 8, 3wral 2807 . . . 4
1716, 7, 3wral 2807 . . 3
185, 6, 17w3a 973 . 2
192, 18wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  dfsmo2  7037  issmo  7038  smoeq  7040  smodm  7041  smores  7042  smofvon  7049  smoel  7050  smoiso  7052
  Copyright terms: Public domain W3C validator