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

Definition df-smo 8293
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 (Smo 𝐴 ↔ (𝐴:dom 𝐴⟢On ∧ Ord dom 𝐴 ∧ βˆ€π‘₯ ∈ dom π΄βˆ€π‘¦ ∈ dom 𝐴(π‘₯ ∈ 𝑦 β†’ (π΄β€˜π‘₯) ∈ (π΄β€˜π‘¦))))
Distinct variable group:   π‘₯,𝑦,𝐴

Detailed syntax breakdown of Definition df-smo
StepHypRef Expression
1 cA . . 3 class 𝐴
21wsmo 8292 . 2 wff Smo 𝐴
31cdm 5634 . . . 4 class dom 𝐴
4 con0 6318 . . . 4 class On
53, 4, 1wf 6493 . . 3 wff 𝐴:dom 𝐴⟢On
63word 6317 . . 3 wff Ord dom 𝐴
7 vx . . . . . . 7 setvar π‘₯
8 vy . . . . . . 7 setvar 𝑦
97, 8wel 2108 . . . . . 6 wff π‘₯ ∈ 𝑦
107cv 1541 . . . . . . . 8 class π‘₯
1110, 1cfv 6497 . . . . . . 7 class (π΄β€˜π‘₯)
128cv 1541 . . . . . . . 8 class 𝑦
1312, 1cfv 6497 . . . . . . 7 class (π΄β€˜π‘¦)
1411, 13wcel 2107 . . . . . 6 wff (π΄β€˜π‘₯) ∈ (π΄β€˜π‘¦)
159, 14wi 4 . . . . 5 wff (π‘₯ ∈ 𝑦 β†’ (π΄β€˜π‘₯) ∈ (π΄β€˜π‘¦))
1615, 8, 3wral 3061 . . . 4 wff βˆ€π‘¦ ∈ dom 𝐴(π‘₯ ∈ 𝑦 β†’ (π΄β€˜π‘₯) ∈ (π΄β€˜π‘¦))
1716, 7, 3wral 3061 . . 3 wff βˆ€π‘₯ ∈ dom π΄βˆ€π‘¦ ∈ dom 𝐴(π‘₯ ∈ 𝑦 β†’ (π΄β€˜π‘₯) ∈ (π΄β€˜π‘¦))
185, 6, 17w3a 1088 . 2 wff (𝐴:dom 𝐴⟢On ∧ Ord dom 𝐴 ∧ βˆ€π‘₯ ∈ dom π΄βˆ€π‘¦ ∈ dom 𝐴(π‘₯ ∈ 𝑦 β†’ (π΄β€˜π‘₯) ∈ (π΄β€˜π‘¦)))
192, 18wb 205 1 wff (Smo 𝐴 ↔ (𝐴:dom 𝐴⟢On ∧ Ord dom 𝐴 ∧ βˆ€π‘₯ ∈ dom π΄βˆ€π‘¦ ∈ dom 𝐴(π‘₯ ∈ 𝑦 β†’ (π΄β€˜π‘₯) ∈ (π΄β€˜π‘¦))))
Colors of variables: wff setvar class
This definition is referenced by:  dfsmo2  8294  issmo  8295  smoeq  8297  smodm  8298  smores  8299  smofvon  8306  smoel  8307  smoiso  8309
  Copyright terms: Public domain W3C validator