Metamath Proof Explorer


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 Gino Giotto, 19-May-2023)

Ref Expression
Hypotheses issmo.1 A : B On
issmo.2 Ord B
issmo.3 x B y B x y A x 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 B y B x y A x 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 dom A x B
11 4 eleq2i y dom A y B
12 10 11 3 syl2anb x dom A y dom A x y A x A y
13 12 rgen2 x dom A y dom A x y A x A y
14 df-smo Smo A A : dom A On Ord dom A x dom A y dom A x y A x A y
15 6 9 13 14 mpbir3an Smo A