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