Theorem suprfinzcl

Description: The supremum of a nonempty finite set of integers is a member of the set. (Contributed by AV, 1-Oct-2019)

	Ref	Expression
Assertion	suprfinzcl	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		zssre	⊢ ℤ ⊆ ℝ
2		ltso	⊢ < Or ℝ
3		soss	⊢ ( ℤ ⊆ ℝ → ( < Or ℝ → < Or ℤ ) )
4	1 2 3	mp2	⊢ < Or ℤ
5	4	a1i	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → < Or ℤ )
6		simp3	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → 𝐴 ∈ Fin )
7		simp2	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → 𝐴 ≠ ∅ )
8		simp1	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → 𝐴 ⊆ ℤ )
9		fisup2g	⊢ ( ( < Or ℤ ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐴 ⊆ ℤ ) ) → ∃ 𝑟 ∈ 𝐴 ( ∀ 𝑎 ∈ 𝐴 ¬ 𝑟 < 𝑎 ∧ ∀ 𝑎 ∈ ℤ ( 𝑎 < 𝑟 → ∃ 𝑏 ∈ 𝐴 𝑎 < 𝑏 ) ) )
10	5 6 7 8 9	syl13anc	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → ∃ 𝑟 ∈ 𝐴 ( ∀ 𝑎 ∈ 𝐴 ¬ 𝑟 < 𝑎 ∧ ∀ 𝑎 ∈ ℤ ( 𝑎 < 𝑟 → ∃ 𝑏 ∈ 𝐴 𝑎 < 𝑏 ) ) )
11		id	⊢ ( 𝐴 ⊆ ℤ → 𝐴 ⊆ ℤ )
12	11 1	sstrdi	⊢ ( 𝐴 ⊆ ℤ → 𝐴 ⊆ ℝ )
13	12	3ad2ant1	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → 𝐴 ⊆ ℝ )
14		ssrexv	⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑟 ∈ 𝐴 ( ∀ 𝑎 ∈ 𝐴 ¬ 𝑟 < 𝑎 ∧ ∀ 𝑎 ∈ ℤ ( 𝑎 < 𝑟 → ∃ 𝑏 ∈ 𝐴 𝑎 < 𝑏 ) ) → ∃ 𝑟 ∈ ℝ ( ∀ 𝑎 ∈ 𝐴 ¬ 𝑟 < 𝑎 ∧ ∀ 𝑎 ∈ ℤ ( 𝑎 < 𝑟 → ∃ 𝑏 ∈ 𝐴 𝑎 < 𝑏 ) ) ) )
15	13 14	syl	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → ( ∃ 𝑟 ∈ 𝐴 ( ∀ 𝑎 ∈ 𝐴 ¬ 𝑟 < 𝑎 ∧ ∀ 𝑎 ∈ ℤ ( 𝑎 < 𝑟 → ∃ 𝑏 ∈ 𝐴 𝑎 < 𝑏 ) ) → ∃ 𝑟 ∈ ℝ ( ∀ 𝑎 ∈ 𝐴 ¬ 𝑟 < 𝑎 ∧ ∀ 𝑎 ∈ ℤ ( 𝑎 < 𝑟 → ∃ 𝑏 ∈ 𝐴 𝑎 < 𝑏 ) ) ) )
16		ssel2	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ ℤ )
17	16	zred	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ ℝ )
18	17	ex	⊢ ( 𝐴 ⊆ ℤ → ( 𝑎 ∈ 𝐴 → 𝑎 ∈ ℝ ) )
19	18	3ad2ant1	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → ( 𝑎 ∈ 𝐴 → 𝑎 ∈ ℝ ) )
20	19	adantr	⊢ ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ∧ 𝑟 ∈ ℝ ) → ( 𝑎 ∈ 𝐴 → 𝑎 ∈ ℝ ) )
21	20	imp	⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ ℝ )
22		simplr	⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑎 ∈ 𝐴 ) → 𝑟 ∈ ℝ )
23	21 22	lenltd	⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 ≤ 𝑟 ↔ ¬ 𝑟 < 𝑎 ) )
24	23	bicomd	⊢ ( ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ∧ 𝑟 ∈ ℝ ) ∧ 𝑎 ∈ 𝐴 ) → ( ¬ 𝑟 < 𝑎 ↔ 𝑎 ≤ 𝑟 ) )
25	24	ralbidva	⊢ ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ∧ 𝑟 ∈ ℝ ) → ( ∀ 𝑎 ∈ 𝐴 ¬ 𝑟 < 𝑎 ↔ ∀ 𝑎 ∈ 𝐴 𝑎 ≤ 𝑟 ) )
26	25	biimpd	⊢ ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ∧ 𝑟 ∈ ℝ ) → ( ∀ 𝑎 ∈ 𝐴 ¬ 𝑟 < 𝑎 → ∀ 𝑎 ∈ 𝐴 𝑎 ≤ 𝑟 ) )
27	26	adantrd	⊢ ( ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ∧ 𝑟 ∈ ℝ ) → ( ( ∀ 𝑎 ∈ 𝐴 ¬ 𝑟 < 𝑎 ∧ ∀ 𝑎 ∈ ℤ ( 𝑎 < 𝑟 → ∃ 𝑏 ∈ 𝐴 𝑎 < 𝑏 ) ) → ∀ 𝑎 ∈ 𝐴 𝑎 ≤ 𝑟 ) )
28	27	reximdva	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → ( ∃ 𝑟 ∈ ℝ ( ∀ 𝑎 ∈ 𝐴 ¬ 𝑟 < 𝑎 ∧ ∀ 𝑎 ∈ ℤ ( 𝑎 < 𝑟 → ∃ 𝑏 ∈ 𝐴 𝑎 < 𝑏 ) ) → ∃ 𝑟 ∈ ℝ ∀ 𝑎 ∈ 𝐴 𝑎 ≤ 𝑟 ) )
29	15 28	syld	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → ( ∃ 𝑟 ∈ 𝐴 ( ∀ 𝑎 ∈ 𝐴 ¬ 𝑟 < 𝑎 ∧ ∀ 𝑎 ∈ ℤ ( 𝑎 < 𝑟 → ∃ 𝑏 ∈ 𝐴 𝑎 < 𝑏 ) ) → ∃ 𝑟 ∈ ℝ ∀ 𝑎 ∈ 𝐴 𝑎 ≤ 𝑟 ) )
30	10 29	mpd	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → ∃ 𝑟 ∈ ℝ ∀ 𝑎 ∈ 𝐴 𝑎 ≤ 𝑟 )
31		suprzcl	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑟 ∈ ℝ ∀ 𝑎 ∈ 𝐴 𝑎 ≤ 𝑟 ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )
32	30 31	syld3an3	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )