Metamath Proof Explorer


Theorem ssnnssfz

Description: For any finite subset of NN , find a superset in the form of a set of sequential integers. (Contributed by Thierry Arnoux, 13-Sep-2017)

Ref Expression
Assertion ssnnssfz ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) → ∃ 𝑛 ∈ ℕ 𝐴 ⊆ ( 1 ... 𝑛 ) )

Proof

Step Hyp Ref Expression
1 1nn 1 ∈ ℕ
2 simpr ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 = ∅ ) → 𝐴 = ∅ )
3 0ss ∅ ⊆ ( 1 ... 1 )
4 2 3 eqsstrdi ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 = ∅ ) → 𝐴 ⊆ ( 1 ... 1 ) )
5 oveq2 ( 𝑛 = 1 → ( 1 ... 𝑛 ) = ( 1 ... 1 ) )
6 5 sseq2d ( 𝑛 = 1 → ( 𝐴 ⊆ ( 1 ... 𝑛 ) ↔ 𝐴 ⊆ ( 1 ... 1 ) ) )
7 6 rspcev ( ( 1 ∈ ℕ ∧ 𝐴 ⊆ ( 1 ... 1 ) ) → ∃ 𝑛 ∈ ℕ 𝐴 ⊆ ( 1 ... 𝑛 ) )
8 1 4 7 sylancr ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 = ∅ ) → ∃ 𝑛 ∈ ℕ 𝐴 ⊆ ( 1 ... 𝑛 ) )
9 elin ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ↔ ( 𝐴 ∈ 𝒫 ℕ ∧ 𝐴 ∈ Fin ) )
10 9 simplbi ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) → 𝐴 ∈ 𝒫 ℕ )
11 10 adantr ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ∈ 𝒫 ℕ )
12 11 elpwid ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ⊆ ℕ )
13 nnssre ℕ ⊆ ℝ
14 ltso < Or ℝ
15 soss ( ℕ ⊆ ℝ → ( < Or ℝ → < Or ℕ ) )
16 13 14 15 mp2 < Or ℕ
17 16 a1i ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) → < Or ℕ )
18 9 simprbi ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) → 𝐴 ∈ Fin )
19 18 adantr ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ∈ Fin )
20 simpr ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
21 fisupcl ( ( < Or ℕ ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐴 ⊆ ℕ ) ) → sup ( 𝐴 , ℕ , < ) ∈ 𝐴 )
22 17 19 20 12 21 syl13anc ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) → sup ( 𝐴 , ℕ , < ) ∈ 𝐴 )
23 12 22 sseldd ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) → sup ( 𝐴 , ℕ , < ) ∈ ℕ )
24 12 sselda ( ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → 𝑥 ∈ ℕ )
25 nnuz ℕ = ( ℤ ‘ 1 )
26 24 25 eleqtrdi ( ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → 𝑥 ∈ ( ℤ ‘ 1 ) )
27 24 nnzd ( ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → 𝑥 ∈ ℤ )
28 12 adantr ( ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → 𝐴 ⊆ ℕ )
29 22 adantr ( ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → sup ( 𝐴 , ℕ , < ) ∈ 𝐴 )
30 28 29 sseldd ( ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → sup ( 𝐴 , ℕ , < ) ∈ ℕ )
31 30 nnzd ( ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → sup ( 𝐴 , ℕ , < ) ∈ ℤ )
32 fisup2g ( ( < Or ℕ ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐴 ⊆ ℕ ) ) → ∃ 𝑥𝐴 ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℕ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
33 17 19 20 12 32 syl13anc ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥𝐴 ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℕ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
34 ssrexv ( 𝐴 ⊆ ℕ → ( ∃ 𝑥𝐴 ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℕ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) → ∃ 𝑥 ∈ ℕ ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℕ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) ) )
35 12 33 34 sylc ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ ℕ ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℕ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
36 17 35 supub ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) → ( 𝑥𝐴 → ¬ sup ( 𝐴 , ℕ , < ) < 𝑥 ) )
37 36 imp ( ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → ¬ sup ( 𝐴 , ℕ , < ) < 𝑥 )
38 24 nnred ( ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → 𝑥 ∈ ℝ )
39 30 nnred ( ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → sup ( 𝐴 , ℕ , < ) ∈ ℝ )
40 38 39 lenltd ( ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → ( 𝑥 ≤ sup ( 𝐴 , ℕ , < ) ↔ ¬ sup ( 𝐴 , ℕ , < ) < 𝑥 ) )
41 37 40 mpbird ( ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → 𝑥 ≤ sup ( 𝐴 , ℕ , < ) )
42 eluz2 ( sup ( 𝐴 , ℕ , < ) ∈ ( ℤ𝑥 ) ↔ ( 𝑥 ∈ ℤ ∧ sup ( 𝐴 , ℕ , < ) ∈ ℤ ∧ 𝑥 ≤ sup ( 𝐴 , ℕ , < ) ) )
43 27 31 41 42 syl3anbrc ( ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → sup ( 𝐴 , ℕ , < ) ∈ ( ℤ𝑥 ) )
44 eluzfz ( ( 𝑥 ∈ ( ℤ ‘ 1 ) ∧ sup ( 𝐴 , ℕ , < ) ∈ ( ℤ𝑥 ) ) → 𝑥 ∈ ( 1 ... sup ( 𝐴 , ℕ , < ) ) )
45 26 43 44 syl2anc ( ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → 𝑥 ∈ ( 1 ... sup ( 𝐴 , ℕ , < ) ) )
46 45 ex ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) → ( 𝑥𝐴𝑥 ∈ ( 1 ... sup ( 𝐴 , ℕ , < ) ) ) )
47 46 ssrdv ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ⊆ ( 1 ... sup ( 𝐴 , ℕ , < ) ) )
48 oveq2 ( 𝑛 = sup ( 𝐴 , ℕ , < ) → ( 1 ... 𝑛 ) = ( 1 ... sup ( 𝐴 , ℕ , < ) ) )
49 48 sseq2d ( 𝑛 = sup ( 𝐴 , ℕ , < ) → ( 𝐴 ⊆ ( 1 ... 𝑛 ) ↔ 𝐴 ⊆ ( 1 ... sup ( 𝐴 , ℕ , < ) ) ) )
50 49 rspcev ( ( sup ( 𝐴 , ℕ , < ) ∈ ℕ ∧ 𝐴 ⊆ ( 1 ... sup ( 𝐴 , ℕ , < ) ) ) → ∃ 𝑛 ∈ ℕ 𝐴 ⊆ ( 1 ... 𝑛 ) )
51 23 47 50 syl2anc ( ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝐴 ≠ ∅ ) → ∃ 𝑛 ∈ ℕ 𝐴 ⊆ ( 1 ... 𝑛 ) )
52 8 51 pm2.61dane ( 𝐴 ∈ ( 𝒫 ℕ ∩ Fin ) → ∃ 𝑛 ∈ ℕ 𝐴 ⊆ ( 1 ... 𝑛 ) )