Metamath Proof Explorer

Theorem smores

Description: A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 16-Nov-2011) (Proof shortened by Mario Carneiro, 5-Dec-2016)

Ref Expression
Assertion smores ( ( Smo 𝐴 ∧ 𝐵 ∈ dom 𝐴 ) → Smo ( 𝐴 ↾ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 funres ⊢ ( Fun 𝐴 → Fun ( 𝐴 ↾ 𝐵 ) )
2 funfn ⊢ ( Fun 𝐴 ↔ 𝐴 Fn dom 𝐴 )
3 funfn ⊢ ( Fun ( 𝐴 ↾ 𝐵 ) ↔ ( 𝐴 ↾ 𝐵 ) Fn dom ( 𝐴 ↾ 𝐵 ) )
4 1 2 3 3imtr3i ⊢ ( 𝐴 Fn dom 𝐴 → ( 𝐴 ↾ 𝐵 ) Fn dom ( 𝐴 ↾ 𝐵 ) )
5 rnresss ⊢ ran ( 𝐴 ↾ 𝐵 ) ⊆ ran 𝐴
6 sstr ⊢ ( ( ran ( 𝐴 ↾ 𝐵 ) ⊆ ran 𝐴 ∧ ran 𝐴 ⊆ On ) → ran ( 𝐴 ↾ 𝐵 ) ⊆ On )
7 5 6 mpan ⊢ ( ran 𝐴 ⊆ On → ran ( 𝐴 ↾ 𝐵 ) ⊆ On )
8 4 7 anim12i ⊢ ( ( 𝐴 Fn dom 𝐴 ∧ ran 𝐴 ⊆ On ) → ( ( 𝐴 ↾ 𝐵 ) Fn dom ( 𝐴 ↾ 𝐵 ) ∧ ran ( 𝐴 ↾ 𝐵 ) ⊆ On ) )
9 df-f ⊢ ( 𝐴 : dom 𝐴 ⟶ On ↔ ( 𝐴 Fn dom 𝐴 ∧ ran 𝐴 ⊆ On ) )
10 df-f ⊢ ( ( 𝐴 ↾ 𝐵 ) : dom ( 𝐴 ↾ 𝐵 ) ⟶ On ↔ ( ( 𝐴 ↾ 𝐵 ) Fn dom ( 𝐴 ↾ 𝐵 ) ∧ ran ( 𝐴 ↾ 𝐵 ) ⊆ On ) )
11 8 9 10 3imtr4i ⊢ ( 𝐴 : dom 𝐴 ⟶ On → ( 𝐴 ↾ 𝐵 ) : dom ( 𝐴 ↾ 𝐵 ) ⟶ On )
12 11 a1i ⊢ ( 𝐵 ∈ dom 𝐴 → ( 𝐴 : dom 𝐴 ⟶ On → ( 𝐴 ↾ 𝐵 ) : dom ( 𝐴 ↾ 𝐵 ) ⟶ On ) )
13 ordelord ⊢ ( ( Ord dom 𝐴 ∧ 𝐵 ∈ dom 𝐴 ) → Ord 𝐵 )
14 13 expcom ⊢ ( 𝐵 ∈ dom 𝐴 → ( Ord dom 𝐴 → Ord 𝐵 ) )
15 ordin ⊢ ( ( Ord 𝐵 ∧ Ord dom 𝐴 ) → Ord ( 𝐵 ∩ dom 𝐴 ) )
16 15 ex ⊢ ( Ord 𝐵 → ( Ord dom 𝐴 → Ord ( 𝐵 ∩ dom 𝐴 ) ) )
17 14 16 syli ⊢ ( 𝐵 ∈ dom 𝐴 → ( Ord dom 𝐴 → Ord ( 𝐵 ∩ dom 𝐴 ) ) )
18 dmres ⊢ dom ( 𝐴 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐴 )
19 ordeq ⊢ ( dom ( 𝐴 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐴 ) → ( Ord dom ( 𝐴 ↾ 𝐵 ) ↔ Ord ( 𝐵 ∩ dom 𝐴 ) ) )
20 18 19 ax-mp ⊢ ( Ord dom ( 𝐴 ↾ 𝐵 ) ↔ Ord ( 𝐵 ∩ dom 𝐴 ) )
21 17 20 imbitrrdi ⊢ ( 𝐵 ∈ dom 𝐴 → ( Ord dom 𝐴 → Ord dom ( 𝐴 ↾ 𝐵 ) ) )
22 dmresss ⊢ dom ( 𝐴 ↾ 𝐵 ) ⊆ dom 𝐴
23 ssralv ⊢ ( dom ( 𝐴 ↾ 𝐵 ) ⊆ dom 𝐴 → ( ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) )
24 22 23 ax-mp ⊢ ( ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) )
25 ssralv ⊢ ( dom ( 𝐴 ↾ 𝐵 ) ⊆ dom 𝐴 → ( ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) )
26 22 25 ax-mp ⊢ ( ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) )
27 26 ralimi ⊢ ( ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) )
28 24 27 syl ⊢ ( ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) )
29 resdmss ⊢ dom ( 𝐴 ↾ 𝐵 ) ⊆ 𝐵
30 simpl ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∧ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ) → 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) )
31 29 30 sselid ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∧ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
32 31 fvresd ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∧ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ) → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
33 simpr ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∧ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ) → 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) )
34 29 33 sselid ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∧ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
35 34 fvresd ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∧ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ) → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) )
36 32 35 eleq12d ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∧ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ) → ( ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) ↔ ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) )
37 36 imbi2d ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∧ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ) → ( ( 𝑥 ∈ 𝑦 → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) ) ↔ ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) )
38 37 ralbidva ⊢ ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) → ( ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) )
39 38 ralbiia ⊢ ( ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) )
40 28 39 sylibr ⊢ ( ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) ) )
41 40 a1i ⊢ ( 𝐵 ∈ dom 𝐴 → ( ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) ) ) )
42 12 21 41 3anim123d ⊢ ( 𝐵 ∈ dom 𝐴 → ( ( 𝐴 : dom 𝐴 ⟶ On ∧ Ord dom 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) → ( ( 𝐴 ↾ 𝐵 ) : dom ( 𝐴 ↾ 𝐵 ) ⟶ On ∧ Ord dom ( 𝐴 ↾ 𝐵 ) ∧ ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ) )
43 df-smo ⊢ ( Smo 𝐴 ↔ ( 𝐴 : dom 𝐴 ⟶ On ∧ Ord dom 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) )
44 df-smo ⊢ ( Smo ( 𝐴 ↾ 𝐵 ) ↔ ( ( 𝐴 ↾ 𝐵 ) : dom ( 𝐴 ↾ 𝐵 ) ⟶ On ∧ Ord dom ( 𝐴 ↾ 𝐵 ) ∧ ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) ) ) )
45 42 43 44 3imtr4g ⊢ ( 𝐵 ∈ dom 𝐴 → ( Smo 𝐴 → Smo ( 𝐴 ↾ 𝐵 ) ) )
46 45 impcom ⊢ ( ( Smo 𝐴 ∧ 𝐵 ∈ dom 𝐴 ) → Smo ( 𝐴 ↾ 𝐵 ) )