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 ( 𝐹𝐴 ) )