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 resss ⊢ ( 𝐴 ↾ 𝐵 ) ⊆ 𝐴
6 5 rnssi ⊢ ran ( 𝐴 ↾ 𝐵 ) ⊆ ran 𝐴
7 sstr ⊢ ( ( ran ( 𝐴 ↾ 𝐵 ) ⊆ ran 𝐴 ∧ ran 𝐴 ⊆ On ) → ran ( 𝐴 ↾ 𝐵 ) ⊆ On )
8 6 7 mpan ⊢ ( ran 𝐴 ⊆ On → ran ( 𝐴 ↾ 𝐵 ) ⊆ On )
9 4 8 anim12i ⊢ ( ( 𝐴 Fn dom 𝐴 ∧ ran 𝐴 ⊆ On ) → ( ( 𝐴 ↾ 𝐵 ) Fn dom ( 𝐴 ↾ 𝐵 ) ∧ ran ( 𝐴 ↾ 𝐵 ) ⊆ On ) )
10 df-f ⊢ ( 𝐴 : dom 𝐴 ⟶ On ↔ ( 𝐴 Fn dom 𝐴 ∧ ran 𝐴 ⊆ On ) )
11 df-f ⊢ ( ( 𝐴 ↾ 𝐵 ) : dom ( 𝐴 ↾ 𝐵 ) ⟶ On ↔ ( ( 𝐴 ↾ 𝐵 ) Fn dom ( 𝐴 ↾ 𝐵 ) ∧ ran ( 𝐴 ↾ 𝐵 ) ⊆ On ) )
12 9 10 11 3imtr4i ⊢ ( 𝐴 : dom 𝐴 ⟶ On → ( 𝐴 ↾ 𝐵 ) : dom ( 𝐴 ↾ 𝐵 ) ⟶ On )
13 12 a1i ⊢ ( 𝐵 ∈ dom 𝐴 → ( 𝐴 : dom 𝐴 ⟶ On → ( 𝐴 ↾ 𝐵 ) : dom ( 𝐴 ↾ 𝐵 ) ⟶ On ) )
14 ordelord ⊢ ( ( Ord dom 𝐴 ∧ 𝐵 ∈ dom 𝐴 ) → Ord 𝐵 )
15 14 expcom ⊢ ( 𝐵 ∈ dom 𝐴 → ( Ord dom 𝐴 → Ord 𝐵 ) )
16 ordin ⊢ ( ( Ord 𝐵 ∧ Ord dom 𝐴 ) → Ord ( 𝐵 ∩ dom 𝐴 ) )
17 16 ex ⊢ ( Ord 𝐵 → ( Ord dom 𝐴 → Ord ( 𝐵 ∩ dom 𝐴 ) ) )
18 15 17 syli ⊢ ( 𝐵 ∈ dom 𝐴 → ( Ord dom 𝐴 → Ord ( 𝐵 ∩ dom 𝐴 ) ) )
19 dmres ⊢ dom ( 𝐴 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐴 )
20 ordeq ⊢ ( dom ( 𝐴 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐴 ) → ( Ord dom ( 𝐴 ↾ 𝐵 ) ↔ Ord ( 𝐵 ∩ dom 𝐴 ) ) )
21 19 20 ax-mp ⊢ ( Ord dom ( 𝐴 ↾ 𝐵 ) ↔ Ord ( 𝐵 ∩ dom 𝐴 ) )
22 18 21 imbitrrdi ⊢ ( 𝐵 ∈ dom 𝐴 → ( Ord dom 𝐴 → Ord dom ( 𝐴 ↾ 𝐵 ) ) )
23 dmss ⊢ ( ( 𝐴 ↾ 𝐵 ) ⊆ 𝐴 → dom ( 𝐴 ↾ 𝐵 ) ⊆ dom 𝐴 )
24 5 23 ax-mp ⊢ dom ( 𝐴 ↾ 𝐵 ) ⊆ dom 𝐴
25 ssralv ⊢ ( dom ( 𝐴 ↾ 𝐵 ) ⊆ dom 𝐴 → ( ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) )
26 24 25 ax-mp ⊢ ( ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) )
27 ssralv ⊢ ( dom ( 𝐴 ↾ 𝐵 ) ⊆ dom 𝐴 → ( ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) )
28 24 27 ax-mp ⊢ ( ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) )
29 28 ralimi ⊢ ( ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) )
30 26 29 syl ⊢ ( ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) )
31 inss1 ⊢ ( 𝐵 ∩ dom 𝐴 ) ⊆ 𝐵
32 19 31 eqsstri ⊢ dom ( 𝐴 ↾ 𝐵 ) ⊆ 𝐵
33 simpl ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∧ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ) → 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) )
34 32 33 sselid ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∧ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
35 34 fvresd ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∧ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ) → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑥 ) )
36 simpr ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∧ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ) → 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) )
37 32 36 sselid ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∧ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
38 37 fvresd ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∧ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ) → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) )
39 35 38 eleq12d ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∧ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ) → ( ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) ↔ ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) )
40 39 imbi2d ⊢ ( ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∧ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ) → ( ( 𝑥 ∈ 𝑦 → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) ) ↔ ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) )
41 40 ralbidva ⊢ ( 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) → ( ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) )
42 41 ralbiia ⊢ ( ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) )
43 30 42 sylibr ⊢ ( ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) ) )
44 43 a1i ⊢ ( 𝐵 ∈ dom 𝐴 → ( ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) ) ) )
45 13 22 44 3anim123d ⊢ ( 𝐵 ∈ dom 𝐴 → ( ( 𝐴 : dom 𝐴 ⟶ On ∧ Ord dom 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) → ( ( 𝐴 ↾ 𝐵 ) : dom ( 𝐴 ↾ 𝐵 ) ⟶ On ∧ Ord dom ( 𝐴 ↾ 𝐵 ) ∧ ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ) )
46 df-smo ⊢ ( Smo 𝐴 ↔ ( 𝐴 : dom 𝐴 ⟶ On ∧ Ord dom 𝐴 ∧ ∀ 𝑥 ∈ dom 𝐴 ∀ 𝑦 ∈ dom 𝐴 ( 𝑥 ∈ 𝑦 → ( 𝐴 ‘ 𝑥 ) ∈ ( 𝐴 ‘ 𝑦 ) ) ) )
47 df-smo ⊢ ( Smo ( 𝐴 ↾ 𝐵 ) ↔ ( ( 𝐴 ↾ 𝐵 ) : dom ( 𝐴 ↾ 𝐵 ) ⟶ On ∧ Ord dom ( 𝐴 ↾ 𝐵 ) ∧ ∀ 𝑥 ∈ dom ( 𝐴 ↾ 𝐵 ) ∀ 𝑦 ∈ dom ( 𝐴 ↾ 𝐵 ) ( 𝑥 ∈ 𝑦 → ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑥 ) ∈ ( ( 𝐴 ↾ 𝐵 ) ‘ 𝑦 ) ) ) )
48 45 46 47 3imtr4g ⊢ ( 𝐵 ∈ dom 𝐴 → ( Smo 𝐴 → Smo ( 𝐴 ↾ 𝐵 ) ) )
49 48 impcom ⊢ ( ( Smo 𝐴 ∧ 𝐵 ∈ dom 𝐴 ) → Smo ( 𝐴 ↾ 𝐵 ) )