This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 ssinc.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 ssinc.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 id ⊢ ( 𝜑 → 𝜑 )
15 fveq2 ⊢ ( 𝑛 = 𝑀 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑀 ) )
16 15 sseq2d ⊢ ( 𝑛 = 𝑀 → ( ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑀 ) ) )
17 16 imbi2d ⊢ ( 𝑛 = 𝑀 → ( ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑛 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑀 ) ) ) )
18 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑚 ) )
19 18 sseq2d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑚 ) ) )
20 19 imbi2d ⊢ ( 𝑛 = 𝑚 → ( ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑛 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑚 ) ) ) )
21 fveq2 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑚 + 1 ) ) )
22 21 sseq2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) )
23 22 imbi2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑛 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) )
24 fveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑁 ) )
25 24 sseq2d ⊢ ( 𝑛 = 𝑁 → ( ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑁 ) ) )
26 25 imbi2d ⊢ ( 𝑛 = 𝑁 → ( ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑛 ) ) ↔ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑁 ) ) ) )
27 ssidd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑀 ) )
28 27 a1i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑀 ) ) )
29 simpr ⊢ ( ( ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑚 ) ) ∧ 𝜑 ) → 𝜑 )
30 simpl ⊢ ( ( ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑚 ) ) ∧ 𝜑 ) → ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑚 ) ) )
31 pm3.35 ⊢ ( ( 𝜑 ∧ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑚 ) ) ) → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑚 ) )
32 29 30 31 syl2anc ⊢ ( ( ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑚 ) ) ∧ 𝜑 ) → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑚 ) )
33 32 3adant1 ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) ∧ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑚 ) ) ∧ 𝜑 ) → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑚 ) )
34 simpr ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) ∧ 𝜑 ) → 𝜑 )
35 simplll ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) ∧ 𝜑 ) → 𝑀 ∈ ℤ )
36 simplr1 ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) ∧ 𝜑 ) → 𝑚 ∈ ℤ )
37 simplr2 ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) ∧ 𝜑 ) → 𝑀 ≤ 𝑚 )
38 35 36 37 3jca ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) ∧ 𝜑 ) → ( 𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ) )
39 eluz2 ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ) )
40 38 39 sylibr ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) ∧ 𝜑 ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) )
41 simpllr ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) ∧ 𝜑 ) → 𝑁 ∈ ℤ )
42 simplr3 ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) ∧ 𝜑 ) → 𝑚 < 𝑁 )
43 40 41 42 3jca ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) ∧ 𝜑 ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝑚 < 𝑁 ) )
44 elfzo2 ⊢ ( 𝑚 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝑚 < 𝑁 ) )
45 43 44 sylibr ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) ∧ 𝜑 ) → 𝑚 ∈ ( 𝑀 ..^ 𝑁 ) )
46 34 45 2 syl2anc ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) ∧ 𝜑 ) → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ ( 𝑚 + 1 ) ) )
47 46 3adant2 ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) ∧ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑚 ) ) ∧ 𝜑 ) → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ ( 𝑚 + 1 ) ) )
48 33 47 sstrd ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) ∧ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑚 ) ) ∧ 𝜑 ) → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ ( 𝑚 + 1 ) ) )
49 48 3exp ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ≤ 𝑚 ∧ 𝑚 < 𝑁 ) ) → ( ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑚 ) ) → ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) )
50 17 20 23 26 28 49 fzind ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑁 ) ) → ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑁 ) ) )
51 13 14 50 sylc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ⊆ ( 𝐹 ‘ 𝑁 ) )