Metamath Proof Explorer

Theorem smores2

Description: A strictly monotone ordinal function restricted to an ordinal is still monotone. (Contributed by Mario Carneiro, 15-Mar-2013)

Ref Expression
Assertion smores2 ( ( Smo 𝐹 ∧ Ord 𝐴 ) → Smo ( 𝐹 ↾ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 dfsmo2 ⊢ ( Smo 𝐹 ↔ ( 𝐹 : dom 𝐹 ⟶ On ∧ Ord dom 𝐹 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
2 1 simp1bi ⊢ ( Smo 𝐹 → 𝐹 : dom 𝐹 ⟶ On )
3 2 ffund ⊢ ( Smo 𝐹 → Fun 𝐹 )
4 funres ⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ 𝐴 ) )
5 4 funfnd ⊢ ( Fun 𝐹 → ( 𝐹 ↾ 𝐴 ) Fn dom ( 𝐹 ↾ 𝐴 ) )
6 3 5 syl ⊢ ( Smo 𝐹 → ( 𝐹 ↾ 𝐴 ) Fn dom ( 𝐹 ↾ 𝐴 ) )
7 df-ima ⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 )
8 imassrn ⊢ ( 𝐹 “ 𝐴 ) ⊆ ran 𝐹
9 7 8 eqsstrri ⊢ ran ( 𝐹 ↾ 𝐴 ) ⊆ ran 𝐹
10 2 frnd ⊢ ( Smo 𝐹 → ran 𝐹 ⊆ On )
11 9 10 sstrid ⊢ ( Smo 𝐹 → ran ( 𝐹 ↾ 𝐴 ) ⊆ On )
12 df-f ⊢ ( ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ On ↔ ( ( 𝐹 ↾ 𝐴 ) Fn dom ( 𝐹 ↾ 𝐴 ) ∧ ran ( 𝐹 ↾ 𝐴 ) ⊆ On ) )
13 6 11 12 sylanbrc ⊢ ( Smo 𝐹 → ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ On )
14 13 adantr ⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ On )
15 smodm ⊢ ( Smo 𝐹 → Ord dom 𝐹 )
16 ordin ⊢ ( ( Ord 𝐴 ∧ Ord dom 𝐹 ) → Ord ( 𝐴 ∩ dom 𝐹 ) )
17 dmres ⊢ dom ( 𝐹 ↾ 𝐴 ) = ( 𝐴 ∩ dom 𝐹 )
18 ordeq ⊢ ( dom ( 𝐹 ↾ 𝐴 ) = ( 𝐴 ∩ dom 𝐹 ) → ( Ord dom ( 𝐹 ↾ 𝐴 ) ↔ Ord ( 𝐴 ∩ dom 𝐹 ) ) )
19 17 18 ax-mp ⊢ ( Ord dom ( 𝐹 ↾ 𝐴 ) ↔ Ord ( 𝐴 ∩ dom 𝐹 ) )
20 16 19 sylibr ⊢ ( ( Ord 𝐴 ∧ Ord dom 𝐹 ) → Ord dom ( 𝐹 ↾ 𝐴 ) )
21 20 ancoms ⊢ ( ( Ord dom 𝐹 ∧ Ord 𝐴 ) → Ord dom ( 𝐹 ↾ 𝐴 ) )
22 15 21 sylan ⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → Ord dom ( 𝐹 ↾ 𝐴 ) )
23 resss ⊢ ( 𝐹 ↾ 𝐴 ) ⊆ 𝐹
24 dmss ⊢ ( ( 𝐹 ↾ 𝐴 ) ⊆ 𝐹 → dom ( 𝐹 ↾ 𝐴 ) ⊆ dom 𝐹 )
25 23 24 ax-mp ⊢ dom ( 𝐹 ↾ 𝐴 ) ⊆ dom 𝐹
26 1 simp3bi ⊢ ( Smo 𝐹 → ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) )
27 ssralv ⊢ ( dom ( 𝐹 ↾ 𝐴 ) ⊆ dom 𝐹 → ( ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) → ∀ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
28 25 26 27 mpsyl ⊢ ( Smo 𝐹 → ∀ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) )
29 28 adantr ⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → ∀ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) )
30 ordtr1 ⊢ ( Ord dom ( 𝐹 ↾ 𝐴 ) → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) → 𝑦 ∈ dom ( 𝐹 ↾ 𝐴 ) ) )
31 22 30 syl ⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) → 𝑦 ∈ dom ( 𝐹 ↾ 𝐴 ) ) )
32 inss1 ⊢ ( 𝐴 ∩ dom 𝐹 ) ⊆ 𝐴
33 17 32 eqsstri ⊢ dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴
34 33 sseli ⊢ ( 𝑦 ∈ dom ( 𝐹 ↾ 𝐴 ) → 𝑦 ∈ 𝐴 )
35 31 34 syl6 ⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) → 𝑦 ∈ 𝐴 ) )
36 35 expcomd ⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → ( 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴 ) ) )
37 36 imp31 ⊢ ( ( ( ( Smo 𝐹 ∧ Ord 𝐴 ) ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝐴 )
38 37 fvresd ⊢ ( ( ( ( Smo 𝐹 ∧ Ord 𝐴 ) ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
39 33 sseli ⊢ ( 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) → 𝑥 ∈ 𝐴 )
40 39 fvresd ⊢ ( 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
41 40 ad2antlr ⊢ ( ( ( ( Smo 𝐹 ∧ Ord 𝐴 ) ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
42 38 41 eleq12d ⊢ ( ( ( ( Smo 𝐹 ∧ Ord 𝐴 ) ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
43 42 ralbidva ⊢ ( ( ( Smo 𝐹 ∧ Ord 𝐴 ) ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
44 43 ralbidva ⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → ( ∀ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ∀ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
45 29 44 mpbird ⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → ∀ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ∀ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) )
46 dfsmo2 ⊢ ( Smo ( 𝐹 ↾ 𝐴 ) ↔ ( ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ On ∧ Ord dom ( 𝐹 ↾ 𝐴 ) ∧ ∀ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ∀ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ) )
47 14 22 45 46 syl3anbrc ⊢ ( ( Smo 𝐹 ∧ Ord 𝐴 ) → Smo ( 𝐹 ↾ 𝐴 ) )