Definition df-smo 7443

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 /\ A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) )

Distinct variable group:   x, y, A

Detailed syntax breakdown of Definition df-smo

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wsmo 7442	. 2 wff Smo A
3	1	cdm 5114	. . . 4 class dom A
4		con0 5723	. . . 4 class On
5	3, 4, 1	wf 5884	. . 3 wff A : dom A --> On
6	3	word 5722	. . 3 wff Ord dom A
7		vx	. . . . . . 7 setvar x
8		vy	. . . . . . 7 setvar y
9	7, 8	wel 1991	. . . . . 6 wff x e. y
10	7	cv 1482	. . . . . . . 8 class x
11	10, 1	cfv 5888	. . . . . . 7 class ( A ` x )
12	8	cv 1482	. . . . . . . 8 class y
13	12, 1	cfv 5888	. . . . . . 7 class ( A ` y )
14	11, 13	wcel 1990	. . . . . 6 wff ( A ` x ) e. ( A ` y )
15	9, 14	wi 4	. . . . 5 wff ( x e. y -> ( A ` x ) e. ( A ` y ) )
16	15, 8, 3	wral 2912	. . . 4 wff A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) )
17	16, 7, 3	wral 2912	. . 3 wff A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) )
18	5, 6, 17	w3a 1037	. 2 wff ( 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 ) ) )
19	2, 18	wb 196	1 wff ( 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 ) ) ) )

This definition is referenced by:  dfsmo2  7444  issmo  7445  smoeq  7447  smodm  7448  smores  7449  smofvon  7456  smoel  7457  smoiso  7459