supxrunb3

Description: The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		peano2re	$⊢ w \in ℝ \to w + 1 \in ℝ$
2	1	adantl	$⊢ (\forall x \in ℝ \exists y \in A x \leq y \land w \in ℝ) \to w + 1 \in ℝ$
3		simpl	$⊢ (\forall x \in ℝ \exists y \in A x \leq y \land w \in ℝ) \to \forall x \in ℝ \exists y \in A x \leq y$
4		breq1	$⊢ x = w + 1 \to (x \leq y \leftrightarrow w + 1 \leq y)$
5	4	rexbidv	$⊢ x = w + 1 \to (\exists y \in A x \leq y \leftrightarrow \exists y \in A w + 1 \leq y)$
6	5	rspcva	$⊢ (w + 1 \in ℝ \land \forall x \in ℝ \exists y \in A x \leq y) \to \exists y \in A w + 1 \leq y$
7	2 3 6	syl2anc	$⊢ (\forall x \in ℝ \exists y \in A x \leq y \land w \in ℝ) \to \exists y \in A w + 1 \leq y$
8	7	adantll	$⊢ ((A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x \leq y) \land w \in ℝ) \to \exists y \in A w + 1 \leq y$
9		nfv	$⊢ Ⅎ y A \subseteq ℝ^{*}$
10		nfcv	$⊢ \underline{Ⅎ} y ℝ$
11		nfre1	$⊢ Ⅎ y \exists y \in A x \leq y$
12	10 11	nfralw	$⊢ Ⅎ y \forall x \in ℝ \exists y \in A x \leq y$
13	9 12	nfan	$⊢ Ⅎ y (A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x \leq y)$
14		nfv	$⊢ Ⅎ y w \in ℝ$
15	13 14	nfan	$⊢ Ⅎ y ((A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x \leq y) \land w \in ℝ)$
16		simp1r	$⊢ ((A \subseteq ℝ^{*} \land w \in ℝ) \land y \in A \land w + 1 \leq y) \to w \in ℝ$
17		rexr	$⊢ w \in ℝ \to w \in ℝ^{*}$
18	16 17	syl	$⊢ ((A \subseteq ℝ^{} \land w \in ℝ) \land y \in A \land w + 1 \leq y) \to w \in ℝ^{}$
19	1	rexrd	$⊢ w \in ℝ \to w + 1 \in ℝ^{*}$
20	16 19	syl	$⊢ ((A \subseteq ℝ^{} \land w \in ℝ) \land y \in A \land w + 1 \leq y) \to w + 1 \in ℝ^{}$
21		simp1l	$⊢ ((A \subseteq ℝ^{} \land w \in ℝ) \land y \in A \land w + 1 \leq y) \to A \subseteq ℝ^{}$
22		simp2	$⊢ ((A \subseteq ℝ^{*} \land w \in ℝ) \land y \in A \land w + 1 \leq y) \to y \in A$
23		ssel2	$⊢ (A \subseteq ℝ^{} \land y \in A) \to y \in ℝ^{}$
24	21 22 23	syl2anc	$⊢ ((A \subseteq ℝ^{} \land w \in ℝ) \land y \in A \land w + 1 \leq y) \to y \in ℝ^{}$
25	16	ltp1d	$⊢ ((A \subseteq ℝ^{*} \land w \in ℝ) \land y \in A \land w + 1 \leq y) \to w < w + 1$
26		simp3	$⊢ ((A \subseteq ℝ^{*} \land w \in ℝ) \land y \in A \land w + 1 \leq y) \to w + 1 \leq y$
27	18 20 24 25 26	xrltletrd	$⊢ ((A \subseteq ℝ^{*} \land w \in ℝ) \land y \in A \land w + 1 \leq y) \to w < y$
28	27	3exp	$⊢ (A \subseteq ℝ^{*} \land w \in ℝ) \to (y \in A \to (w + 1 \leq y \to w < y))$
29	28	adantlr	$⊢ ((A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x \leq y) \land w \in ℝ) \to (y \in A \to (w + 1 \leq y \to w < y))$
30	15 29	reximdai	$⊢ ((A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x \leq y) \land w \in ℝ) \to (\exists y \in A w + 1 \leq y \to \exists y \in A w < y)$
31	8 30	mpd	$⊢ ((A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x \leq y) \land w \in ℝ) \to \exists y \in A w < y$
32	31	ralrimiva	$⊢ (A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x \leq y) \to \forall w \in ℝ \exists y \in A w < y$
33	32	ex	$⊢ A \subseteq ℝ^{*} \to (\forall x \in ℝ \exists y \in A x \leq y \to \forall w \in ℝ \exists y \in A w < y)$
34		breq1	$⊢ w = x \to (w < y \leftrightarrow x < y)$
35	34	rexbidv	$⊢ w = x \to (\exists y \in A w < y \leftrightarrow \exists y \in A x < y)$
36	35	cbvralvw	$⊢ \forall w \in ℝ \exists y \in A w < y \leftrightarrow \forall x \in ℝ \exists y \in A x < y$
37	36	biimpi	$⊢ \forall w \in ℝ \exists y \in A w < y \to \forall x \in ℝ \exists y \in A x < y$
38		nfv	$⊢ Ⅎ x A \subseteq ℝ^{*}$
39		nfra1	$⊢ Ⅎ x \forall x \in ℝ \exists y \in A x < y$
40	38 39	nfan	$⊢ Ⅎ x (A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x < y)$
41		simpll	$⊢ ((A \subseteq ℝ^{} \land \forall x \in ℝ \exists y \in A x < y) \land x \in ℝ) \to A \subseteq ℝ^{}$
42		simpr	$⊢ ((A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x < y) \land x \in ℝ) \to x \in ℝ$
43		rspa	$⊢ (\forall x \in ℝ \exists y \in A x < y \land x \in ℝ) \to \exists y \in A x < y$
44	43	adantll	$⊢ ((A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x < y) \land x \in ℝ) \to \exists y \in A x < y$
45		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
46	45	ad3antlr	$⊢ (((A \subseteq ℝ^{} \land x \in ℝ) \land y \in A) \land x < y) \to x \in ℝ^{}$
47	23	adantr	$⊢ ((A \subseteq ℝ^{} \land y \in A) \land x < y) \to y \in ℝ^{}$
48	47	adantllr	$⊢ (((A \subseteq ℝ^{} \land x \in ℝ) \land y \in A) \land x < y) \to y \in ℝ^{}$
49		simpr	$⊢ (((A \subseteq ℝ^{*} \land x \in ℝ) \land y \in A) \land x < y) \to x < y$
50	46 48 49	xrltled	$⊢ (((A \subseteq ℝ^{*} \land x \in ℝ) \land y \in A) \land x < y) \to x \leq y$
51	50	ex	$⊢ ((A \subseteq ℝ^{*} \land x \in ℝ) \land y \in A) \to (x < y \to x \leq y)$
52	51	reximdva	$⊢ (A \subseteq ℝ^{*} \land x \in ℝ) \to (\exists y \in A x < y \to \exists y \in A x \leq y)$
53	52	adantlr	$⊢ ((A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x < y) \land x \in ℝ) \to (\exists y \in A x < y \to \exists y \in A x \leq y)$
54	44 53	mpd	$⊢ ((A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x < y) \land x \in ℝ) \to \exists y \in A x \leq y$
55		simpr	$⊢ ((A \subseteq ℝ^{*} \land x \in ℝ) \land \exists y \in A x \leq y) \to \exists y \in A x \leq y$
56	41 42 54 55	syl21anc	$⊢ ((A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x < y) \land x \in ℝ) \to \exists y \in A x \leq y$
57	56	ex	$⊢ (A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x < y) \to (x \in ℝ \to \exists y \in A x \leq y)$
58	40 57	ralrimi	$⊢ (A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A x < y) \to \forall x \in ℝ \exists y \in A x \leq y$
59	37 58	sylan2	$⊢ (A \subseteq ℝ^{*} \land \forall w \in ℝ \exists y \in A w < y) \to \forall x \in ℝ \exists y \in A x \leq y$
60	59	ex	$⊢ A \subseteq ℝ^{*} \to (\forall w \in ℝ \exists y \in A w < y \to \forall x \in ℝ \exists y \in A x \leq y)$
61	33 60	impbid	$⊢ A \subseteq ℝ^{*} \to (\forall x \in ℝ \exists y \in A x \leq y \leftrightarrow \forall w \in ℝ \exists y \in A w < y)$
62		supxrunb2	$⊢ A \subseteq ℝ^{} \to (\forall w \in ℝ \exists y \in A w < y \leftrightarrow sup (A ℝ^{} <) = +∞)$
63	61 62	bitrd	$⊢ A \subseteq ℝ^{} \to (\forall x \in ℝ \exists y \in A x \leq y \leftrightarrow sup (A ℝ^{} <) = +∞)$

Metamath Proof Explorer

Theorem supxrunb3

Proof