supxrunb1

Description: The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006)

		Ref	Expression
	Assertion	supxrunb1	$⊢ A \subseteq ℝ^{} \to (\forall x \in ℝ \exists y \in A x \leq y \leftrightarrow sup (A ℝ^{} <) = +∞)$

Proof

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq ℝ^{} \to (z \in A \to z \in ℝ^{})$
2		pnfnlt	$⊢ z \in ℝ^{*} \to \neg +∞ < z$
3	1 2	syl6	$⊢ A \subseteq ℝ^{*} \to (z \in A \to \neg +∞ < z)$
4	3	ralrimiv	$⊢ A \subseteq ℝ^{*} \to \forall z \in A \neg +∞ < z$
5	4	adantr	$⊢ (A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x \leq y) \to \forall z \in A \neg +∞ < z$
6		peano2re	$⊢ z \in ℝ \to z + 1 \in ℝ$
7		breq1	$⊢ x = z + 1 \to (x \leq y \leftrightarrow z + 1 \leq y)$
8	7	rexbidv	$⊢ x = z + 1 \to (\exists y \in A x \leq y \leftrightarrow \exists y \in A z + 1 \leq y)$
9	8	rspcva	$⊢ (z + 1 \in ℝ \land \forall x \in ℝ \exists y \in A x \leq y) \to \exists y \in A z + 1 \leq y$
10	9	adantrr	$⊢ (z + 1 \in ℝ \land (\forall x \in ℝ \exists y \in A x \leq y \land A \subseteq ℝ^{*})) \to \exists y \in A z + 1 \leq y$
11	10	ancoms	$⊢ ((\forall x \in ℝ \exists y \in A x \leq y \land A \subseteq ℝ^{*}) \land z + 1 \in ℝ) \to \exists y \in A z + 1 \leq y$
12	6 11	sylan2	$⊢ ((\forall x \in ℝ \exists y \in A x \leq y \land A \subseteq ℝ^{*}) \land z \in ℝ) \to \exists y \in A z + 1 \leq y$
13		ssel2	$⊢ (A \subseteq ℝ^{} \land y \in A) \to y \in ℝ^{}$
14		ltp1	$⊢ z \in ℝ \to z < z + 1$
15	14	adantr	$⊢ (z \in ℝ \land y \in ℝ^{*}) \to z < z + 1$
16	6	ancli	$⊢ z \in ℝ \to (z \in ℝ \land z + 1 \in ℝ)$
17		rexr	$⊢ z \in ℝ \to z \in ℝ^{*}$
18		rexr	$⊢ z + 1 \in ℝ \to z + 1 \in ℝ^{*}$
19		xrltletr	$⊢ (z \in ℝ^{} \land z + 1 \in ℝ^{} \land y \in ℝ^{*}) \to ((z < z + 1 \land z + 1 \leq y) \to z < y)$
20	18 19	syl3an2	$⊢ (z \in ℝ^{} \land z + 1 \in ℝ \land y \in ℝ^{}) \to ((z < z + 1 \land z + 1 \leq y) \to z < y)$
21	17 20	syl3an1	$⊢ (z \in ℝ \land z + 1 \in ℝ \land y \in ℝ^{*}) \to ((z < z + 1 \land z + 1 \leq y) \to z < y)$
22	21	3expa	$⊢ ((z \in ℝ \land z + 1 \in ℝ) \land y \in ℝ^{*}) \to ((z < z + 1 \land z + 1 \leq y) \to z < y)$
23	16 22	sylan	$⊢ (z \in ℝ \land y \in ℝ^{*}) \to ((z < z + 1 \land z + 1 \leq y) \to z < y)$
24	15 23	mpand	$⊢ (z \in ℝ \land y \in ℝ^{*}) \to (z + 1 \leq y \to z < y)$
25	24	ancoms	$⊢ (y \in ℝ^{*} \land z \in ℝ) \to (z + 1 \leq y \to z < y)$
26	13 25	sylan	$⊢ ((A \subseteq ℝ^{*} \land y \in A) \land z \in ℝ) \to (z + 1 \leq y \to z < y)$
27	26	an32s	$⊢ ((A \subseteq ℝ^{*} \land z \in ℝ) \land y \in A) \to (z + 1 \leq y \to z < y)$
28	27	reximdva	$⊢ (A \subseteq ℝ^{*} \land z \in ℝ) \to (\exists y \in A z + 1 \leq y \to \exists y \in A z < y)$
29	28	adantll	$⊢ ((\forall x \in ℝ \exists y \in A x \leq y \land A \subseteq ℝ^{*}) \land z \in ℝ) \to (\exists y \in A z + 1 \leq y \to \exists y \in A z < y)$
30	12 29	mpd	$⊢ ((\forall x \in ℝ \exists y \in A x \leq y \land A \subseteq ℝ^{*}) \land z \in ℝ) \to \exists y \in A z < y$
31	30	exp31	$⊢ \forall x \in ℝ \exists y \in A x \leq y \to (A \subseteq ℝ^{*} \to (z \in ℝ \to \exists y \in A z < y))$
32	31	a1dd	$⊢ \forall x \in ℝ \exists y \in A x \leq y \to (A \subseteq ℝ^{*} \to (z < +∞ \to (z \in ℝ \to \exists y \in A z < y)))$
33	32	com4r	$⊢ z \in ℝ \to (\forall x \in ℝ \exists y \in A x \leq y \to (A \subseteq ℝ^{*} \to (z < +∞ \to \exists y \in A z < y)))$
34	33	com13	$⊢ A \subseteq ℝ^{*} \to (\forall x \in ℝ \exists y \in A x \leq y \to (z \in ℝ \to (z < +∞ \to \exists y \in A z < y)))$
35	34	imp	$⊢ (A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x \leq y) \to (z \in ℝ \to (z < +∞ \to \exists y \in A z < y))$
36	35	ralrimiv	$⊢ (A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x \leq y) \to \forall z \in ℝ (z < +∞ \to \exists y \in A z < y)$
37	5 36	jca	$⊢ (A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x \leq y) \to (\forall z \in A \neg +∞ < z \land \forall z \in ℝ (z < +∞ \to \exists y \in A z < y))$
38		pnfxr	$⊢ +∞ \in ℝ^{*}$
39		supxr	$⊢ ((A \subseteq ℝ^{} \land +∞ \in ℝ^{}) \land (\forall z \in A \neg +∞ < z \land \forall z \in ℝ (z < +∞ \to \exists y \in A z < y))) \to sup (A ℝ^{*} <) = +∞$
40	38 39	mpanl2	$⊢ (A \subseteq ℝ^{} \land (\forall z \in A \neg +∞ < z \land \forall z \in ℝ (z < +∞ \to \exists y \in A z < y))) \to sup (A ℝ^{} <) = +∞$
41	37 40	syldan	$⊢ (A \subseteq ℝ^{} \land \forall x \in ℝ \exists y \in A x \leq y) \to sup (A ℝ^{} <) = +∞$
42	41	ex	$⊢ A \subseteq ℝ^{} \to (\forall x \in ℝ \exists y \in A x \leq y \to sup (A ℝ^{} <) = +∞)$
43		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
44	43	ad2antlr	$⊢ ((A \subseteq ℝ^{} \land x \in ℝ) \land sup (A ℝ^{} <) = +∞) \to x \in ℝ^{*}$
45		ltpnf	$⊢ x \in ℝ \to x < +∞$
46		breq2	$⊢ sup (A ℝ^{} <) = +∞ \to (x < sup (A ℝ^{} <) \leftrightarrow x < +∞)$
47	45 46	syl5ibr	$⊢ sup (A ℝ^{} <) = +∞ \to (x \in ℝ \to x < sup (A ℝ^{} <))$
48	47	impcom	$⊢ (x \in ℝ \land sup (A ℝ^{} <) = +∞) \to x < sup (A ℝ^{} <)$
49	48	adantll	$⊢ ((A \subseteq ℝ^{} \land x \in ℝ) \land sup (A ℝ^{} <) = +∞) \to x < sup (A ℝ^{*} <)$
50		xrltso	$⊢ < Or ℝ^{*}$
51	50	a1i	$⊢ ((A \subseteq ℝ^{} \land x \in ℝ) \land sup (A ℝ^{} <) = +∞) \to < Or ℝ^{*}$
52		xrsupss	$⊢ A \subseteq ℝ^{} \to \exists z \in ℝ^{} (\forall w \in A \neg z < w \land \forall w \in ℝ^{*} (w < z \to \exists y \in A w < y))$
53	52	ad2antrr	$⊢ ((A \subseteq ℝ^{} \land x \in ℝ) \land sup (A ℝ^{} <) = +∞) \to \exists z \in ℝ^{} (\forall w \in A \neg z < w \land \forall w \in ℝ^{} (w < z \to \exists y \in A w < y))$
54	51 53	suplub	$⊢ ((A \subseteq ℝ^{} \land x \in ℝ) \land sup (A ℝ^{} <) = +∞) \to ((x \in ℝ^{} \land x < sup (A ℝ^{} <)) \to \exists y \in A x < y)$
55	44 49 54	mp2and	$⊢ ((A \subseteq ℝ^{} \land x \in ℝ) \land sup (A ℝ^{} <) = +∞) \to \exists y \in A x < y$
56	55	ex	$⊢ (A \subseteq ℝ^{} \land x \in ℝ) \to (sup (A ℝ^{} <) = +∞ \to \exists y \in A x < y)$
57	43	ad2antlr	$⊢ ((A \subseteq ℝ^{} \land x \in ℝ) \land y \in A) \to x \in ℝ^{}$
58	13	adantlr	$⊢ ((A \subseteq ℝ^{} \land x \in ℝ) \land y \in A) \to y \in ℝ^{}$
59		xrltle	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to (x < y \to x \leq y)$
60	57 58 59	syl2anc	$⊢ ((A \subseteq ℝ^{*} \land x \in ℝ) \land y \in A) \to (x < y \to x \leq y)$
61	60	reximdva	$⊢ (A \subseteq ℝ^{*} \land x \in ℝ) \to (\exists y \in A x < y \to \exists y \in A x \leq y)$
62	56 61	syld	$⊢ (A \subseteq ℝ^{} \land x \in ℝ) \to (sup (A ℝ^{} <) = +∞ \to \exists y \in A x \leq y)$
63	62	ralrimdva	$⊢ A \subseteq ℝ^{} \to (sup (A ℝ^{} <) = +∞ \to \forall x \in ℝ \exists y \in A x \leq y)$
64	42 63	impbid	$⊢ A \subseteq ℝ^{} \to (\forall x \in ℝ \exists y \in A x \leq y \leftrightarrow sup (A ℝ^{} <) = +∞)$

Metamath Proof Explorer

Theorem supxrunb1

Proof