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