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