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

Metamath Proof Explorer

Theorem smoeq

Description: Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011)

Ref Expression
Assertion smoeq 
|- ( A = B -> ( Smo A <-> Smo B ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A = B -> A = B )
2 dmeq 
 |-  ( A = B -> dom A = dom B )
3 1 2 feq12d 
 |-  ( A = B -> ( A : dom A --> On <-> B : dom B --> On ) )
4 ordeq 
 |-  ( dom A = dom B -> ( Ord dom A <-> Ord dom B ) )
5 2 4 syl 
 |-  ( A = B -> ( Ord dom A <-> Ord dom B ) )
6 fveq1 
 |-  ( A = B -> ( A ` x ) = ( B ` x ) )
7 fveq1 
 |-  ( A = B -> ( A ` y ) = ( B ` y ) )
8 6 7 eleq12d 
 |-  ( A = B -> ( ( A ` x ) e. ( A ` y ) <-> ( B ` x ) e. ( B ` y ) ) )
9 8 imbi2d 
 |-  ( A = B -> ( ( x e. y -> ( A ` x ) e. ( A ` y ) ) <-> ( x e. y -> ( B ` x ) e. ( B ` y ) ) ) )
10 9 2ralbidv 
 |-  ( A = B -> ( A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) <-> A. x e. dom A A. y e. dom A ( x e. y -> ( B ` x ) e. ( B ` y ) ) ) )
11 2 raleqdv 
 |-  ( A = B -> ( A. y e. dom A ( x e. y -> ( B ` x ) e. ( B ` y ) ) <-> A. y e. dom B ( x e. y -> ( B ` x ) e. ( B ` y ) ) ) )
12 11 ralbidv 
 |-  ( A = B -> ( A. x e. dom A A. y e. dom A ( x e. y -> ( B ` x ) e. ( B ` y ) ) <-> A. x e. dom A A. y e. dom B ( x e. y -> ( B ` x ) e. ( B ` y ) ) ) )
13 2 raleqdv 
 |-  ( A = B -> ( A. x e. dom A A. y e. dom B ( x e. y -> ( B ` x ) e. ( B ` y ) ) <-> A. x e. dom B A. y e. dom B ( x e. y -> ( B ` x ) e. ( B ` y ) ) ) )
14 10 12 13 3bitrd 
 |-  ( A = B -> ( A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) <-> A. x e. dom B A. y e. dom B ( x e. y -> ( B ` x ) e. ( B ` y ) ) ) )
15 3 5 14 3anbi123d 
 |-  ( A = B -> ( ( 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 ) ) ) <-> ( B : dom B --> On /\ Ord dom B /\ A. x e. dom B A. y e. dom B ( x e. y -> ( B ` x ) e. ( B ` y ) ) ) ) )
16 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 ) ) ) )
17 df-smo 
 |-  ( Smo B <-> ( B : dom B --> On /\ Ord dom B /\ A. x e. dom B A. y e. dom B ( x e. y -> ( B ` x ) e. ( B ` y ) ) ) )
18 15 16 17 3bitr4g 
 |-  ( A = B -> ( Smo A <-> Smo B ) )