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 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
ssdec.2 ( ( 𝜑𝑚 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐹 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝐹𝑚 ) )
Assertion ssdec ( 𝜑 → ( 𝐹𝑁 ) ⊆ ( 𝐹𝑀 ) )

Proof

Step Hyp Ref Expression
1 ssdec.1 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
2 ssdec.2 ( ( 𝜑𝑚 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐹 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝐹𝑚 ) )
3 eluzel2 ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑀 ∈ ℤ )
4 1 3 syl ( 𝜑𝑀 ∈ ℤ )
5 eluzelz ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑁 ∈ ℤ )
6 1 5 syl ( 𝜑𝑁 ∈ ℤ )
7 4 6 jca ( 𝜑 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
8 eluzle ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑀𝑁 )
9 1 8 syl ( 𝜑𝑀𝑁 )
10 6 zred ( 𝜑𝑁 ∈ ℝ )
11 10 leidd ( 𝜑𝑁𝑁 )
12 6 9 11 3jca ( 𝜑 → ( 𝑁 ∈ ℤ ∧ 𝑀𝑁𝑁𝑁 ) )
13 7 12 jca ( 𝜑 → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀𝑁𝑁𝑁 ) ) )
14 fveq2 ( 𝑛 = 𝑀 → ( 𝐹𝑛 ) = ( 𝐹𝑀 ) )
15 14 sseq1d ( 𝑛 = 𝑀 → ( ( 𝐹𝑛 ) ⊆ ( 𝐹𝑀 ) ↔ ( 𝐹𝑀 ) ⊆ ( 𝐹𝑀 ) ) )
16 15 imbi2d ( 𝑛 = 𝑀 → ( ( 𝜑 → ( 𝐹𝑛 ) ⊆ ( 𝐹𝑀 ) ) ↔ ( 𝜑 → ( 𝐹𝑀 ) ⊆ ( 𝐹𝑀 ) ) ) )
17 fveq2 ( 𝑛 = 𝑚 → ( 𝐹𝑛 ) = ( 𝐹𝑚 ) )
18 17 sseq1d ( 𝑛 = 𝑚 → ( ( 𝐹𝑛 ) ⊆ ( 𝐹𝑀 ) ↔ ( 𝐹𝑚 ) ⊆ ( 𝐹𝑀 ) ) )
19 18 imbi2d ( 𝑛 = 𝑚 → ( ( 𝜑 → ( 𝐹𝑛 ) ⊆ ( 𝐹𝑀 ) ) ↔ ( 𝜑 → ( 𝐹𝑚 ) ⊆ ( 𝐹𝑀 ) ) ) )
20 fveq2 ( 𝑛 = ( 𝑚 + 1 ) → ( 𝐹𝑛 ) = ( 𝐹 ‘ ( 𝑚 + 1 ) ) )
21 20 sseq1d ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝐹𝑛 ) ⊆ ( 𝐹𝑀 ) ↔ ( 𝐹 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝐹𝑀 ) ) )
22 21 imbi2d ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝜑 → ( 𝐹𝑛 ) ⊆ ( 𝐹𝑀 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝐹𝑀 ) ) ) )
23 fveq2 ( 𝑛 = 𝑁 → ( 𝐹𝑛 ) = ( 𝐹𝑁 ) )
24 23 sseq1d ( 𝑛 = 𝑁 → ( ( 𝐹𝑛 ) ⊆ ( 𝐹𝑀 ) ↔ ( 𝐹𝑁 ) ⊆ ( 𝐹𝑀 ) ) )
25 24 imbi2d ( 𝑛 = 𝑁 → ( ( 𝜑 → ( 𝐹𝑛 ) ⊆ ( 𝐹𝑀 ) ) ↔ ( 𝜑 → ( 𝐹𝑁 ) ⊆ ( 𝐹𝑀 ) ) ) )
26 ssidd ( 𝜑 → ( 𝐹𝑀 ) ⊆ ( 𝐹𝑀 ) )
27 26 a1i ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀𝑁 ) → ( 𝜑 → ( 𝐹𝑀 ) ⊆ ( 𝐹𝑀 ) ) )
28 simpr ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀𝑚𝑚 < 𝑁 ) ) ∧ 𝜑 ) → 𝜑 )
29 simplll ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀𝑚𝑚 < 𝑁 ) ) ∧ 𝜑 ) → 𝑀 ∈ ℤ )
30 simplr1 ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀𝑚𝑚 < 𝑁 ) ) ∧ 𝜑 ) → 𝑚 ∈ ℤ )
31 simplr2 ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀𝑚𝑚 < 𝑁 ) ) ∧ 𝜑 ) → 𝑀𝑚 )
32 29 30 31 3jca ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀𝑚𝑚 < 𝑁 ) ) ∧ 𝜑 ) → ( 𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀𝑚 ) )
33 eluz2 ( 𝑚 ∈ ( ℤ𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀𝑚 ) )
34 32 33 sylibr ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀𝑚𝑚 < 𝑁 ) ) ∧ 𝜑 ) → 𝑚 ∈ ( ℤ𝑀 ) )
35 simpllr ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀𝑚𝑚 < 𝑁 ) ) ∧ 𝜑 ) → 𝑁 ∈ ℤ )
36 simplr3 ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀𝑚𝑚 < 𝑁 ) ) ∧ 𝜑 ) → 𝑚 < 𝑁 )
37 34 35 36 3jca ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀𝑚𝑚 < 𝑁 ) ) ∧ 𝜑 ) → ( 𝑚 ∈ ( ℤ𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝑚 < 𝑁 ) )
38 elfzo2 ( 𝑚 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑚 ∈ ( ℤ𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝑚 < 𝑁 ) )
39 37 38 sylibr ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀𝑚𝑚 < 𝑁 ) ) ∧ 𝜑 ) → 𝑚 ∈ ( 𝑀 ..^ 𝑁 ) )
40 28 39 2 syl2anc ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀𝑚𝑚 < 𝑁 ) ) ∧ 𝜑 ) → ( 𝐹 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝐹𝑚 ) )
41 40 3adant2 ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀𝑚𝑚 < 𝑁 ) ) ∧ ( 𝜑 → ( 𝐹𝑚 ) ⊆ ( 𝐹𝑀 ) ) ∧ 𝜑 ) → ( 𝐹 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝐹𝑚 ) )
42 simpr ( ( ( 𝜑 → ( 𝐹𝑚 ) ⊆ ( 𝐹𝑀 ) ) ∧ 𝜑 ) → 𝜑 )
43 simpl ( ( ( 𝜑 → ( 𝐹𝑚 ) ⊆ ( 𝐹𝑀 ) ) ∧ 𝜑 ) → ( 𝜑 → ( 𝐹𝑚 ) ⊆ ( 𝐹𝑀 ) ) )
44 pm3.35 ( ( 𝜑 ∧ ( 𝜑 → ( 𝐹𝑚 ) ⊆ ( 𝐹𝑀 ) ) ) → ( 𝐹𝑚 ) ⊆ ( 𝐹𝑀 ) )
45 42 43 44 syl2anc ( ( ( 𝜑 → ( 𝐹𝑚 ) ⊆ ( 𝐹𝑀 ) ) ∧ 𝜑 ) → ( 𝐹𝑚 ) ⊆ ( 𝐹𝑀 ) )
46 45 3adant1 ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀𝑚𝑚 < 𝑁 ) ) ∧ ( 𝜑 → ( 𝐹𝑚 ) ⊆ ( 𝐹𝑀 ) ) ∧ 𝜑 ) → ( 𝐹𝑚 ) ⊆ ( 𝐹𝑀 ) )
47 41 46 sstrd ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀𝑚𝑚 < 𝑁 ) ) ∧ ( 𝜑 → ( 𝐹𝑚 ) ⊆ ( 𝐹𝑀 ) ) ∧ 𝜑 ) → ( 𝐹 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝐹𝑀 ) )
48 47 3exp ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀𝑚𝑚 < 𝑁 ) ) → ( ( 𝜑 → ( 𝐹𝑚 ) ⊆ ( 𝐹𝑀 ) ) → ( 𝜑 → ( 𝐹 ‘ ( 𝑚 + 1 ) ) ⊆ ( 𝐹𝑀 ) ) ) )
49 16 19 22 25 27 48 fzind ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀𝑁𝑁𝑁 ) ) → ( 𝜑 → ( 𝐹𝑁 ) ⊆ ( 𝐹𝑀 ) ) )
50 13 49 mpcom ( 𝜑 → ( 𝐹𝑁 ) ⊆ ( 𝐹𝑀 ) )