This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝐴 , ℝ , < ) ∈ 𝐴 )