Theorem ssnn0ssfz

Description: For any finite subset of NN0 , find a superset in the form of a set of sequential integers, analogous to ssnnssfz . (Contributed by AV, 30-Sep-2019)

	Ref	Expression
Assertion	ssnn0ssfz	⊢ ( 𝐴 ∈ ( 𝒫 ℕ0 ∩ Fin ) → ∃ 𝑛 ∈ ℕ0 𝐴 ⊆ ( 0 ... 𝑛 ) )

Proof

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