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 𝐵 ) )