zsupss

Description: Any nonempty bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-sup .) (Contributed by Mario Carneiro, 21-Apr-2015)

		Ref	Expression
	Assertion	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 B (y < x \to \exists z \in A y < z))$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ y = m \to (y \leq x \leftrightarrow m \leq x)$
2	1	cbvralvw	$⊢ \forall y \in A y \leq x \leftrightarrow \forall m \in A m \leq x$
3		breq2	$⊢ x = n \to (m \leq x \leftrightarrow m \leq n)$
4	3	ralbidv	$⊢ x = n \to (\forall m \in A m \leq x \leftrightarrow \forall m \in A m \leq n)$
5	2 4	bitrid	$⊢ x = n \to (\forall y \in A y \leq x \leftrightarrow \forall m \in A m \leq n)$
6	5	cbvrexvw	$⊢ \exists x \in ℤ \forall y \in A y \leq x \leftrightarrow \exists n \in ℤ \forall m \in A m \leq n$
7		simp1rl	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land w \in ℤ \land - w \in A) \to n \in ℤ$
8	7	znegcld	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land w \in ℤ \land - w \in A) \to - n \in ℤ$
9		simp2	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land w \in ℤ \land - w \in A) \to w \in ℤ$
10	9	zred	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land w \in ℤ \land - w \in A) \to w \in ℝ$
11	7	zred	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land w \in ℤ \land - w \in A) \to n \in ℝ$
12		breq1	$⊢ m = - w \to (m \leq n \leftrightarrow - w \leq n)$
13		simp1rr	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land w \in ℤ \land - w \in A) \to \forall m \in A m \leq n$
14		simp3	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land w \in ℤ \land - w \in A) \to - w \in A$
15	12 13 14	rspcdva	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land w \in ℤ \land - w \in A) \to - w \leq n$
16	10 11 15	lenegcon1d	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land w \in ℤ \land - w \in A) \to - n \leq w$
17		eluz2	$⊢ w \in ℤ_{\geq (- n)} \leftrightarrow (- n \in ℤ \land w \in ℤ \land - n \leq w)$
18	8 9 16 17	syl3anbrc	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land w \in ℤ \land - w \in A) \to w \in ℤ_{\geq (- n)}$
19	18	rabssdv	$⊢ ((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \to \{w \in ℤ \| - w \in A\} \subseteq ℤ_{\geq (- n)}$
20		n0	$⊢ A \neq \emptyset \leftrightarrow \exists n n \in A$
21		ssel2	$⊢ (A \subseteq ℤ \land n \in A) \to n \in ℤ$
22	21	znegcld	$⊢ (A \subseteq ℤ \land n \in A) \to - n \in ℤ$
23	21	zcnd	$⊢ (A \subseteq ℤ \land n \in A) \to n \in ℂ$
24	23	negnegd	$⊢ (A \subseteq ℤ \land n \in A) \to - (- n) = n$
25		simpr	$⊢ (A \subseteq ℤ \land n \in A) \to n \in A$
26	24 25	eqeltrd	$⊢ (A \subseteq ℤ \land n \in A) \to - (- n) \in A$
27		negeq	$⊢ w = - n \to - w = - (- n)$
28	27	eleq1d	$⊢ w = - n \to (- w \in A \leftrightarrow - (- n) \in A)$
29	28	rspcev	$⊢ (- n \in ℤ \land - (- n) \in A) \to \exists w \in ℤ - w \in A$
30	22 26 29	syl2anc	$⊢ (A \subseteq ℤ \land n \in A) \to \exists w \in ℤ - w \in A$
31	30	ex	$⊢ A \subseteq ℤ \to (n \in A \to \exists w \in ℤ - w \in A)$
32	31	exlimdv	$⊢ A \subseteq ℤ \to (\exists n n \in A \to \exists w \in ℤ - w \in A)$
33	32	imp	$⊢ (A \subseteq ℤ \land \exists n n \in A) \to \exists w \in ℤ - w \in A$
34	20 33	sylan2b	$⊢ (A \subseteq ℤ \land A \neq \emptyset) \to \exists w \in ℤ - w \in A$
35	34	adantr	$⊢ ((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \to \exists w \in ℤ - w \in A$
36		rabn0	$⊢ \{w \in ℤ \| - w \in A\} \neq \emptyset \leftrightarrow \exists w \in ℤ - w \in A$
37	35 36	sylibr	$⊢ ((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \to \{w \in ℤ \| - w \in A\} \neq \emptyset$
38		infssuzcl	$⊢ (\{w \in ℤ \| - w \in A\} \subseteq ℤ_{\geq (- n)} \land \{w \in ℤ \| - w \in A\} \neq \emptyset) \to sup (\{w \in ℤ \| - w \in A\} ℝ <) \in \{w \in ℤ \| - w \in A\}$
39	19 37 38	syl2anc	$⊢ ((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \to sup (\{w \in ℤ \| - w \in A\} ℝ <) \in \{w \in ℤ \| - w \in A\}$
40		negeq	$⊢ n = sup (\{w \in ℤ \| - w \in A\} ℝ <) \to - n = - sup (\{w \in ℤ \| - w \in A\} ℝ <)$
41	40	eleq1d	$⊢ n = sup (\{w \in ℤ \| - w \in A\} ℝ <) \to (- n \in A \leftrightarrow - sup (\{w \in ℤ \| - w \in A\} ℝ <) \in A)$
42		negeq	$⊢ w = n \to - w = - n$
43	42	eleq1d	$⊢ w = n \to (- w \in A \leftrightarrow - n \in A)$
44	43	cbvrabv	$⊢ \{w \in ℤ \| - w \in A\} = \{n \in ℤ \| - n \in A\}$
45	41 44	elrab2	$⊢ sup (\{w \in ℤ \| - w \in A\} ℝ <) \in \{w \in ℤ \| - w \in A\} \leftrightarrow (sup (\{w \in ℤ \| - w \in A\} ℝ <) \in ℤ \land - sup (\{w \in ℤ \| - w \in A\} ℝ <) \in A)$
46	45	simprbi	$⊢ sup (\{w \in ℤ \| - w \in A\} ℝ <) \in \{w \in ℤ \| - w \in A\} \to - sup (\{w \in ℤ \| - w \in A\} ℝ <) \in A$
47	39 46	syl	$⊢ ((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \to - sup (\{w \in ℤ \| - w \in A\} ℝ <) \in A$
48		simpll	$⊢ ((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \to A \subseteq ℤ$
49	48	sselda	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to y \in ℤ$
50	49	zred	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to y \in ℝ$
51		ssrab2	$⊢ \{w \in ℤ \| - w \in A\} \subseteq ℤ$
52	39	adantr	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to sup (\{w \in ℤ \| - w \in A\} ℝ <) \in \{w \in ℤ \| - w \in A\}$
53	51 52	sselid	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to sup (\{w \in ℤ \| - w \in A\} ℝ <) \in ℤ$
54	53	znegcld	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to - sup (\{w \in ℤ \| - w \in A\} ℝ <) \in ℤ$
55	54	zred	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to - sup (\{w \in ℤ \| - w \in A\} ℝ <) \in ℝ$
56	53	zred	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to sup (\{w \in ℤ \| - w \in A\} ℝ <) \in ℝ$
57	19	adantr	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to \{w \in ℤ \| - w \in A\} \subseteq ℤ_{\geq (- n)}$
58		negeq	$⊢ w = - y \to - w = - (- y)$
59	58	eleq1d	$⊢ w = - y \to (- w \in A \leftrightarrow - (- y) \in A)$
60	49	znegcld	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to - y \in ℤ$
61	49	zcnd	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to y \in ℂ$
62	61	negnegd	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to - (- y) = y$
63		simpr	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to y \in A$
64	62 63	eqeltrd	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to - (- y) \in A$
65	59 60 64	elrabd	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to - y \in \{w \in ℤ \| - w \in A\}$
66		infssuzle	$⊢ (\{w \in ℤ \| - w \in A\} \subseteq ℤ_{\geq (- n)} \land - y \in \{w \in ℤ \| - w \in A\}) \to sup (\{w \in ℤ \| - w \in A\} ℝ <) \leq - y$
67	57 65 66	syl2anc	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to sup (\{w \in ℤ \| - w \in A\} ℝ <) \leq - y$
68	56 50 67	lenegcon2d	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to y \leq - sup (\{w \in ℤ \| - w \in A\} ℝ <)$
69	50 55 68	lensymd	$⊢ (((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \land y \in A) \to \neg - sup (\{w \in ℤ \| - w \in A\} ℝ <) < y$
70	69	ralrimiva	$⊢ ((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \to \forall y \in A \neg - sup (\{w \in ℤ \| - w \in A\} ℝ <) < y$
71		breq2	$⊢ z = - sup (\{w \in ℤ \| - w \in A\} ℝ <) \to (y < z \leftrightarrow y < - sup (\{w \in ℤ \| - w \in A\} ℝ <))$
72	71	rspcev	$⊢ (- sup (\{w \in ℤ \| - w \in A\} ℝ <) \in A \land y < - sup (\{w \in ℤ \| - w \in A\} ℝ <)) \to \exists z \in A y < z$
73	72	ex	$⊢ - sup (\{w \in ℤ \| - w \in A\} ℝ <) \in A \to (y < - sup (\{w \in ℤ \| - w \in A\} ℝ <) \to \exists z \in A y < z)$
74	47 73	syl	$⊢ ((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \to (y < - sup (\{w \in ℤ \| - w \in A\} ℝ <) \to \exists z \in A y < z)$
75	74	ralrimivw	$⊢ ((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \to \forall y \in B (y < - sup (\{w \in ℤ \| - w \in A\} ℝ <) \to \exists z \in A y < z)$
76		breq1	$⊢ x = - sup (\{w \in ℤ \| - w \in A\} ℝ <) \to (x < y \leftrightarrow - sup (\{w \in ℤ \| - w \in A\} ℝ <) < y)$
77	76	notbid	$⊢ x = - sup (\{w \in ℤ \| - w \in A\} ℝ <) \to (\neg x < y \leftrightarrow \neg - sup (\{w \in ℤ \| - w \in A\} ℝ <) < y)$
78	77	ralbidv	$⊢ x = - sup (\{w \in ℤ \| - w \in A\} ℝ <) \to (\forall y \in A \neg x < y \leftrightarrow \forall y \in A \neg - sup (\{w \in ℤ \| - w \in A\} ℝ <) < y)$
79		breq2	$⊢ x = - sup (\{w \in ℤ \| - w \in A\} ℝ <) \to (y < x \leftrightarrow y < - sup (\{w \in ℤ \| - w \in A\} ℝ <))$
80	79	imbi1d	$⊢ x = - sup (\{w \in ℤ \| - w \in A\} ℝ <) \to ((y < x \to \exists z \in A y < z) \leftrightarrow (y < - sup (\{w \in ℤ \| - w \in A\} ℝ <) \to \exists z \in A y < z))$
81	80	ralbidv	$⊢ x = - sup (\{w \in ℤ \| - w \in A\} ℝ <) \to (\forall y \in B (y < x \to \exists z \in A y < z) \leftrightarrow \forall y \in B (y < - sup (\{w \in ℤ \| - w \in A\} ℝ <) \to \exists z \in A y < z))$
82	78 81	anbi12d	$⊢ x = - sup (\{w \in ℤ \| - w \in A\} ℝ <) \to ((\forall y \in A \neg x < y \land \forall y \in B (y < x \to \exists z \in A y < z)) \leftrightarrow (\forall y \in A \neg - sup (\{w \in ℤ \| - w \in A\} ℝ <) < y \land \forall y \in B (y < - sup (\{w \in ℤ \| - w \in A\} ℝ <) \to \exists z \in A y < z)))$
83	82	rspcev	$⊢ (- sup (\{w \in ℤ \| - w \in A\} ℝ <) \in A \land (\forall y \in A \neg - sup (\{w \in ℤ \| - w \in A\} ℝ <) < y \land \forall y \in B (y < - sup (\{w \in ℤ \| - w \in A\} ℝ <) \to \exists z \in A y < z))) \to \exists x \in A (\forall y \in A \neg x < y \land \forall y \in B (y < x \to \exists z \in A y < z))$
84	47 70 75 83	syl12anc	$⊢ ((A \subseteq ℤ \land A \neq \emptyset) \land (n \in ℤ \land \forall m \in A m \leq n)) \to \exists x \in A (\forall y \in A \neg x < y \land \forall y \in B (y < x \to \exists z \in A y < z))$
85	84	rexlimdvaa	$⊢ (A \subseteq ℤ \land A \neq \emptyset) \to (\exists n \in ℤ \forall m \in A m \leq n \to \exists x \in A (\forall y \in A \neg x < y \land \forall y \in B (y < x \to \exists z \in A y < z)))$
86	6 85	biimtrid	$⊢ (A \subseteq ℤ \land A \neq \emptyset) \to (\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 B (y < x \to \exists z \in A y < z)))$
87	86	3impia	$⊢ (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 B (y < x \to \exists z \in A y < z))$

Metamath Proof Explorer

Theorem zsupss

Proof