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 ... 𝑛 ) )