ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-smo Structured version   GIF version

Definition df-smo 5823
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 A ↔ (A:dom A⟶On Ord dom A x dom Ay dom A(x y → (Ax) (Ay))))
Distinct variable group:   x,y,A

Detailed syntax breakdown of Definition df-smo
StepHypRef Expression
1 cA . . 3 class A
21wsmo 5822 . 2 wff Smo A
31cdm 4272 . . . 4 class dom A
4 con0 4049 . . . 4 class On
53, 4, 1wf 4825 . . 3 wff A:dom A⟶On
63word 4048 . . 3 wff Ord dom A
7 vx . . . . . . 7 setvar x
8 vy . . . . . . 7 setvar y
97, 8wel 1375 . . . . . 6 wff x y
107cv 1227 . . . . . . . 8 class x
1110, 1cfv 4829 . . . . . . 7 class (Ax)
128cv 1227 . . . . . . . 8 class y
1312, 1cfv 4829 . . . . . . 7 class (Ay)
1411, 13wcel 1374 . . . . . 6 wff (Ax) (Ay)
159, 14wi 4 . . . . 5 wff (x y → (Ax) (Ay))
1615, 8, 3wral 2284 . . . 4 wff y dom A(x y → (Ax) (Ay))
1716, 7, 3wral 2284 . . 3 wff x dom Ay dom A(x y → (Ax) (Ay))
185, 6, 17w3a 873 . 2 wff (A:dom A⟶On Ord dom A x dom Ay dom A(x y → (Ax) (Ay)))
192, 18wb 98 1 wff (Smo A ↔ (A:dom A⟶On Ord dom A x dom Ay dom A(x y → (Ax) (Ay))))
Colors of variables: wff set class
This definition is referenced by:  dfsmo2  5824  issmo  5825  smoeq  5827  smodm  5828  smores  5829  smofvon  5836  smoel  5837  smoiso  5839
  Copyright terms: Public domain W3C validator