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 ( 𝐴 ↾ 𝐶 ) )