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 A y B x B y
9 8 imbi2d A = B x y A x A y x y B x B y
10 9 2ralbidv A = B x dom A y dom A x y A x A y x dom A y dom A x y B x B y
11 2 raleqdv A = B y dom A x y B x B y y dom B x y B x B y
12 11 ralbidv A = B x dom A y dom A x y B x B y x dom A y dom B x y B x B y
13 2 raleqdv A = B x dom A y dom B x y B x B y x dom B y dom B x y B x B y
14 10 12 13 3bitrd A = B x dom A y dom A x y A x A y x dom B y dom B x y B x B y
15 3 5 14 3anbi123d A = B A : dom A On Ord dom A x dom A y dom A x y A x A y B : dom B On Ord dom B x dom B y dom B x y B x B y
16 df-smo Smo A A : dom A On Ord dom A x dom A y dom A x y A x A y
17 df-smo Smo B B : dom B On Ord dom B x dom B y dom B x y B x B y
18 15 16 17 3bitr4g A = B Smo A Smo B