Metamath Proof Explorer

Theorem suprzub

Description: The supremum of a bounded-above set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015)

		Ref	Expression
	Assertion	suprzub	$⊢ (A \subseteq ℤ \land \exists x \in ℤ \forall y \in A y \leq x \land B \in A) \to B \leq sup (A ℝ <)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \subseteq ℤ \land \exists x \in ℤ \forall y \in A y \leq x \land B \in A) \to A \subseteq ℤ$
2		zssre	$⊢ ℤ \subseteq ℝ$
3	1 2	sstrdi	$⊢ (A \subseteq ℤ \land \exists x \in ℤ \forall y \in A y \leq x \land B \in A) \to A \subseteq ℝ$
4		simp3	$⊢ (A \subseteq ℤ \land \exists x \in ℤ \forall y \in A y \leq x \land B \in A) \to B \in A$
5	3 4	sseldd	$⊢ (A \subseteq ℤ \land \exists x \in ℤ \forall y \in A y \leq x \land B \in A) \to B \in ℝ$
6	4	ne0d	$⊢ (A \subseteq ℤ \land \exists x \in ℤ \forall y \in A y \leq x \land B \in A) \to A \neq \emptyset$
7		simp2	$⊢ (A \subseteq ℤ \land \exists x \in ℤ \forall y \in A y \leq x \land B \in A) \to \exists x \in ℤ \forall y \in A y \leq x$
8		suprzcl2	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land \exists x \in ℤ \forall y \in A y \leq x) \to sup (A ℝ <) \in A$
9	1 6 7 8	syl3anc	$⊢ (A \subseteq ℤ \land \exists x \in ℤ \forall y \in A y \leq x \land B \in A) \to sup (A ℝ <) \in A$
10	3 9	sseldd	$⊢ (A \subseteq ℤ \land \exists x \in ℤ \forall y \in A y \leq x \land B \in A) \to sup (A ℝ <) \in ℝ$
11		ltso	$⊢ < Or ℝ$
12	11	a1i	$⊢ (A \subseteq ℤ \land \exists x \in ℤ \forall y \in A y \leq x \land B \in A) \to < Or ℝ$
13		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))$
14	1 6 7 13	syl3anc	$⊢ (A \subseteq ℤ \land \exists x \in ℤ \forall y \in A y \leq x \land B \in A) \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))$
15		ssrexv	$⊢ 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 \exists x \in ℝ (\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z)))$
16	3 14 15	sylc	$⊢ (A \subseteq ℤ \land \exists x \in ℤ \forall y \in A y \leq x \land B \in A) \to \exists x \in ℝ (\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z))$
17	12 16	supub	$⊢ (A \subseteq ℤ \land \exists x \in ℤ \forall y \in A y \leq x \land B \in A) \to (B \in A \to \neg sup (A ℝ <) < B)$
18	4 17	mpd	$⊢ (A \subseteq ℤ \land \exists x \in ℤ \forall y \in A y \leq x \land B \in A) \to \neg sup (A ℝ <) < B$
19	5 10 18	nltled	$⊢ (A \subseteq ℤ \land \exists x \in ℤ \forall y \in A y \leq x \land B \in A) \to B \leq sup (A ℝ <)$