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⟶\mathrm{On}$$
	issmo.2	$$⊢\mathrm{Ord}B$$
	issmo.3	$$⊢\left(x\in B\wedge y\in B\right)\to \left(x\in y\to A\left(x\right)\in A\left(y\right)\right)$$
	issmo.4	$$⊢\mathrm{dom}A=B$$
Assertion	issmo	$$⊢\mathrm{Smo}A$$

Proof

Step	Hyp	Ref	Expression
1		issmo.1	$$⊢A:B⟶\mathrm{On}$$
2		issmo.2	$$⊢\mathrm{Ord}B$$
3		issmo.3	$$⊢\left(x\in B\wedge y\in B\right)\to \left(x\in y\to A\left(x\right)\in A\left(y\right)\right)$$
4		issmo.4	$$⊢\mathrm{dom}A=B$$
5	4	feq2i	$$⊢A:\mathrm{dom}A⟶\mathrm{On}\leftrightarrow A:B⟶\mathrm{On}$$
6	1 5	mpbir	$$⊢A:\mathrm{dom}A⟶\mathrm{On}$$
7		ordeq	$$⊢\mathrm{dom}A=B\to \left(\mathrm{Ord}\mathrm{dom}A\leftrightarrow \mathrm{Ord}B\right)$$
8	4 7	ax-mp	$$⊢\mathrm{Ord}\mathrm{dom}A\leftrightarrow \mathrm{Ord}B$$
9	2 8	mpbir	$$⊢\mathrm{Ord}\mathrm{dom}A$$
10	4	eleq2i	$$⊢x\in \mathrm{dom}A\leftrightarrow x\in B$$
11	4	eleq2i	$$⊢y\in \mathrm{dom}A\leftrightarrow y\in B$$
12	10 11 3	syl2anb	$$⊢\left(x\in \mathrm{dom}A\wedge y\in \mathrm{dom}A\right)\to \left(x\in y\to A\left(x\right)\in A\left(y\right)\right)$$
13	12	rgen2	$$⊢\forall x\in \mathrm{dom}A\forall y\in \mathrm{dom}A\left(x\in y\to A\left(x\right)\in A\left(y\right)\right)$$
14		df-smo	$$⊢\mathrm{Smo}A\leftrightarrow \left(A:\mathrm{dom}A⟶\mathrm{On}\wedge \mathrm{Ord}\mathrm{dom}A\wedge \forall x\in \mathrm{dom}A\forall y\in \mathrm{dom}A\left(x\in y\to A\left(x\right)\in A\left(y\right)\right)\right)$$
15	6 9 13 14	mpbir3an	$$⊢\mathrm{Smo}A$$