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	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℤ \forall y \in A y \leq x) \to sup (A ℝ <) \in A$

Proof

Step	Hyp	Ref	Expression
1		zsupss	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℤ \forall y \in A y \leq x) \to \exists x \in A (\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z))$
2		ssel2	$⊢ (A \subseteq ℤ \land x \in A) \to x \in ℤ$
3	2	zred	$⊢ (A \subseteq ℤ \land x \in A) \to x \in ℝ$
4		ltso	$⊢ < Or ℝ$
5	4	a1i	$⊢ ⊤ \to < Or ℝ$
6	5	eqsup	$⊢ ⊤ \to ((x \in ℝ \land \forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z)) \to sup (A ℝ <) = x)$
7	6	mptru	$⊢ (x \in ℝ \land \forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z)) \to sup (A ℝ <) = x$
8	7	3expib	$⊢ x \in ℝ \to ((\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z)) \to sup (A ℝ <) = x)$
9	3 8	syl	$⊢ (A \subseteq ℤ \land x \in A) \to ((\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z)) \to sup (A ℝ <) = x)$
10		simpr	$⊢ (A \subseteq ℤ \land x \in A) \to x \in A$
11		eleq1	$⊢ sup (A ℝ <) = x \to (sup (A ℝ <) \in A \leftrightarrow x \in A)$
12	10 11	syl5ibrcom	$⊢ (A \subseteq ℤ \land x \in A) \to (sup (A ℝ <) = x \to sup (A ℝ <) \in A)$
13	9 12	syld	$⊢ (A \subseteq ℤ \land x \in A) \to ((\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z)) \to sup (A ℝ <) \in A)$
14	13	rexlimdva	$⊢ A \subseteq ℤ \to (\exists x \in A (\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z)) \to sup (A ℝ <) \in A)$
15	14	3ad2ant1	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℤ \forall y \in A y \leq x) \to (\exists x \in A (\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z)) \to sup (A ℝ <) \in A)$
16	1 15	mpd	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℤ \forall y \in A y \leq x) \to sup (A ℝ <) \in A$