xrub

Description: By quantifying only over reals, we can specify any extended real upper bound for any set of extended reals. (Contributed by NM, 9-Apr-2006)

		Ref	Expression
	Assertion	xrub	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (\forall x \in ℝ (x < B \to \exists y \in A x < y) \leftrightarrow \forall x \in ℝ^{*} (x < B \to \exists y \in A x < y))$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ x = z \to (x < B \leftrightarrow z < B)$
2		breq1	$⊢ x = z \to (x < y \leftrightarrow z < y)$
3	2	rexbidv	$⊢ x = z \to (\exists y \in A x < y \leftrightarrow \exists y \in A z < y)$
4	1 3	imbi12d	$⊢ x = z \to ((x < B \to \exists y \in A x < y) \leftrightarrow (z < B \to \exists y \in A z < y))$
5	4	cbvralvw	$⊢ \forall x \in ℝ (x < B \to \exists y \in A x < y) \leftrightarrow \forall z \in ℝ (z < B \to \exists y \in A z < y)$
6		elxr	$⊢ x \in ℝ^{*} \leftrightarrow (x \in ℝ \lor x = +∞ \lor x = −∞)$
7		pm2.27	$⊢ x \in ℝ \to ((x \in ℝ \to (x < B \to \exists y \in A x < y)) \to (x < B \to \exists y \in A x < y))$
8	7	a1i	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land \forall z \in ℝ (z < B \to \exists y \in A z < y)) \to (x \in ℝ \to ((x \in ℝ \to (x < B \to \exists y \in A x < y)) \to (x < B \to \exists y \in A x < y)))$
9		pnfnlt	$⊢ B \in ℝ^{*} \to \neg +∞ < B$
10		breq1	$⊢ x = +∞ \to (x < B \leftrightarrow +∞ < B)$
11	10	notbid	$⊢ x = +∞ \to (\neg x < B \leftrightarrow \neg +∞ < B)$
12	9 11	imbitrrid	$⊢ x = +∞ \to (B \in ℝ^{*} \to \neg x < B)$
13		pm2.21	$⊢ \neg x < B \to (x < B \to \exists y \in A x < y)$
14	12 13	syl6com	$⊢ B \in ℝ^{*} \to (x = +∞ \to (x < B \to \exists y \in A x < y))$
15	14	ad2antlr	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land \forall z \in ℝ (z < B \to \exists y \in A z < y)) \to (x = +∞ \to (x < B \to \exists y \in A x < y))$
16	15	a1dd	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land \forall z \in ℝ (z < B \to \exists y \in A z < y)) \to (x = +∞ \to ((x \in ℝ \to (x < B \to \exists y \in A x < y)) \to (x < B \to \exists y \in A x < y)))$
17		elxr	$⊢ B \in ℝ^{*} \leftrightarrow (B \in ℝ \lor B = +∞ \lor B = −∞)$
18		peano2rem	$⊢ B \in ℝ \to B - 1 \in ℝ$
19		breq1	$⊢ z = B - 1 \to (z < B \leftrightarrow B - 1 < B)$
20		breq1	$⊢ z = B - 1 \to (z < y \leftrightarrow B - 1 < y)$
21	20	rexbidv	$⊢ z = B - 1 \to (\exists y \in A z < y \leftrightarrow \exists y \in A B - 1 < y)$
22	19 21	imbi12d	$⊢ z = B - 1 \to ((z < B \to \exists y \in A z < y) \leftrightarrow (B - 1 < B \to \exists y \in A B - 1 < y))$
23	22	rspcv	$⊢ B - 1 \in ℝ \to (\forall z \in ℝ (z < B \to \exists y \in A z < y) \to (B - 1 < B \to \exists y \in A B - 1 < y))$
24	18 23	syl	$⊢ B \in ℝ \to (\forall z \in ℝ (z < B \to \exists y \in A z < y) \to (B - 1 < B \to \exists y \in A B - 1 < y))$
25	24	adantl	$⊢ (A \subseteq ℝ^{*} \land B \in ℝ) \to (\forall z \in ℝ (z < B \to \exists y \in A z < y) \to (B - 1 < B \to \exists y \in A B - 1 < y))$
26		ltm1	$⊢ B \in ℝ \to B - 1 < B$
27		id	$⊢ (B - 1 < B \to \exists y \in A B - 1 < y) \to (B - 1 < B \to \exists y \in A B - 1 < y)$
28	26 27	syl5com	$⊢ B \in ℝ \to ((B - 1 < B \to \exists y \in A B - 1 < y) \to \exists y \in A B - 1 < y)$
29	28	adantl	$⊢ (A \subseteq ℝ^{*} \land B \in ℝ) \to ((B - 1 < B \to \exists y \in A B - 1 < y) \to \exists y \in A B - 1 < y)$
30	18	ad2antlr	$⊢ ((A \subseteq ℝ^{*} \land B \in ℝ) \land y \in A) \to B - 1 \in ℝ$
31		mnflt	$⊢ B - 1 \in ℝ \to −∞ < B - 1$
32	30 31	syl	$⊢ ((A \subseteq ℝ^{*} \land B \in ℝ) \land y \in A) \to −∞ < B - 1$
33		mnfxr	$⊢ −∞ \in ℝ^{*}$
34	30	rexrd	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ) \land y \in A) \to B - 1 \in ℝ^{}$
35		ssel2	$⊢ (A \subseteq ℝ^{} \land y \in A) \to y \in ℝ^{}$
36	35	adantlr	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ) \land y \in A) \to y \in ℝ^{}$
37		xrlttr	$⊢ (−∞ \in ℝ^{} \land B - 1 \in ℝ^{} \land y \in ℝ^{*}) \to ((−∞ < B - 1 \land B - 1 < y) \to −∞ < y)$
38	33 34 36 37	mp3an2i	$⊢ ((A \subseteq ℝ^{*} \land B \in ℝ) \land y \in A) \to ((−∞ < B - 1 \land B - 1 < y) \to −∞ < y)$
39	32 38	mpand	$⊢ ((A \subseteq ℝ^{*} \land B \in ℝ) \land y \in A) \to (B - 1 < y \to −∞ < y)$
40	39	reximdva	$⊢ (A \subseteq ℝ^{*} \land B \in ℝ) \to (\exists y \in A B - 1 < y \to \exists y \in A −∞ < y)$
41	25 29 40	3syld	$⊢ (A \subseteq ℝ^{*} \land B \in ℝ) \to (\forall z \in ℝ (z < B \to \exists y \in A z < y) \to \exists y \in A −∞ < y)$
42	41	a1dd	$⊢ (A \subseteq ℝ^{*} \land B \in ℝ) \to (\forall z \in ℝ (z < B \to \exists y \in A z < y) \to (−∞ < B \to \exists y \in A −∞ < y))$
43		1re	$⊢ 1 \in ℝ$
44		breq1	$⊢ z = 1 \to (z < B \leftrightarrow 1 < B)$
45		breq1	$⊢ z = 1 \to (z < y \leftrightarrow 1 < y)$
46	45	rexbidv	$⊢ z = 1 \to (\exists y \in A z < y \leftrightarrow \exists y \in A 1 < y)$
47	44 46	imbi12d	$⊢ z = 1 \to ((z < B \to \exists y \in A z < y) \leftrightarrow (1 < B \to \exists y \in A 1 < y))$
48	47	rspcv	$⊢ 1 \in ℝ \to (\forall z \in ℝ (z < B \to \exists y \in A z < y) \to (1 < B \to \exists y \in A 1 < y))$
49	43 48	ax-mp	$⊢ \forall z \in ℝ (z < B \to \exists y \in A z < y) \to (1 < B \to \exists y \in A 1 < y)$
50		ltpnf	$⊢ 1 \in ℝ \to 1 < +∞$
51	43 50	ax-mp	$⊢ 1 < +∞$
52		breq2	$⊢ B = +∞ \to (1 < B \leftrightarrow 1 < +∞)$
53	51 52	mpbiri	$⊢ B = +∞ \to 1 < B$
54		id	$⊢ (1 < B \to \exists y \in A 1 < y) \to (1 < B \to \exists y \in A 1 < y)$
55	53 54	syl5com	$⊢ B = +∞ \to ((1 < B \to \exists y \in A 1 < y) \to \exists y \in A 1 < y)$
56		mnflt	$⊢ 1 \in ℝ \to −∞ < 1$
57	43 56	ax-mp	$⊢ −∞ < 1$
58		rexr	$⊢ 1 \in ℝ \to 1 \in ℝ^{*}$
59	43 58	ax-mp	$⊢ 1 \in ℝ^{*}$
60		xrlttr	$⊢ (−∞ \in ℝ^{} \land 1 \in ℝ^{} \land y \in ℝ^{*}) \to ((−∞ < 1 \land 1 < y) \to −∞ < y)$
61	33 59 60	mp3an12	$⊢ y \in ℝ^{*} \to ((−∞ < 1 \land 1 < y) \to −∞ < y)$
62	57 61	mpani	$⊢ y \in ℝ^{*} \to (1 < y \to −∞ < y)$
63	35 62	syl	$⊢ (A \subseteq ℝ^{*} \land y \in A) \to (1 < y \to −∞ < y)$
64	63	reximdva	$⊢ A \subseteq ℝ^{*} \to (\exists y \in A 1 < y \to \exists y \in A −∞ < y)$
65	55 64	sylan9r	$⊢ (A \subseteq ℝ^{*} \land B = +∞) \to ((1 < B \to \exists y \in A 1 < y) \to \exists y \in A −∞ < y)$
66	49 65	syl5	$⊢ (A \subseteq ℝ^{*} \land B = +∞) \to (\forall z \in ℝ (z < B \to \exists y \in A z < y) \to \exists y \in A −∞ < y)$
67	66	a1dd	$⊢ (A \subseteq ℝ^{*} \land B = +∞) \to (\forall z \in ℝ (z < B \to \exists y \in A z < y) \to (−∞ < B \to \exists y \in A −∞ < y))$
68		xrltnr	$⊢ −∞ \in ℝ^{*} \to \neg −∞ < −∞$
69	33 68	ax-mp	$⊢ \neg −∞ < −∞$
70		breq2	$⊢ B = −∞ \to (−∞ < B \leftrightarrow −∞ < −∞)$
71	69 70	mtbiri	$⊢ B = −∞ \to \neg −∞ < B$
72	71	adantl	$⊢ (A \subseteq ℝ^{*} \land B = −∞) \to \neg −∞ < B$
73	72	pm2.21d	$⊢ (A \subseteq ℝ^{*} \land B = −∞) \to (−∞ < B \to \exists y \in A −∞ < y)$
74	73	a1d	$⊢ (A \subseteq ℝ^{*} \land B = −∞) \to (\forall z \in ℝ (z < B \to \exists y \in A z < y) \to (−∞ < B \to \exists y \in A −∞ < y))$
75	42 67 74	3jaodan	$⊢ (A \subseteq ℝ^{*} \land (B \in ℝ \lor B = +∞ \lor B = −∞)) \to (\forall z \in ℝ (z < B \to \exists y \in A z < y) \to (−∞ < B \to \exists y \in A −∞ < y))$
76	17 75	sylan2b	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (\forall z \in ℝ (z < B \to \exists y \in A z < y) \to (−∞ < B \to \exists y \in A −∞ < y))$
77	76	imp	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land \forall z \in ℝ (z < B \to \exists y \in A z < y)) \to (−∞ < B \to \exists y \in A −∞ < y)$
78		breq1	$⊢ x = −∞ \to (x < B \leftrightarrow −∞ < B)$
79		breq1	$⊢ x = −∞ \to (x < y \leftrightarrow −∞ < y)$
80	79	rexbidv	$⊢ x = −∞ \to (\exists y \in A x < y \leftrightarrow \exists y \in A −∞ < y)$
81	78 80	imbi12d	$⊢ x = −∞ \to ((x < B \to \exists y \in A x < y) \leftrightarrow (−∞ < B \to \exists y \in A −∞ < y))$
82	77 81	syl5ibrcom	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land \forall z \in ℝ (z < B \to \exists y \in A z < y)) \to (x = −∞ \to (x < B \to \exists y \in A x < y))$
83	82	a1dd	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land \forall z \in ℝ (z < B \to \exists y \in A z < y)) \to (x = −∞ \to ((x \in ℝ \to (x < B \to \exists y \in A x < y)) \to (x < B \to \exists y \in A x < y)))$
84	8 16 83	3jaod	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land \forall z \in ℝ (z < B \to \exists y \in A z < y)) \to ((x \in ℝ \lor x = +∞ \lor x = −∞) \to ((x \in ℝ \to (x < B \to \exists y \in A x < y)) \to (x < B \to \exists y \in A x < y)))$
85	6 84	biimtrid	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land \forall z \in ℝ (z < B \to \exists y \in A z < y)) \to (x \in ℝ^{*} \to ((x \in ℝ \to (x < B \to \exists y \in A x < y)) \to (x < B \to \exists y \in A x < y)))$
86	85	com23	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land \forall z \in ℝ (z < B \to \exists y \in A z < y)) \to ((x \in ℝ \to (x < B \to \exists y \in A x < y)) \to (x \in ℝ^{*} \to (x < B \to \exists y \in A x < y)))$
87	86	ralimdv2	$⊢ ((A \subseteq ℝ^{} \land B \in ℝ^{}) \land \forall z \in ℝ (z < B \to \exists y \in A z < y)) \to (\forall x \in ℝ (x < B \to \exists y \in A x < y) \to \forall x \in ℝ^{*} (x < B \to \exists y \in A x < y))$
88	87	ex	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (\forall z \in ℝ (z < B \to \exists y \in A z < y) \to (\forall x \in ℝ (x < B \to \exists y \in A x < y) \to \forall x \in ℝ^{*} (x < B \to \exists y \in A x < y)))$
89	5 88	biimtrid	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (\forall x \in ℝ (x < B \to \exists y \in A x < y) \to (\forall x \in ℝ (x < B \to \exists y \in A x < y) \to \forall x \in ℝ^{*} (x < B \to \exists y \in A x < y)))$
90	89	pm2.43d	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (\forall x \in ℝ (x < B \to \exists y \in A x < y) \to \forall x \in ℝ^{*} (x < B \to \exists y \in A x < y))$
91		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
92	91	imim1i	$⊢ (x \in ℝ^{*} \to (x < B \to \exists y \in A x < y)) \to (x \in ℝ \to (x < B \to \exists y \in A x < y))$
93	92	ralimi2	$⊢ \forall x \in ℝ^{*} (x < B \to \exists y \in A x < y) \to \forall x \in ℝ (x < B \to \exists y \in A x < y)$
94	90 93	impbid1	$⊢ (A \subseteq ℝ^{} \land B \in ℝ^{}) \to (\forall x \in ℝ (x < B \to \exists y \in A x < y) \leftrightarrow \forall x \in ℝ^{*} (x < B \to \exists y \in A x < y))$

Metamath Proof Explorer

Theorem xrub

Proof