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

Metamath Proof Explorer

Theorem suprzcl2

Description: The supremum of a bounded-above set of integers is a member of the set. (This version of suprzcl avoids ax-pre-sup .) (Contributed by Mario Carneiro, 21-Apr-2015) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion suprzcl2 ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 zsupss ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
2 ssel2 ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℤ )
3 2 zred ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
4 ltso ⊢ < Or ℝ
5 4 a1i ⊢ ( ⊤ → < Or ℝ )
6 5 eqsup ⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) → sup ( 𝐴 , ℝ , < ) = 𝑥 ) )
7 6 mptru ⊢ ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) → sup ( 𝐴 , ℝ , < ) = 𝑥 )
8 7 3expib ⊢ ( 𝑥 ∈ ℝ → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) → sup ( 𝐴 , ℝ , < ) = 𝑥 ) )
9 3 8 syl ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝑥 ∈ 𝐴 ) → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) → sup ( 𝐴 , ℝ , < ) = 𝑥 ) )
10 simpr ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
11 eleq1 ⊢ ( sup ( 𝐴 , ℝ , < ) = 𝑥 → ( sup ( 𝐴 , ℝ , < ) ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
12 10 11 syl5ibrcom ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝑥 ∈ 𝐴 ) → ( sup ( 𝐴 , ℝ , < ) = 𝑥 → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 ) )
13 9 12 syld ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝑥 ∈ 𝐴 ) → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 ) )
14 13 rexlimdva ⊢ ( 𝐴 ⊆ ℤ → ( ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 ) )
15 14 3ad2ant1 ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → ( ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 ) )
16 1 15 mpd ⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )