Metamath Proof Explorer

Theorem ssdec

Description: Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses ssdec.1 
|- ( ph -> N e. ( ZZ>= ` M ) )
ssdec.2 
|- ( ( ph /\ m e. ( M ..^ N ) ) -> ( F ` ( m + 1 ) ) C_ ( F ` m ) )
Assertion ssdec 
|- ( ph -> ( F ` N ) C_ ( F ` M ) )

Proof

Step Hyp Ref Expression
1 ssdec.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 ssdec.2 
 |-  ( ( ph /\ m e. ( M ..^ N ) ) -> ( F ` ( m + 1 ) ) C_ ( F ` m ) )
3 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
4 1 3 syl 
 |-  ( ph -> M e. ZZ )
5 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
6 1 5 syl 
 |-  ( ph -> N e. ZZ )
7 4 6 jca 
 |-  ( ph -> ( M e. ZZ /\ N e. ZZ ) )
8 eluzle 
 |-  ( N e. ( ZZ>= ` M ) -> M <_ N )
9 1 8 syl 
 |-  ( ph -> M <_ N )
10 6 zred 
 |-  ( ph -> N e. RR )
11 10 leidd 
 |-  ( ph -> N <_ N )
12 6 9 11 3jca 
 |-  ( ph -> ( N e. ZZ /\ M <_ N /\ N <_ N ) )
13 7 12 jca 
 |-  ( ph -> ( ( M e. ZZ /\ N e. ZZ ) /\ ( N e. ZZ /\ M <_ N /\ N <_ N ) ) )
14 fveq2 
 |-  ( n = M -> ( F ` n ) = ( F ` M ) )
15 14 sseq1d 
 |-  ( n = M -> ( ( F ` n ) C_ ( F ` M ) <-> ( F ` M ) C_ ( F ` M ) ) )
16 15 imbi2d 
 |-  ( n = M -> ( ( ph -> ( F ` n ) C_ ( F ` M ) ) <-> ( ph -> ( F ` M ) C_ ( F ` M ) ) ) )
17 fveq2 
 |-  ( n = m -> ( F ` n ) = ( F ` m ) )
18 17 sseq1d 
 |-  ( n = m -> ( ( F ` n ) C_ ( F ` M ) <-> ( F ` m ) C_ ( F ` M ) ) )
19 18 imbi2d 
 |-  ( n = m -> ( ( ph -> ( F ` n ) C_ ( F ` M ) ) <-> ( ph -> ( F ` m ) C_ ( F ` M ) ) ) )
20 fveq2 
 |-  ( n = ( m + 1 ) -> ( F ` n ) = ( F ` ( m + 1 ) ) )
21 20 sseq1d 
 |-  ( n = ( m + 1 ) -> ( ( F ` n ) C_ ( F ` M ) <-> ( F ` ( m + 1 ) ) C_ ( F ` M ) ) )
22 21 imbi2d 
 |-  ( n = ( m + 1 ) -> ( ( ph -> ( F ` n ) C_ ( F ` M ) ) <-> ( ph -> ( F ` ( m + 1 ) ) C_ ( F ` M ) ) ) )
23 fveq2 
 |-  ( n = N -> ( F ` n ) = ( F ` N ) )
24 23 sseq1d 
 |-  ( n = N -> ( ( F ` n ) C_ ( F ` M ) <-> ( F ` N ) C_ ( F ` M ) ) )
25 24 imbi2d 
 |-  ( n = N -> ( ( ph -> ( F ` n ) C_ ( F ` M ) ) <-> ( ph -> ( F ` N ) C_ ( F ` M ) ) ) )
26 ssidd 
 |-  ( ph -> ( F ` M ) C_ ( F ` M ) )
27 26 a1i 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( ph -> ( F ` M ) C_ ( F ` M ) ) )
28 simpr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> ph )
29 simplll 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> M e. ZZ )
30 simplr1 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> m e. ZZ )
31 simplr2 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> M <_ m )
32 29 30 31 3jca 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> ( M e. ZZ /\ m e. ZZ /\ M <_ m ) )
33 eluz2 
 |-  ( m e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ m e. ZZ /\ M <_ m ) )
34 32 33 sylibr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> m e. ( ZZ>= ` M ) )
35 simpllr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> N e. ZZ )
36 simplr3 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> m < N )
37 34 35 36 3jca 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> ( m e. ( ZZ>= ` M ) /\ N e. ZZ /\ m < N ) )
38 elfzo2 
 |-  ( m e. ( M ..^ N ) <-> ( m e. ( ZZ>= ` M ) /\ N e. ZZ /\ m < N ) )
39 37 38 sylibr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> m e. ( M ..^ N ) )
40 28 39 2 syl2anc 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> ( F ` ( m + 1 ) ) C_ ( F ` m ) )
41 40 3adant2 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ( ph -> ( F ` m ) C_ ( F ` M ) ) /\ ph ) -> ( F ` ( m + 1 ) ) C_ ( F ` m ) )
42 simpr 
 |-  ( ( ( ph -> ( F ` m ) C_ ( F ` M ) ) /\ ph ) -> ph )
43 simpl 
 |-  ( ( ( ph -> ( F ` m ) C_ ( F ` M ) ) /\ ph ) -> ( ph -> ( F ` m ) C_ ( F ` M ) ) )
44 pm3.35 
 |-  ( ( ph /\ ( ph -> ( F ` m ) C_ ( F ` M ) ) ) -> ( F ` m ) C_ ( F ` M ) )
45 42 43 44 syl2anc 
 |-  ( ( ( ph -> ( F ` m ) C_ ( F ` M ) ) /\ ph ) -> ( F ` m ) C_ ( F ` M ) )
46 45 3adant1 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ( ph -> ( F ` m ) C_ ( F ` M ) ) /\ ph ) -> ( F ` m ) C_ ( F ` M ) )
47 41 46 sstrd 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ( ph -> ( F ` m ) C_ ( F ` M ) ) /\ ph ) -> ( F ` ( m + 1 ) ) C_ ( F ` M ) )
48 47 3exp 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) -> ( ( ph -> ( F ` m ) C_ ( F ` M ) ) -> ( ph -> ( F ` ( m + 1 ) ) C_ ( F ` M ) ) ) )
49 16 19 22 25 27 48 fzind 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( N e. ZZ /\ M <_ N /\ N <_ N ) ) -> ( ph -> ( F ` N ) C_ ( F ` M ) ) )
50 13 49 mpcom 
 |-  ( ph -> ( F ` N ) C_ ( F ` M ) )