This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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