Metamath Proof Explorer

Theorem uzfissfz

Description: For any finite subset of the upper integers, there is a finite set of sequential integers that includes it. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses uzfissfz.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
uzfissfz.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
uzfissfz.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑍 )
uzfissfz.fi ⊢ ( 𝜑 → 𝐴 ∈ Fin )
Assertion uzfissfz ( 𝜑 → ∃ 𝑘 ∈ 𝑍 𝐴 ⊆ ( 𝑀 ... 𝑘 ) )

Proof

Step Hyp Ref Expression
1 uzfissfz.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 uzfissfz.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 uzfissfz.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑍 )
4 uzfissfz.fi ⊢ ( 𝜑 → 𝐴 ∈ Fin )
5 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
6 1 5 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
7 2 a1i ⊢ ( 𝜑 → 𝑍 = ( ℤ≥ ‘ 𝑀 ) )
8 7 eqcomd ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑀 ) = 𝑍 )
9 6 8 eleqtrd ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝑀 ∈ 𝑍 )
11 id ⊢ ( 𝐴 = ∅ → 𝐴 = ∅ )
12 0ss ⊢ ∅ ⊆ ( 𝑀 ... 𝑀 )
13 12 a1i ⊢ ( 𝐴 = ∅ → ∅ ⊆ ( 𝑀 ... 𝑀 ) )
14 11 13 eqsstrd ⊢ ( 𝐴 = ∅ → 𝐴 ⊆ ( 𝑀 ... 𝑀 ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝐴 ⊆ ( 𝑀 ... 𝑀 ) )
16 oveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝑀 ... 𝑘 ) = ( 𝑀 ... 𝑀 ) )
17 16 sseq2d ⊢ ( 𝑘 = 𝑀 → ( 𝐴 ⊆ ( 𝑀 ... 𝑘 ) ↔ 𝐴 ⊆ ( 𝑀 ... 𝑀 ) ) )
18 17 rspcev ⊢ ( ( 𝑀 ∈ 𝑍 ∧ 𝐴 ⊆ ( 𝑀 ... 𝑀 ) ) → ∃ 𝑘 ∈ 𝑍 𝐴 ⊆ ( 𝑀 ... 𝑘 ) )
19 10 15 18 syl2anc ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ∃ 𝑘 ∈ 𝑍 𝐴 ⊆ ( 𝑀 ... 𝑘 ) )
20 3 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝐴 ⊆ 𝑍 )
21 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
22 2 21 eqsstri ⊢ 𝑍 ⊆ ℤ
23 22 a1i ⊢ ( 𝜑 → 𝑍 ⊆ ℤ )
24 3 23 sstrd ⊢ ( 𝜑 → 𝐴 ⊆ ℤ )
25 24 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝐴 ⊆ ℤ )
26 11 necon3bi ⊢ ( ¬ 𝐴 = ∅ → 𝐴 ≠ ∅ )
27 26 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝐴 ≠ ∅ )
28 4 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝐴 ∈ Fin )
29 suprfinzcl ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )
30 25 27 28 29 syl3anc ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )
31 20 30 sseldd ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → sup ( 𝐴 , ℝ , < ) ∈ 𝑍 )
32 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑀 ∈ ℤ )
33 22 31 sseldi ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → sup ( 𝐴 , ℝ , < ) ∈ ℤ )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → sup ( 𝐴 , ℝ , < ) ∈ ℤ )
35 25 sselda ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ ℤ )
36 32 34 35 3jca ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝑀 ∈ ℤ ∧ sup ( 𝐴 , ℝ , < ) ∈ ℤ ∧ 𝑗 ∈ ℤ ) )
37 3 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ 𝑍 )
38 2 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑍 = ( ℤ≥ ‘ 𝑀 ) )
39 37 38 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
40 eluzle ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑗 )
41 39 40 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑀 ≤ 𝑗 )
42 41 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑀 ≤ 𝑗 )
43 zssre ⊢ ℤ ⊆ ℝ
44 24 43 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
45 44 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → 𝐴 ⊆ ℝ )
46 27 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → 𝐴 ≠ ∅ )
47 fimaxre2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
48 44 4 47 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
50 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ 𝐴 )
51 suprub ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ≤ sup ( 𝐴 , ℝ , < ) )
52 45 46 49 50 51 syl31anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ≤ sup ( 𝐴 , ℝ , < ) )
53 36 42 52 jca32 ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑀 ∈ ℤ ∧ sup ( 𝐴 , ℝ , < ) ∈ ℤ ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ sup ( 𝐴 , ℝ , < ) ) ) )
54 elfz2 ⊢ ( 𝑗 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ sup ( 𝐴 , ℝ , < ) ∈ ℤ ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ sup ( 𝐴 , ℝ , < ) ) ) )
55 53 54 sylibr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
56 55 ralrimiva ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ∀ 𝑗 ∈ 𝐴 𝑗 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
57 dfss3 ⊢ ( 𝐴 ⊆ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ↔ ∀ 𝑗 ∈ 𝐴 𝑗 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
58 56 57 sylibr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝐴 ⊆ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
59 oveq2 ⊢ ( 𝑘 = sup ( 𝐴 , ℝ , < ) → ( 𝑀 ... 𝑘 ) = ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
60 59 sseq2d ⊢ ( 𝑘 = sup ( 𝐴 , ℝ , < ) → ( 𝐴 ⊆ ( 𝑀 ... 𝑘 ) ↔ 𝐴 ⊆ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ) )
61 60 rspcev ⊢ ( ( sup ( 𝐴 , ℝ , < ) ∈ 𝑍 ∧ 𝐴 ⊆ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ) → ∃ 𝑘 ∈ 𝑍 𝐴 ⊆ ( 𝑀 ... 𝑘 ) )
62 31 58 61 syl2anc ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ∃ 𝑘 ∈ 𝑍 𝐴 ⊆ ( 𝑀 ... 𝑘 ) )
63 19 62 pm2.61dan ⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 𝐴 ⊆ ( 𝑀 ... 𝑘 ) )