uzsupss

Description: Any bounded subset of an upper set of integers has a supremum. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 21-Apr-2015)

		Ref	Expression
	Hypothesis	uzsupss.1	$⊢ Z = ℤ_{\geq M}$
	Assertion	uzsupss	$⊢ (M \in ℤ \land A \subseteq Z \land \exists x \in ℤ \forall y \in A y \leq x) \to \exists x \in Z (\forall y \in A \neg x < y \land \forall y \in Z (y < x \to \exists z \in A y < z))$

Proof

Step	Hyp	Ref	Expression
1		uzsupss.1	$⊢ Z = ℤ_{\geq M}$
2		simpl1	$⊢ ((M \in ℤ \land A \subseteq Z \land \exists x \in ℤ \forall y \in A y \leq x) \land A = \emptyset) \to M \in ℤ$
3		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
4	2 3	syl	$⊢ ((M \in ℤ \land A \subseteq Z \land \exists x \in ℤ \forall y \in A y \leq x) \land A = \emptyset) \to M \in ℤ_{\geq M}$
5	4 1	eleqtrrdi	$⊢ ((M \in ℤ \land A \subseteq Z \land \exists x \in ℤ \forall y \in A y \leq x) \land A = \emptyset) \to M \in Z$
6		ral0	$⊢ \forall y \in \emptyset \neg M < y$
7		simpr	$⊢ ((M \in ℤ \land A \subseteq Z \land \exists x \in ℤ \forall y \in A y \leq x) \land A = \emptyset) \to A = \emptyset$
8	7	raleqdv	$⊢ ((M \in ℤ \land A \subseteq Z \land \exists x \in ℤ \forall y \in A y \leq x) \land A = \emptyset) \to (\forall y \in A \neg M < y \leftrightarrow \forall y \in \emptyset \neg M < y)$
9	6 8	mpbiri	$⊢ ((M \in ℤ \land A \subseteq Z \land \exists x \in ℤ \forall y \in A y \leq x) \land A = \emptyset) \to \forall y \in A \neg M < y$
10		eluzle	$⊢ y \in ℤ_{\geq M} \to M \leq y$
11		eluzel2	$⊢ y \in ℤ_{\geq M} \to M \in ℤ$
12		eluzelz	$⊢ y \in ℤ_{\geq M} \to y \in ℤ$
13		zre	$⊢ M \in ℤ \to M \in ℝ$
14		zre	$⊢ y \in ℤ \to y \in ℝ$
15		lenlt	$⊢ (M \in ℝ \land y \in ℝ) \to (M \leq y \leftrightarrow \neg y < M)$
16	13 14 15	syl2an	$⊢ (M \in ℤ \land y \in ℤ) \to (M \leq y \leftrightarrow \neg y < M)$
17	11 12 16	syl2anc	$⊢ y \in ℤ_{\geq M} \to (M \leq y \leftrightarrow \neg y < M)$
18	10 17	mpbid	$⊢ y \in ℤ_{\geq M} \to \neg y < M$
19	18 1	eleq2s	$⊢ y \in Z \to \neg y < M$
20	19	pm2.21d	$⊢ y \in Z \to (y < M \to \exists z \in A y < z)$
21	20	rgen	$⊢ \forall y \in Z (y < M \to \exists z \in A y < z)$
22	21	a1i	$⊢ ((M \in ℤ \land A \subseteq Z \land \exists x \in ℤ \forall y \in A y \leq x) \land A = \emptyset) \to \forall y \in Z (y < M \to \exists z \in A y < z)$
23		breq1	$⊢ x = M \to (x < y \leftrightarrow M < y)$
24	23	notbid	$⊢ x = M \to (\neg x < y \leftrightarrow \neg M < y)$
25	24	ralbidv	$⊢ x = M \to (\forall y \in A \neg x < y \leftrightarrow \forall y \in A \neg M < y)$
26		breq2	$⊢ x = M \to (y < x \leftrightarrow y < M)$
27	26	imbi1d	$⊢ x = M \to ((y < x \to \exists z \in A y < z) \leftrightarrow (y < M \to \exists z \in A y < z))$
28	27	ralbidv	$⊢ x = M \to (\forall y \in Z (y < x \to \exists z \in A y < z) \leftrightarrow \forall y \in Z (y < M \to \exists z \in A y < z))$
29	25 28	anbi12d	$⊢ x = M \to ((\forall y \in A \neg x < y \land \forall y \in Z (y < x \to \exists z \in A y < z)) \leftrightarrow (\forall y \in A \neg M < y \land \forall y \in Z (y < M \to \exists z \in A y < z)))$
30	29	rspcev	$⊢ (M \in Z \land (\forall y \in A \neg M < y \land \forall y \in Z (y < M \to \exists z \in A y < z))) \to \exists x \in Z (\forall y \in A \neg x < y \land \forall y \in Z (y < x \to \exists z \in A y < z))$
31	5 9 22 30	syl12anc	$⊢ ((M \in ℤ \land A \subseteq Z \land \exists x \in ℤ \forall y \in A y \leq x) \land A = \emptyset) \to \exists x \in Z (\forall y \in A \neg x < y \land \forall y \in Z (y < x \to \exists z \in A y < z))$
32		simpl2	$⊢ ((M \in ℤ \land A \subseteq Z \land \exists x \in ℤ \forall y \in A y \leq x) \land A \neq \emptyset) \to A \subseteq Z$
33		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
34	1 33	eqsstri	$⊢ Z \subseteq ℤ$
35	32 34	sstrdi	$⊢ ((M \in ℤ \land A \subseteq Z \land \exists x \in ℤ \forall y \in A y \leq x) \land A \neq \emptyset) \to A \subseteq ℤ$
36		simpr	$⊢ ((M \in ℤ \land A \subseteq Z \land \exists x \in ℤ \forall y \in A y \leq x) \land A \neq \emptyset) \to A \neq \emptyset$
37		simpl3	$⊢ ((M \in ℤ \land A \subseteq Z \land \exists x \in ℤ \forall y \in A y \leq x) \land A \neq \emptyset) \to \exists x \in ℤ \forall y \in A y \leq x$
38		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 Z (y < x \to \exists z \in A y < z))$
39	35 36 37 38	syl3anc	$⊢ ((M \in ℤ \land A \subseteq Z \land \exists x \in ℤ \forall y \in A y \leq x) \land A \neq \emptyset) \to \exists x \in A (\forall y \in A \neg x < y \land \forall y \in Z (y < x \to \exists z \in A y < z))$
40		ssrexv	$⊢ A \subseteq Z \to (\exists x \in A (\forall y \in A \neg x < y \land \forall y \in Z (y < x \to \exists z \in A y < z)) \to \exists x \in Z (\forall y \in A \neg x < y \land \forall y \in Z (y < x \to \exists z \in A y < z)))$
41	32 39 40	sylc	$⊢ ((M \in ℤ \land A \subseteq Z \land \exists x \in ℤ \forall y \in A y \leq x) \land A \neq \emptyset) \to \exists x \in Z (\forall y \in A \neg x < y \land \forall y \in Z (y < x \to \exists z \in A y < z))$
42	31 41	pm2.61dane	$⊢ (M \in ℤ \land A \subseteq Z \land \exists x \in ℤ \forall y \in A y \leq x) \to \exists x \in Z (\forall y \in A \neg x < y \land \forall y \in Z (y < x \to \exists z \in A y < z))$

Metamath Proof Explorer

Theorem uzsupss

Proof