This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) ) )