Theorem issmo

Description: Conditions for which A is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 15-Nov-2011) Avoid ax-13 . (Revised by GG, 19-May-2023)

	Ref	Expression
Hypotheses	issmo.1	|- A : B --> On
	issmo.2	|- Ord B
	issmo.3	|- ( ( x e. B /\ y e. B ) -> ( x e. y -> ( A ` x ) e. ( A ` y ) ) )
	issmo.4	|- dom A = B
Assertion	issmo	|- Smo A

Proof

Step	Hyp	Ref	Expression
1		issmo.1	|- A : B --> On
2		issmo.2	|- Ord B
3		issmo.3	|- ( ( x e. B /\ y e. B ) -> ( x e. y -> ( A ` x ) e. ( A ` y ) ) )
4		issmo.4	|- dom A = B
5	4	feq2i	|- ( A : dom A --> On <-> A : B --> On )
6	1 5	mpbir	|- A : dom A --> On
7		ordeq	|- ( dom A = B -> ( Ord dom A <-> Ord B ) )
8	4 7	ax-mp	|- ( Ord dom A <-> Ord B )
9	2 8	mpbir	|- Ord dom A
10	4	eleq2i	|- ( x e. dom A <-> x e. B )
11	4	eleq2i	|- ( y e. dom A <-> y e. B )
12	10 11 3	syl2anb	|- ( ( x e. dom A /\ y e. dom A ) -> ( x e. y -> ( A ` x ) e. ( A ` y ) ) )
13	12	rgen2	|- A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) )
14		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 ) ) ) )
15	6 9 13 14	mpbir3an	|- Smo A