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⁡Ax∈y→A⁡x∈A⁡y↔∀x∈dom⁡A∀y∈dom⁡Ax∈y→B⁡x∈B⁡y
11 2 raleqdv ⊢A=B→∀y∈dom⁡Ax∈y→B⁡x∈B⁡y↔∀y∈dom⁡Bx∈y→B⁡x∈B⁡y
12 11 ralbidv ⊢A=B→∀x∈dom⁡A∀y∈dom⁡Ax∈y→B⁡x∈B⁡y↔∀x∈dom⁡A∀y∈dom⁡Bx∈y→B⁡x∈B⁡y
13 2 raleqdv ⊢A=B→∀x∈dom⁡A∀y∈dom⁡Bx∈y→B⁡x∈B⁡y↔∀x∈dom⁡B∀y∈dom⁡Bx∈y→B⁡x∈B⁡y
14 10 12 13 3bitrd ⊢A=B→∀x∈dom⁡A∀y∈dom⁡Ax∈y→A⁡x∈A⁡y↔∀x∈dom⁡B∀y∈dom⁡Bx∈y→B⁡x∈B⁡y
15 3 5 14 3anbi123d ⊢A=B→A:dom⁡A⟶On∧Ord⁡dom⁡A∧∀x∈dom⁡A∀y∈dom⁡Ax∈y→A⁡x∈A⁡y↔B:dom⁡B⟶On∧Ord⁡dom⁡B∧∀x∈dom⁡B∀y∈dom⁡Bx∈y→B⁡x∈B⁡y
16 df-smo ⊢Smo⁡A↔A:dom⁡A⟶On∧Ord⁡dom⁡A∧∀x∈dom⁡A∀y∈dom⁡Ax∈y→A⁡x∈A⁡y
17 df-smo ⊢Smo⁡B↔B:dom⁡B⟶On∧Ord⁡dom⁡B∧∀x∈dom⁡B∀y∈dom⁡Bx∈y→B⁡x∈B⁡y
18 15 16 17 3bitr4g ⊢A=B→Smo⁡A↔Smo⁡B