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 ( 𝐴 = 𝐵 → ( Smo 𝐴 ↔ Smo 𝐵 ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝐴 = 𝐵 → 𝐴 = 𝐵 )
2 dmeq ⊢ ( 𝐴 = 𝐵 → dom 𝐴 = dom 𝐵 )
3 1 2 feq12d ⊢ ( 𝐴 = 𝐵 → ( 𝐴 : dom 𝐴 ⟶ On ↔ 𝐵 : dom 𝐵 ⟶ On ) )
4 ordeq ⊢ ( dom 𝐴 = dom 𝐵 → ( Ord dom 𝐴 ↔ Ord dom 𝐵 ) )
5 2 4 syl ⊢ ( 𝐴 = 𝐵 → ( Ord dom 𝐴 ↔ Ord dom 𝐵 ) )
6 fveq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
7 fveq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) )
8 6 7 eleq12d ⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ↔ ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) )
9 8 imbi2d ⊢ ( 𝐴 = 𝐵 → ( ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ↔ ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ) )
10 9 2ralbidv ⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ) )
11 2 raleqdv ⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ dom 𝐵 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ) )
12 11 ralbidv ⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐵 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ) )
13 2 raleqdv ⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐵 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ dom 𝐵 ∀ 𝑦 ∈ dom 𝐵 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ) )
14 10 12 13 3bitrd ⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ dom 𝐵 ∀ 𝑦 ∈ dom 𝐵 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ) )
15 3 5 14 3anbi123d ⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 : dom 𝐴 ⟶ On ∧ Ord dom 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) ↔ ( 𝐵 : dom 𝐵 ⟶ On ∧ Ord dom 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐵 ∀ 𝑦 ∈ dom 𝐵 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ) ) )
16 df-smo ⊢ ( Smo 𝐴 ↔ ( 𝐴 : dom 𝐴 ⟶ On ∧ Ord dom 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) )
17 df-smo ⊢ ( Smo 𝐵 ↔ ( 𝐵 : dom 𝐵 ⟶ On ∧ Ord dom 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐵 ∀ 𝑦 ∈ dom 𝐵 ( 𝑥 ∈ 𝑦 → ( 𝐵 ‘ 𝑥 ) ∈ ( 𝐵 ‘ 𝑦 ) ) ) )
18 15 16 17 3bitr4g ⊢ ( 𝐴 = 𝐵 → ( Smo 𝐴 ↔ Smo 𝐵 ) )