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

Definition df-smo 5842
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 5841 . 2 wff Smo A
31cdm 4288 . . . 4 class dom A
4 con0 4066 . . . 4 class On
53, 4, 1wf 4841 . . 3 wff A:dom A⟶On
63word 4065 . . 3 wff Ord dom A
7 vx . . . . . . 7 setvar x
8 vy . . . . . . 7 setvar y
97, 8wel 1391 . . . . . 6 wff x y
107cv 1241 . . . . . . . 8 class x
1110, 1cfv 4845 . . . . . . 7 class (Ax)
128cv 1241 . . . . . . . 8 class y
1312, 1cfv 4845 . . . . . . 7 class (Ay)
1411, 13wcel 1390 . . . . . 6 wff (Ax) (Ay)
159, 14wi 4 . . . . 5 wff (x y → (Ax) (Ay))
1615, 8, 3wral 2300 . . . 4 wff y dom A(x y → (Ax) (Ay))
1716, 7, 3wral 2300 . . 3 wff x dom Ay dom A(x y → (Ax) (Ay))
185, 6, 17w3a 884 . 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  5843  issmo  5844  smoeq  5846  smodm  5847  smores  5848  smofvon  5855  smoel  5856  smoiso  5858
  Copyright terms: Public domain W3C validator