Metamath Proof Explorer

Theorem ssinc

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

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

Proof

Step Hyp Ref Expression
1 ssinc.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 ssinc.2 
 |-  ( ( ph /\ m e. ( M ..^ N ) ) -> ( F ` m ) C_ ( F ` ( m + 1 ) ) )
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 id 
 |-  ( ph -> ph )
15 fveq2 
 |-  ( n = M -> ( F ` n ) = ( F ` M ) )
16 15 sseq2d 
 |-  ( n = M -> ( ( F ` M ) C_ ( F ` n ) <-> ( F ` M ) C_ ( F ` M ) ) )
17 16 imbi2d 
 |-  ( n = M -> ( ( ph -> ( F ` M ) C_ ( F ` n ) ) <-> ( ph -> ( F ` M ) C_ ( F ` M ) ) ) )
18 fveq2 
 |-  ( n = m -> ( F ` n ) = ( F ` m ) )
19 18 sseq2d 
 |-  ( n = m -> ( ( F ` M ) C_ ( F ` n ) <-> ( F ` M ) C_ ( F ` m ) ) )
20 19 imbi2d 
 |-  ( n = m -> ( ( ph -> ( F ` M ) C_ ( F ` n ) ) <-> ( ph -> ( F ` M ) C_ ( F ` m ) ) ) )
21 fveq2 
 |-  ( n = ( m + 1 ) -> ( F ` n ) = ( F ` ( m + 1 ) ) )
22 21 sseq2d 
 |-  ( n = ( m + 1 ) -> ( ( F ` M ) C_ ( F ` n ) <-> ( F ` M ) C_ ( F ` ( m + 1 ) ) ) )
23 22 imbi2d 
 |-  ( n = ( m + 1 ) -> ( ( ph -> ( F ` M ) C_ ( F ` n ) ) <-> ( ph -> ( F ` M ) C_ ( F ` ( m + 1 ) ) ) ) )
24 fveq2 
 |-  ( n = N -> ( F ` n ) = ( F ` N ) )
25 24 sseq2d 
 |-  ( n = N -> ( ( F ` M ) C_ ( F ` n ) <-> ( F ` M ) C_ ( F ` N ) ) )
26 25 imbi2d 
 |-  ( n = N -> ( ( ph -> ( F ` M ) C_ ( F ` n ) ) <-> ( ph -> ( F ` M ) C_ ( F ` N ) ) ) )
27 ssidd 
 |-  ( ph -> ( F ` M ) C_ ( F ` M ) )
28 27 a1i 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( ph -> ( F ` M ) C_ ( F ` M ) ) )
29 simpr 
 |-  ( ( ( ph -> ( F ` M ) C_ ( F ` m ) ) /\ ph ) -> ph )
30 simpl 
 |-  ( ( ( ph -> ( F ` M ) C_ ( F ` m ) ) /\ ph ) -> ( ph -> ( F ` M ) C_ ( F ` m ) ) )
31 pm3.35 
 |-  ( ( ph /\ ( ph -> ( F ` M ) C_ ( F ` m ) ) ) -> ( F ` M ) C_ ( F ` m ) )
32 29 30 31 syl2anc 
 |-  ( ( ( ph -> ( F ` M ) C_ ( F ` m ) ) /\ ph ) -> ( F ` M ) C_ ( F ` m ) )
33 32 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 ) )
34 simpr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> ph )
35 simplll 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> M e. ZZ )
36 simplr1 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> m e. ZZ )
37 simplr2 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> M <_ m )
38 35 36 37 3jca 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> ( M e. ZZ /\ m e. ZZ /\ M <_ m ) )
39 eluz2 
 |-  ( m e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ m e. ZZ /\ M <_ m ) )
40 38 39 sylibr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> m e. ( ZZ>= ` M ) )
41 simpllr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> N e. ZZ )
42 simplr3 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> m < N )
43 40 41 42 3jca 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> ( m e. ( ZZ>= ` M ) /\ N e. ZZ /\ m < N ) )
44 elfzo2 
 |-  ( m e. ( M ..^ N ) <-> ( m e. ( ZZ>= ` M ) /\ N e. ZZ /\ m < N ) )
45 43 44 sylibr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> m e. ( M ..^ N ) )
46 34 45 2 syl2anc 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( m e. ZZ /\ M <_ m /\ m < N ) ) /\ ph ) -> ( F ` m ) C_ ( F ` ( m + 1 ) ) )
47 46 3adant2 
 |-  ( ( ( ( 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 + 1 ) ) )
48 33 47 sstrd 
 |-  ( ( ( ( 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 + 1 ) ) )
49 48 3exp 
 |-  ( ( ( 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 + 1 ) ) ) ) )
50 17 20 23 26 28 49 fzind 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( N e. ZZ /\ M <_ N /\ N <_ N ) ) -> ( ph -> ( F ` M ) C_ ( F ` N ) ) )
51 13 14 50 sylc 
 |-  ( ph -> ( F ` M ) C_ ( F ` N ) )