This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem smores3

Description: A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 19-Nov-2011)

Ref Expression
Assertion smores3 ⊢ Smo ⁡ A ↾ B ∧ C ∈ dom ⁡ A ∩ B ∧ Ord ⁡ B → Smo ⁡ A ↾ C

Proof

Step Hyp Ref Expression
1 dmres ⊢ dom ⁡ A ↾ B = B ∩ dom ⁡ A
2 incom ⊢ B ∩ dom ⁡ A = dom ⁡ A ∩ B
3 1 2 eqtri ⊢ dom ⁡ A ↾ B = dom ⁡ A ∩ B
4 3 eleq2i ⊢ C ∈ dom ⁡ A ↾ B ↔ C ∈ dom ⁡ A ∩ B
5 smores ⊢ Smo ⁡ A ↾ B ∧ C ∈ dom ⁡ A ↾ B → Smo ⁡ A ↾ B ↾ C
6 4 5 sylan2br ⊢ Smo ⁡ A ↾ B ∧ C ∈ dom ⁡ A ∩ B → Smo ⁡ A ↾ B ↾ C
7 6 3adant3 ⊢ Smo ⁡ A ↾ B ∧ C ∈ dom ⁡ A ∩ B ∧ Ord ⁡ B → Smo ⁡ A ↾ B ↾ C
8 elinel2 ⊢ C ∈ dom ⁡ A ∩ B → C ∈ B
9 ordelss ⊢ Ord ⁡ B ∧ C ∈ B → C ⊆ B
10 9 ancoms ⊢ C ∈ B ∧ Ord ⁡ B → C ⊆ B
11 8 10 sylan ⊢ C ∈ dom ⁡ A ∩ B ∧ Ord ⁡ B → C ⊆ B
12 11 3adant1 ⊢ Smo ⁡ A ↾ B ∧ C ∈ dom ⁡ A ∩ B ∧ Ord ⁡ B → C ⊆ B
13 resabs1 ⊢ C ⊆ B → A ↾ B ↾ C = A ↾ C
14 smoeq ⊢ A ↾ B ↾ C = A ↾ C → Smo ⁡ A ↾ B ↾ C ↔ Smo ⁡ A ↾ C
15 12 13 14 3syl ⊢ Smo ⁡ A ↾ B ∧ C ∈ dom ⁡ A ∩ B ∧ Ord ⁡ B → Smo ⁡ A ↾ B ↾ C ↔ Smo ⁡ A ↾ C
16 7 15 mpbid ⊢ Smo ⁡ A ↾ B ∧ C ∈ dom ⁡ A ∩ B ∧ Ord ⁡ B → Smo ⁡ A ↾ C