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 ( 𝐴 ↾ 𝐵 ) ∧ 𝐶 ∈ ( dom 𝐴 ∩ 𝐵 ) ∧ Ord 𝐵 ) → Smo ( 𝐴 ↾ 𝐶 ) )

Proof

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