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