sup2

Description: A nonempty, bounded-above set of reals has a supremum. Stronger version of completeness axiom (it has a slightly weaker antecedent). (Contributed by NM, 19-Jan-1997)

		Ref	Expression
	Assertion	sup2	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A (y < x \lor y = x)) \to \exists x \in ℝ (\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z))$

Proof

Step	Hyp	Ref	Expression
1		peano2re	$⊢ x \in ℝ \to x + 1 \in ℝ$
2	1	adantr	$⊢ (x \in ℝ \land \forall y \in A (y < x \lor y = x)) \to x + 1 \in ℝ$
3	2	a1i	$⊢ A \subseteq ℝ \to ((x \in ℝ \land \forall y \in A (y < x \lor y = x)) \to x + 1 \in ℝ)$
4		ssel	$⊢ A \subseteq ℝ \to (y \in A \to y \in ℝ)$
5		ltp1	$⊢ x \in ℝ \to x < x + 1$
6	1	ancli	$⊢ x \in ℝ \to (x \in ℝ \land x + 1 \in ℝ)$
7		lttr	$⊢ (y \in ℝ \land x \in ℝ \land x + 1 \in ℝ) \to ((y < x \land x < x + 1) \to y < x + 1)$
8	7	3expb	$⊢ (y \in ℝ \land (x \in ℝ \land x + 1 \in ℝ)) \to ((y < x \land x < x + 1) \to y < x + 1)$
9	6 8	sylan2	$⊢ (y \in ℝ \land x \in ℝ) \to ((y < x \land x < x + 1) \to y < x + 1)$
10	5 9	sylan2i	$⊢ (y \in ℝ \land x \in ℝ) \to ((y < x \land x \in ℝ) \to y < x + 1)$
11	10	exp4b	$⊢ y \in ℝ \to (x \in ℝ \to (y < x \to (x \in ℝ \to y < x + 1)))$
12	11	com34	$⊢ y \in ℝ \to (x \in ℝ \to (x \in ℝ \to (y < x \to y < x + 1)))$
13	12	pm2.43d	$⊢ y \in ℝ \to (x \in ℝ \to (y < x \to y < x + 1))$
14	13	imp	$⊢ (y \in ℝ \land x \in ℝ) \to (y < x \to y < x + 1)$
15		breq1	$⊢ y = x \to (y < x + 1 \leftrightarrow x < x + 1)$
16	5 15	syl5ibrcom	$⊢ x \in ℝ \to (y = x \to y < x + 1)$
17	16	adantl	$⊢ (y \in ℝ \land x \in ℝ) \to (y = x \to y < x + 1)$
18	14 17	jaod	$⊢ (y \in ℝ \land x \in ℝ) \to ((y < x \lor y = x) \to y < x + 1)$
19	18	ex	$⊢ y \in ℝ \to (x \in ℝ \to ((y < x \lor y = x) \to y < x + 1))$
20	4 19	syl6	$⊢ A \subseteq ℝ \to (y \in A \to (x \in ℝ \to ((y < x \lor y = x) \to y < x + 1)))$
21	20	com23	$⊢ A \subseteq ℝ \to (x \in ℝ \to (y \in A \to ((y < x \lor y = x) \to y < x + 1)))$
22	21	imp	$⊢ (A \subseteq ℝ \land x \in ℝ) \to (y \in A \to ((y < x \lor y = x) \to y < x + 1))$
23	22	a2d	$⊢ (A \subseteq ℝ \land x \in ℝ) \to ((y \in A \to (y < x \lor y = x)) \to (y \in A \to y < x + 1))$
24	23	ralimdv2	$⊢ (A \subseteq ℝ \land x \in ℝ) \to (\forall y \in A (y < x \lor y = x) \to \forall y \in A y < x + 1)$
25	24	expimpd	$⊢ A \subseteq ℝ \to ((x \in ℝ \land \forall y \in A (y < x \lor y = x)) \to \forall y \in A y < x + 1)$
26	3 25	jcad	$⊢ A \subseteq ℝ \to ((x \in ℝ \land \forall y \in A (y < x \lor y = x)) \to (x + 1 \in ℝ \land \forall y \in A y < x + 1))$
27		ovex	$⊢ x + 1 \in V$
28		eleq1	$⊢ z = x + 1 \to (z \in ℝ \leftrightarrow x + 1 \in ℝ)$
29		breq2	$⊢ z = x + 1 \to (y < z \leftrightarrow y < x + 1)$
30	29	ralbidv	$⊢ z = x + 1 \to (\forall y \in A y < z \leftrightarrow \forall y \in A y < x + 1)$
31	28 30	anbi12d	$⊢ z = x + 1 \to ((z \in ℝ \land \forall y \in A y < z) \leftrightarrow (x + 1 \in ℝ \land \forall y \in A y < x + 1))$
32	27 31	spcev	$⊢ (x + 1 \in ℝ \land \forall y \in A y < x + 1) \to \exists z (z \in ℝ \land \forall y \in A y < z)$
33	26 32	syl6	$⊢ A \subseteq ℝ \to ((x \in ℝ \land \forall y \in A (y < x \lor y = x)) \to \exists z (z \in ℝ \land \forall y \in A y < z))$
34	33	exlimdv	$⊢ A \subseteq ℝ \to (\exists x (x \in ℝ \land \forall y \in A (y < x \lor y = x)) \to \exists z (z \in ℝ \land \forall y \in A y < z))$
35		eleq1	$⊢ z = x \to (z \in ℝ \leftrightarrow x \in ℝ)$
36		breq2	$⊢ z = x \to (y < z \leftrightarrow y < x)$
37	36	ralbidv	$⊢ z = x \to (\forall y \in A y < z \leftrightarrow \forall y \in A y < x)$
38	35 37	anbi12d	$⊢ z = x \to ((z \in ℝ \land \forall y \in A y < z) \leftrightarrow (x \in ℝ \land \forall y \in A y < x))$
39	38	cbvexvw	$⊢ \exists z (z \in ℝ \land \forall y \in A y < z) \leftrightarrow \exists x (x \in ℝ \land \forall y \in A y < x)$
40	34 39	syl6ib	$⊢ A \subseteq ℝ \to (\exists x (x \in ℝ \land \forall y \in A (y < x \lor y = x)) \to \exists x (x \in ℝ \land \forall y \in A y < x))$
41		df-rex	$⊢ \exists x \in ℝ \forall y \in A (y < x \lor y = x) \leftrightarrow \exists x (x \in ℝ \land \forall y \in A (y < x \lor y = x))$
42		df-rex	$⊢ \exists x \in ℝ \forall y \in A y < x \leftrightarrow \exists x (x \in ℝ \land \forall y \in A y < x)$
43	40 41 42	3imtr4g	$⊢ A \subseteq ℝ \to (\exists x \in ℝ \forall y \in A (y < x \lor y = x) \to \exists x \in ℝ \forall y \in A y < x)$
44	43	adantr	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (\exists x \in ℝ \forall y \in A (y < x \lor y = x) \to \exists x \in ℝ \forall y \in A y < x)$
45	44	imdistani	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land \exists x \in ℝ \forall y \in A (y < x \lor y = x)) \to ((A \subseteq ℝ \land A \neq \emptyset) \land \exists x \in ℝ \forall y \in A y < x)$
46		df-3an	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A (y < x \lor y = x)) \leftrightarrow ((A \subseteq ℝ \land A \neq \emptyset) \land \exists x \in ℝ \forall y \in A (y < x \lor y = x))$
47		df-3an	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y < x) \leftrightarrow ((A \subseteq ℝ \land A \neq \emptyset) \land \exists x \in ℝ \forall y \in A y < x)$
48	45 46 47	3imtr4i	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A (y < x \lor y = x)) \to (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y < x)$
49		axsup	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y < x) \to \exists x \in ℝ (\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z))$
50	48 49	syl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A (y < x \lor y = x)) \to \exists x \in ℝ (\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z))$

Metamath Proof Explorer

Theorem sup2

Proof