Metamath Proof Explorer


Definition df-smo

Description: Definition of a strictly monotone ordinal function. Definition 7.46 in TakeutiZaring p. 50. (Contributed by Andrew Salmon, 15-Nov-2011)

Ref Expression
Assertion df-smo
|- ( Smo A <-> ( A : dom A --> On /\ Ord dom A /\ A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA
 |-  A
1 0 wsmo
 |-  Smo A
2 0 cdm
 |-  dom A
3 con0
 |-  On
4 2 3 0 wf
 |-  A : dom A --> On
5 2 word
 |-  Ord dom A
6 vx
 |-  x
7 vy
 |-  y
8 6 cv
 |-  x
9 7 cv
 |-  y
10 8 9 wcel
 |-  x e. y
11 8 0 cfv
 |-  ( A ` x )
12 9 0 cfv
 |-  ( A ` y )
13 11 12 wcel
 |-  ( A ` x ) e. ( A ` y )
14 10 13 wi
 |-  ( x e. y -> ( A ` x ) e. ( A ` y ) )
15 14 7 2 wral
 |-  A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) )
16 15 6 2 wral
 |-  A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) )
17 4 5 16 w3a
 |-  ( A : dom A --> On /\ Ord dom A /\ A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) )
18 1 17 wb
 |-  ( Smo A <-> ( A : dom A --> On /\ Ord dom A /\ A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) )