unb2ltle

Description: "Unbounded below" expressed with < and with <_ . (Contributed by Glauco Siliprandi, 23-Oct-2021)

		Ref	Expression
	Assertion	unb2ltle	$⊢ A \subseteq ℝ^{*} \to (\forall w \in ℝ \exists y \in A y < w \leftrightarrow \forall x \in ℝ \exists y \in A y \leq x)$

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ w A \subseteq ℝ^{*}$
2		nfra1	$⊢ Ⅎ w \forall w \in ℝ \exists y \in A y < w$
3	1 2	nfan	$⊢ Ⅎ w (A \subseteq ℝ^{*} \land \forall w \in ℝ \exists y \in A y < w)$
4		simpll	$⊢ ((A \subseteq ℝ^{} \land \forall w \in ℝ \exists y \in A y < w) \land w \in ℝ) \to A \subseteq ℝ^{}$
5		simpr	$⊢ ((A \subseteq ℝ^{*} \land \forall w \in ℝ \exists y \in A y < w) \land w \in ℝ) \to w \in ℝ$
6		rspa	$⊢ (\forall w \in ℝ \exists y \in A y < w \land w \in ℝ) \to \exists y \in A y < w$
7	6	adantll	$⊢ ((A \subseteq ℝ^{*} \land \forall w \in ℝ \exists y \in A y < w) \land w \in ℝ) \to \exists y \in A y < w$
8		ssel2	$⊢ (A \subseteq ℝ^{} \land y \in A) \to y \in ℝ^{}$
9	8	ad4ant13	$⊢ (((A \subseteq ℝ^{} \land w \in ℝ) \land y \in A) \land y < w) \to y \in ℝ^{}$
10		simpllr	$⊢ (((A \subseteq ℝ^{*} \land w \in ℝ) \land y \in A) \land y < w) \to w \in ℝ$
11	10	rexrd	$⊢ (((A \subseteq ℝ^{} \land w \in ℝ) \land y \in A) \land y < w) \to w \in ℝ^{}$
12		simpr	$⊢ (((A \subseteq ℝ^{*} \land w \in ℝ) \land y \in A) \land y < w) \to y < w$
13	9 11 12	xrltled	$⊢ (((A \subseteq ℝ^{*} \land w \in ℝ) \land y \in A) \land y < w) \to y \leq w$
14	13	ex	$⊢ ((A \subseteq ℝ^{*} \land w \in ℝ) \land y \in A) \to (y < w \to y \leq w)$
15	14	reximdva	$⊢ (A \subseteq ℝ^{*} \land w \in ℝ) \to (\exists y \in A y < w \to \exists y \in A y \leq w)$
16	15	imp	$⊢ ((A \subseteq ℝ^{*} \land w \in ℝ) \land \exists y \in A y < w) \to \exists y \in A y \leq w$
17	4 5 7 16	syl21anc	$⊢ ((A \subseteq ℝ^{*} \land \forall w \in ℝ \exists y \in A y < w) \land w \in ℝ) \to \exists y \in A y \leq w$
18	3 17	ralrimia	$⊢ (A \subseteq ℝ^{*} \land \forall w \in ℝ \exists y \in A y < w) \to \forall w \in ℝ \exists y \in A y \leq w$
19		breq2	$⊢ w = x \to (y \leq w \leftrightarrow y \leq x)$
20	19	rexbidv	$⊢ w = x \to (\exists y \in A y \leq w \leftrightarrow \exists y \in A y \leq x)$
21	20	cbvralvw	$⊢ \forall w \in ℝ \exists y \in A y \leq w \leftrightarrow \forall x \in ℝ \exists y \in A y \leq x$
22	18 21	sylib	$⊢ (A \subseteq ℝ^{*} \land \forall w \in ℝ \exists y \in A y < w) \to \forall x \in ℝ \exists y \in A y \leq x$
23	22	ex	$⊢ A \subseteq ℝ^{*} \to (\forall w \in ℝ \exists y \in A y < w \to \forall x \in ℝ \exists y \in A y \leq x)$
24		simpll	$⊢ ((A \subseteq ℝ^{} \land \forall x \in ℝ \exists y \in A y \leq x) \land w \in ℝ) \to A \subseteq ℝ^{}$
25		simpr	$⊢ ((A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A y \leq x) \land w \in ℝ) \to w \in ℝ$
26		peano2rem	$⊢ w \in ℝ \to w - 1 \in ℝ$
27	26	adantl	$⊢ (\forall x \in ℝ \exists y \in A y \leq x \land w \in ℝ) \to w - 1 \in ℝ$
28		simpl	$⊢ (\forall x \in ℝ \exists y \in A y \leq x \land w \in ℝ) \to \forall x \in ℝ \exists y \in A y \leq x$
29		breq2	$⊢ x = w - 1 \to (y \leq x \leftrightarrow y \leq w - 1)$
30	29	rexbidv	$⊢ x = w - 1 \to (\exists y \in A y \leq x \leftrightarrow \exists y \in A y \leq w - 1)$
31	30	rspcva	$⊢ (w - 1 \in ℝ \land \forall x \in ℝ \exists y \in A y \leq x) \to \exists y \in A y \leq w - 1$
32	27 28 31	syl2anc	$⊢ (\forall x \in ℝ \exists y \in A y \leq x \land w \in ℝ) \to \exists y \in A y \leq w - 1$
33	32	adantll	$⊢ ((A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A y \leq x) \land w \in ℝ) \to \exists y \in A y \leq w - 1$
34	8	ad4ant13	$⊢ (((A \subseteq ℝ^{} \land w \in ℝ) \land y \in A) \land y \leq w - 1) \to y \in ℝ^{}$
35		simpllr	$⊢ (((A \subseteq ℝ^{*} \land w \in ℝ) \land y \in A) \land y \leq w - 1) \to w \in ℝ$
36	26	rexrd	$⊢ w \in ℝ \to w - 1 \in ℝ^{*}$
37	35 36	syl	$⊢ (((A \subseteq ℝ^{} \land w \in ℝ) \land y \in A) \land y \leq w - 1) \to w - 1 \in ℝ^{}$
38	35	rexrd	$⊢ (((A \subseteq ℝ^{} \land w \in ℝ) \land y \in A) \land y \leq w - 1) \to w \in ℝ^{}$
39		simpr	$⊢ (((A \subseteq ℝ^{*} \land w \in ℝ) \land y \in A) \land y \leq w - 1) \to y \leq w - 1$
40	35	ltm1d	$⊢ (((A \subseteq ℝ^{*} \land w \in ℝ) \land y \in A) \land y \leq w - 1) \to w - 1 < w$
41	34 37 38 39 40	xrlelttrd	$⊢ (((A \subseteq ℝ^{*} \land w \in ℝ) \land y \in A) \land y \leq w - 1) \to y < w$
42	41	ex	$⊢ ((A \subseteq ℝ^{*} \land w \in ℝ) \land y \in A) \to (y \leq w - 1 \to y < w)$
43	42	reximdva	$⊢ (A \subseteq ℝ^{*} \land w \in ℝ) \to (\exists y \in A y \leq w - 1 \to \exists y \in A y < w)$
44	43	imp	$⊢ ((A \subseteq ℝ^{*} \land w \in ℝ) \land \exists y \in A y \leq w - 1) \to \exists y \in A y < w$
45	24 25 33 44	syl21anc	$⊢ ((A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A y \leq x) \land w \in ℝ) \to \exists y \in A y < w$
46	45	ralrimiva	$⊢ (A \subseteq ℝ^{*} \land \forall x \in ℝ \exists y \in A y \leq x) \to \forall w \in ℝ \exists y \in A y < w$
47	46	ex	$⊢ A \subseteq ℝ^{*} \to (\forall x \in ℝ \exists y \in A y \leq x \to \forall w \in ℝ \exists y \in A y < w)$
48	23 47	impbid	$⊢ A \subseteq ℝ^{*} \to (\forall w \in ℝ \exists y \in A y < w \leftrightarrow \forall x \in ℝ \exists y \in A y \leq x)$

Metamath Proof Explorer

Theorem unb2ltle

Proof