xrinfmsslem

		Ref	Expression
	Assertion	xrinfmsslem	$⊢ (A \subseteq ℝ^{} \land (A \subseteq ℝ \lor −∞ \in A)) \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{*} (x < y \to \exists z \in A z < y))$

Proof

Step	Hyp	Ref	Expression
1		raleq	$⊢ A = \emptyset \to (\forall y \in A \neg y < x \leftrightarrow \forall y \in \emptyset \neg y < x)$
2		rexeq	$⊢ A = \emptyset \to (\exists z \in A z < y \leftrightarrow \exists z \in \emptyset z < y)$
3	2	imbi2d	$⊢ A = \emptyset \to ((x < y \to \exists z \in A z < y) \leftrightarrow (x < y \to \exists z \in \emptyset z < y))$
4	3	ralbidv	$⊢ A = \emptyset \to (\forall y \in ℝ^{} (x < y \to \exists z \in A z < y) \leftrightarrow \forall y \in ℝ^{} (x < y \to \exists z \in \emptyset z < y))$
5	1 4	anbi12d	$⊢ A = \emptyset \to ((\forall y \in A \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in A z < y)) \leftrightarrow (\forall y \in \emptyset \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in \emptyset z < y)))$
6	5	rexbidv	$⊢ A = \emptyset \to (\exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in A z < y)) \leftrightarrow \exists x \in ℝ^{} (\forall y \in \emptyset \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in \emptyset z < y)))$
7		infm3	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to \exists x \in ℝ (\forall y \in A \neg y < x \land \forall y \in ℝ (x < y \to \exists z \in A z < y))$
8		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
9	8	anim1i	$⊢ (x \in ℝ \land (\forall y \in A \neg y < x \land \forall y \in ℝ (x < y \to \exists z \in A z < y))) \to (x \in ℝ^{*} \land (\forall y \in A \neg y < x \land \forall y \in ℝ (x < y \to \exists z \in A z < y)))$
10	9	reximi2	$⊢ \exists x \in ℝ (\forall y \in A \neg y < x \land \forall y \in ℝ (x < y \to \exists z \in A z < y)) \to \exists x \in ℝ^{*} (\forall y \in A \neg y < x \land \forall y \in ℝ (x < y \to \exists z \in A z < y))$
11	7 10	syl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to \exists x \in ℝ^{*} (\forall y \in A \neg y < x \land \forall y \in ℝ (x < y \to \exists z \in A z < y))$
12		elxr	$⊢ y \in ℝ^{*} \leftrightarrow (y \in ℝ \lor y = +∞ \lor y = −∞)$
13		simpr	$⊢ (((A \subseteq ℝ \land A \neq \emptyset) \land x \in ℝ^{*}) \land (y \in ℝ \to (x < y \to \exists z \in A z < y))) \to (y \in ℝ \to (x < y \to \exists z \in A z < y))$
14		ssel	$⊢ A \subseteq ℝ \to (z \in A \to z \in ℝ)$
15		ltpnf	$⊢ z \in ℝ \to z < +∞$
16	14 15	syl6	$⊢ A \subseteq ℝ \to (z \in A \to z < +∞)$
17	16	ancld	$⊢ A \subseteq ℝ \to (z \in A \to (z \in A \land z < +∞))$
18	17	eximdv	$⊢ A \subseteq ℝ \to (\exists z z \in A \to \exists z (z \in A \land z < +∞))$
19		n0	$⊢ A \neq \emptyset \leftrightarrow \exists z z \in A$
20		df-rex	$⊢ \exists z \in A z < +∞ \leftrightarrow \exists z (z \in A \land z < +∞)$
21	18 19 20	3imtr4g	$⊢ A \subseteq ℝ \to (A \neq \emptyset \to \exists z \in A z < +∞)$
22	21	imp	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to \exists z \in A z < +∞$
23	22	a1d	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (x < +∞ \to \exists z \in A z < +∞)$
24	23	ad2antrr	$⊢ (((A \subseteq ℝ \land A \neq \emptyset) \land x \in ℝ^{*}) \land y = +∞) \to (x < +∞ \to \exists z \in A z < +∞)$
25		breq2	$⊢ y = +∞ \to (x < y \leftrightarrow x < +∞)$
26		breq2	$⊢ y = +∞ \to (z < y \leftrightarrow z < +∞)$
27	26	rexbidv	$⊢ y = +∞ \to (\exists z \in A z < y \leftrightarrow \exists z \in A z < +∞)$
28	25 27	imbi12d	$⊢ y = +∞ \to ((x < y \to \exists z \in A z < y) \leftrightarrow (x < +∞ \to \exists z \in A z < +∞))$
29	28	adantl	$⊢ (((A \subseteq ℝ \land A \neq \emptyset) \land x \in ℝ^{*}) \land y = +∞) \to ((x < y \to \exists z \in A z < y) \leftrightarrow (x < +∞ \to \exists z \in A z < +∞))$
30	24 29	mpbird	$⊢ (((A \subseteq ℝ \land A \neq \emptyset) \land x \in ℝ^{*}) \land y = +∞) \to (x < y \to \exists z \in A z < y)$
31	30	ex	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land x \in ℝ^{*}) \to (y = +∞ \to (x < y \to \exists z \in A z < y))$
32	31	adantr	$⊢ (((A \subseteq ℝ \land A \neq \emptyset) \land x \in ℝ^{*}) \land (y \in ℝ \to (x < y \to \exists z \in A z < y))) \to (y = +∞ \to (x < y \to \exists z \in A z < y))$
33		nltmnf	$⊢ x \in ℝ^{*} \to \neg x < −∞$
34	33	adantr	$⊢ (x \in ℝ^{*} \land y = −∞) \to \neg x < −∞$
35		breq2	$⊢ y = −∞ \to (x < y \leftrightarrow x < −∞)$
36	35	notbid	$⊢ y = −∞ \to (\neg x < y \leftrightarrow \neg x < −∞)$
37	36	adantl	$⊢ (x \in ℝ^{*} \land y = −∞) \to (\neg x < y \leftrightarrow \neg x < −∞)$
38	34 37	mpbird	$⊢ (x \in ℝ^{*} \land y = −∞) \to \neg x < y$
39	38	pm2.21d	$⊢ (x \in ℝ^{*} \land y = −∞) \to (x < y \to \exists z \in A z < y)$
40	39	ex	$⊢ x \in ℝ^{*} \to (y = −∞ \to (x < y \to \exists z \in A z < y))$
41	40	ad2antlr	$⊢ (((A \subseteq ℝ \land A \neq \emptyset) \land x \in ℝ^{*}) \land (y \in ℝ \to (x < y \to \exists z \in A z < y))) \to (y = −∞ \to (x < y \to \exists z \in A z < y))$
42	13 32 41	3jaod	$⊢ (((A \subseteq ℝ \land A \neq \emptyset) \land x \in ℝ^{*}) \land (y \in ℝ \to (x < y \to \exists z \in A z < y))) \to ((y \in ℝ \lor y = +∞ \lor y = −∞) \to (x < y \to \exists z \in A z < y))$
43	12 42	syl5bi	$⊢ (((A \subseteq ℝ \land A \neq \emptyset) \land x \in ℝ^{}) \land (y \in ℝ \to (x < y \to \exists z \in A z < y))) \to (y \in ℝ^{} \to (x < y \to \exists z \in A z < y))$
44	43	ex	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land x \in ℝ^{}) \to ((y \in ℝ \to (x < y \to \exists z \in A z < y)) \to (y \in ℝ^{} \to (x < y \to \exists z \in A z < y)))$
45	44	ralimdv2	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land x \in ℝ^{}) \to (\forall y \in ℝ (x < y \to \exists z \in A z < y) \to \forall y \in ℝ^{} (x < y \to \exists z \in A z < y))$
46	45	anim2d	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land x \in ℝ^{}) \to ((\forall y \in A \neg y < x \land \forall y \in ℝ (x < y \to \exists z \in A z < y)) \to (\forall y \in A \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in A z < y)))$
47	46	reximdva	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (\exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ (x < y \to \exists z \in A z < y)) \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{*} (x < y \to \exists z \in A z < y)))$
48	47	3adant3	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to (\exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ (x < y \to \exists z \in A z < y)) \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{*} (x < y \to \exists z \in A z < y)))$
49	11 48	mpd	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in A z < y))$
50	49	3expa	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land \exists x \in ℝ \forall y \in A x \leq y) \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in A z < y))$
51		ralnex	$⊢ \forall x \in ℝ \neg \forall y \in A x \leq y \leftrightarrow \neg \exists x \in ℝ \forall y \in A x \leq y$
52		rexnal	$⊢ \exists y \in A \neg x \leq y \leftrightarrow \neg \forall y \in A x \leq y$
53		ssel2	$⊢ (A \subseteq ℝ \land y \in A) \to y \in ℝ$
54		letric	$⊢ (x \in ℝ \land y \in ℝ) \to (x \leq y \lor y \leq x)$
55	54	ancoms	$⊢ (y \in ℝ \land x \in ℝ) \to (x \leq y \lor y \leq x)$
56	55	ord	$⊢ (y \in ℝ \land x \in ℝ) \to (\neg x \leq y \to y \leq x)$
57	53 56	sylan	$⊢ ((A \subseteq ℝ \land y \in A) \land x \in ℝ) \to (\neg x \leq y \to y \leq x)$
58	57	an32s	$⊢ ((A \subseteq ℝ \land x \in ℝ) \land y \in A) \to (\neg x \leq y \to y \leq x)$
59	58	reximdva	$⊢ (A \subseteq ℝ \land x \in ℝ) \to (\exists y \in A \neg x \leq y \to \exists y \in A y \leq x)$
60	52 59	syl5bir	$⊢ (A \subseteq ℝ \land x \in ℝ) \to (\neg \forall y \in A x \leq y \to \exists y \in A y \leq x)$
61	60	ralimdva	$⊢ A \subseteq ℝ \to (\forall x \in ℝ \neg \forall y \in A x \leq y \to \forall x \in ℝ \exists y \in A y \leq x)$
62	61	imp	$⊢ (A \subseteq ℝ \land \forall x \in ℝ \neg \forall y \in A x \leq y) \to \forall x \in ℝ \exists y \in A y \leq x$
63	51 62	sylan2br	$⊢ (A \subseteq ℝ \land \neg \exists x \in ℝ \forall y \in A x \leq y) \to \forall x \in ℝ \exists y \in A y \leq x$
64		breq1	$⊢ y = z \to (y \leq x \leftrightarrow z \leq x)$
65	64	cbvrexvw	$⊢ \exists y \in A y \leq x \leftrightarrow \exists z \in A z \leq x$
66	65	ralbii	$⊢ \forall x \in ℝ \exists y \in A y \leq x \leftrightarrow \forall x \in ℝ \exists z \in A z \leq x$
67	63 66	sylib	$⊢ (A \subseteq ℝ \land \neg \exists x \in ℝ \forall y \in A x \leq y) \to \forall x \in ℝ \exists z \in A z \leq x$
68		mnfxr	$⊢ −∞ \in ℝ^{*}$
69		ssel	$⊢ A \subseteq ℝ \to (y \in A \to y \in ℝ)$
70		rexr	$⊢ y \in ℝ \to y \in ℝ^{*}$
71		nltmnf	$⊢ y \in ℝ^{*} \to \neg y < −∞$
72	70 71	syl	$⊢ y \in ℝ \to \neg y < −∞$
73	69 72	syl6	$⊢ A \subseteq ℝ \to (y \in A \to \neg y < −∞)$
74	73	ralrimiv	$⊢ A \subseteq ℝ \to \forall y \in A \neg y < −∞$
75	74	adantr	$⊢ (A \subseteq ℝ \land \forall x \in ℝ \exists z \in A z \leq x) \to \forall y \in A \neg y < −∞$
76		peano2rem	$⊢ y \in ℝ \to y - 1 \in ℝ$
77		breq2	$⊢ x = y - 1 \to (z \leq x \leftrightarrow z \leq y - 1)$
78	77	rexbidv	$⊢ x = y - 1 \to (\exists z \in A z \leq x \leftrightarrow \exists z \in A z \leq y - 1)$
79	78	rspcva	$⊢ (y - 1 \in ℝ \land \forall x \in ℝ \exists z \in A z \leq x) \to \exists z \in A z \leq y - 1$
80	79	adantrr	$⊢ (y - 1 \in ℝ \land (\forall x \in ℝ \exists z \in A z \leq x \land A \subseteq ℝ)) \to \exists z \in A z \leq y - 1$
81	80	ancoms	$⊢ ((\forall x \in ℝ \exists z \in A z \leq x \land A \subseteq ℝ) \land y - 1 \in ℝ) \to \exists z \in A z \leq y - 1$
82	76 81	sylan2	$⊢ ((\forall x \in ℝ \exists z \in A z \leq x \land A \subseteq ℝ) \land y \in ℝ) \to \exists z \in A z \leq y - 1$
83		ssel2	$⊢ (A \subseteq ℝ \land z \in A) \to z \in ℝ$
84		ltm1	$⊢ y \in ℝ \to y - 1 < y$
85	84	adantl	$⊢ (z \in ℝ \land y \in ℝ) \to y - 1 < y$
86	76	ancri	$⊢ y \in ℝ \to (y - 1 \in ℝ \land y \in ℝ)$
87		lelttr	$⊢ (z \in ℝ \land y - 1 \in ℝ \land y \in ℝ) \to ((z \leq y - 1 \land y - 1 < y) \to z < y)$
88	87	3expb	$⊢ (z \in ℝ \land (y - 1 \in ℝ \land y \in ℝ)) \to ((z \leq y - 1 \land y - 1 < y) \to z < y)$
89	86 88	sylan2	$⊢ (z \in ℝ \land y \in ℝ) \to ((z \leq y - 1 \land y - 1 < y) \to z < y)$
90	85 89	mpan2d	$⊢ (z \in ℝ \land y \in ℝ) \to (z \leq y - 1 \to z < y)$
91	83 90	sylan	$⊢ ((A \subseteq ℝ \land z \in A) \land y \in ℝ) \to (z \leq y - 1 \to z < y)$
92	91	an32s	$⊢ ((A \subseteq ℝ \land y \in ℝ) \land z \in A) \to (z \leq y - 1 \to z < y)$
93	92	reximdva	$⊢ (A \subseteq ℝ \land y \in ℝ) \to (\exists z \in A z \leq y - 1 \to \exists z \in A z < y)$
94	93	adantll	$⊢ ((\forall x \in ℝ \exists z \in A z \leq x \land A \subseteq ℝ) \land y \in ℝ) \to (\exists z \in A z \leq y - 1 \to \exists z \in A z < y)$
95	82 94	mpd	$⊢ ((\forall x \in ℝ \exists z \in A z \leq x \land A \subseteq ℝ) \land y \in ℝ) \to \exists z \in A z < y$
96	95	exp31	$⊢ \forall x \in ℝ \exists z \in A z \leq x \to (A \subseteq ℝ \to (y \in ℝ \to \exists z \in A z < y))$
97	96	a1dd	$⊢ \forall x \in ℝ \exists z \in A z \leq x \to (A \subseteq ℝ \to (−∞ < y \to (y \in ℝ \to \exists z \in A z < y)))$
98	97	com4r	$⊢ y \in ℝ \to (\forall x \in ℝ \exists z \in A z \leq x \to (A \subseteq ℝ \to (−∞ < y \to \exists z \in A z < y)))$
99		0re	$⊢ 0 \in ℝ$
100		breq2	$⊢ x = 0 \to (z \leq x \leftrightarrow z \leq 0)$
101	100	rexbidv	$⊢ x = 0 \to (\exists z \in A z \leq x \leftrightarrow \exists z \in A z \leq 0)$
102	101	rspcva	$⊢ (0 \in ℝ \land \forall x \in ℝ \exists z \in A z \leq x) \to \exists z \in A z \leq 0$
103	99 102	mpan	$⊢ \forall x \in ℝ \exists z \in A z \leq x \to \exists z \in A z \leq 0$
104	83 15	syl	$⊢ (A \subseteq ℝ \land z \in A) \to z < +∞$
105	104	a1d	$⊢ (A \subseteq ℝ \land z \in A) \to (z \leq 0 \to z < +∞)$
106	105	reximdva	$⊢ A \subseteq ℝ \to (\exists z \in A z \leq 0 \to \exists z \in A z < +∞)$
107	103 106	mpan9	$⊢ (\forall x \in ℝ \exists z \in A z \leq x \land A \subseteq ℝ) \to \exists z \in A z < +∞$
108	107 27	syl5ibr	$⊢ y = +∞ \to ((\forall x \in ℝ \exists z \in A z \leq x \land A \subseteq ℝ) \to \exists z \in A z < y)$
109	108	a1dd	$⊢ y = +∞ \to ((\forall x \in ℝ \exists z \in A z \leq x \land A \subseteq ℝ) \to (−∞ < y \to \exists z \in A z < y))$
110	109	expd	$⊢ y = +∞ \to (\forall x \in ℝ \exists z \in A z \leq x \to (A \subseteq ℝ \to (−∞ < y \to \exists z \in A z < y)))$
111		xrltnr	$⊢ −∞ \in ℝ^{*} \to \neg −∞ < −∞$
112	68 111	ax-mp	$⊢ \neg −∞ < −∞$
113		breq2	$⊢ y = −∞ \to (−∞ < y \leftrightarrow −∞ < −∞)$
114	112 113	mtbiri	$⊢ y = −∞ \to \neg −∞ < y$
115	114	pm2.21d	$⊢ y = −∞ \to (−∞ < y \to \exists z \in A z < y)$
116	115	2a1d	$⊢ y = −∞ \to (\forall x \in ℝ \exists z \in A z \leq x \to (A \subseteq ℝ \to (−∞ < y \to \exists z \in A z < y)))$
117	98 110 116	3jaoi	$⊢ (y \in ℝ \lor y = +∞ \lor y = −∞) \to (\forall x \in ℝ \exists z \in A z \leq x \to (A \subseteq ℝ \to (−∞ < y \to \exists z \in A z < y)))$
118	12 117	sylbi	$⊢ y \in ℝ^{*} \to (\forall x \in ℝ \exists z \in A z \leq x \to (A \subseteq ℝ \to (−∞ < y \to \exists z \in A z < y)))$
119	118	com13	$⊢ A \subseteq ℝ \to (\forall x \in ℝ \exists z \in A z \leq x \to (y \in ℝ^{*} \to (−∞ < y \to \exists z \in A z < y)))$
120	119	imp	$⊢ (A \subseteq ℝ \land \forall x \in ℝ \exists z \in A z \leq x) \to (y \in ℝ^{*} \to (−∞ < y \to \exists z \in A z < y))$
121	120	ralrimiv	$⊢ (A \subseteq ℝ \land \forall x \in ℝ \exists z \in A z \leq x) \to \forall y \in ℝ^{*} (−∞ < y \to \exists z \in A z < y)$
122	75 121	jca	$⊢ (A \subseteq ℝ \land \forall x \in ℝ \exists z \in A z \leq x) \to (\forall y \in A \neg y < −∞ \land \forall y \in ℝ^{*} (−∞ < y \to \exists z \in A z < y))$
123		breq2	$⊢ x = −∞ \to (y < x \leftrightarrow y < −∞)$
124	123	notbid	$⊢ x = −∞ \to (\neg y < x \leftrightarrow \neg y < −∞)$
125	124	ralbidv	$⊢ x = −∞ \to (\forall y \in A \neg y < x \leftrightarrow \forall y \in A \neg y < −∞)$
126		breq1	$⊢ x = −∞ \to (x < y \leftrightarrow −∞ < y)$
127	126	imbi1d	$⊢ x = −∞ \to ((x < y \to \exists z \in A z < y) \leftrightarrow (−∞ < y \to \exists z \in A z < y))$
128	127	ralbidv	$⊢ x = −∞ \to (\forall y \in ℝ^{} (x < y \to \exists z \in A z < y) \leftrightarrow \forall y \in ℝ^{} (−∞ < y \to \exists z \in A z < y))$
129	125 128	anbi12d	$⊢ x = −∞ \to ((\forall y \in A \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in A z < y)) \leftrightarrow (\forall y \in A \neg y < −∞ \land \forall y \in ℝ^{} (−∞ < y \to \exists z \in A z < y)))$
130	129	rspcev	$⊢ (−∞ \in ℝ^{} \land (\forall y \in A \neg y < −∞ \land \forall y \in ℝ^{} (−∞ < y \to \exists z \in A z < y))) \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in A z < y))$
131	68 122 130	sylancr	$⊢ (A \subseteq ℝ \land \forall x \in ℝ \exists z \in A z \leq x) \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in A z < y))$
132	67 131	syldan	$⊢ (A \subseteq ℝ \land \neg \exists x \in ℝ \forall y \in A x \leq y) \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in A z < y))$
133	132	adantlr	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land \neg \exists x \in ℝ \forall y \in A x \leq y) \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in A z < y))$
134	50 133	pm2.61dan	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in A z < y))$
135		pnfxr	$⊢ +∞ \in ℝ^{*}$
136		ral0	$⊢ \forall y \in \emptyset \neg y < +∞$
137		pnfnlt	$⊢ y \in ℝ^{*} \to \neg +∞ < y$
138	137	pm2.21d	$⊢ y \in ℝ^{*} \to (+∞ < y \to \exists z \in \emptyset z < y)$
139	138	rgen	$⊢ \forall y \in ℝ^{*} (+∞ < y \to \exists z \in \emptyset z < y)$
140	136 139	pm3.2i	$⊢ (\forall y \in \emptyset \neg y < +∞ \land \forall y \in ℝ^{*} (+∞ < y \to \exists z \in \emptyset z < y))$
141		breq2	$⊢ x = +∞ \to (y < x \leftrightarrow y < +∞)$
142	141	notbid	$⊢ x = +∞ \to (\neg y < x \leftrightarrow \neg y < +∞)$
143	142	ralbidv	$⊢ x = +∞ \to (\forall y \in \emptyset \neg y < x \leftrightarrow \forall y \in \emptyset \neg y < +∞)$
144		breq1	$⊢ x = +∞ \to (x < y \leftrightarrow +∞ < y)$
145	144	imbi1d	$⊢ x = +∞ \to ((x < y \to \exists z \in \emptyset z < y) \leftrightarrow (+∞ < y \to \exists z \in \emptyset z < y))$
146	145	ralbidv	$⊢ x = +∞ \to (\forall y \in ℝ^{} (x < y \to \exists z \in \emptyset z < y) \leftrightarrow \forall y \in ℝ^{} (+∞ < y \to \exists z \in \emptyset z < y))$
147	143 146	anbi12d	$⊢ x = +∞ \to ((\forall y \in \emptyset \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in \emptyset z < y)) \leftrightarrow (\forall y \in \emptyset \neg y < +∞ \land \forall y \in ℝ^{} (+∞ < y \to \exists z \in \emptyset z < y)))$
148	147	rspcev	$⊢ (+∞ \in ℝ^{} \land (\forall y \in \emptyset \neg y < +∞ \land \forall y \in ℝ^{} (+∞ < y \to \exists z \in \emptyset z < y))) \to \exists x \in ℝ^{} (\forall y \in \emptyset \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in \emptyset z < y))$
149	135 140 148	mp2an	$⊢ \exists x \in ℝ^{} (\forall y \in \emptyset \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in \emptyset z < y))$
150	149	a1i	$⊢ A \subseteq ℝ \to \exists x \in ℝ^{} (\forall y \in \emptyset \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in \emptyset z < y))$
151	6 134 150	pm2.61ne	$⊢ A \subseteq ℝ \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{} (x < y \to \exists z \in A z < y))$
152	151	adantl	$⊢ (A \subseteq ℝ^{} \land A \subseteq ℝ) \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{*} (x < y \to \exists z \in A z < y))$
153		ssel	$⊢ A \subseteq ℝ^{} \to (y \in A \to y \in ℝ^{})$
154	153 71	syl6	$⊢ A \subseteq ℝ^{*} \to (y \in A \to \neg y < −∞)$
155	154	ralrimiv	$⊢ A \subseteq ℝ^{*} \to \forall y \in A \neg y < −∞$
156		breq1	$⊢ z = −∞ \to (z < y \leftrightarrow −∞ < y)$
157	156	rspcev	$⊢ (−∞ \in A \land −∞ < y) \to \exists z \in A z < y$
158	157	ex	$⊢ −∞ \in A \to (−∞ < y \to \exists z \in A z < y)$
159	158	ralrimivw	$⊢ −∞ \in A \to \forall y \in ℝ^{*} (−∞ < y \to \exists z \in A z < y)$
160	155 159	anim12i	$⊢ (A \subseteq ℝ^{} \land −∞ \in A) \to (\forall y \in A \neg y < −∞ \land \forall y \in ℝ^{} (−∞ < y \to \exists z \in A z < y))$
161	68 160 130	sylancr	$⊢ (A \subseteq ℝ^{} \land −∞ \in A) \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{*} (x < y \to \exists z \in A z < y))$
162	152 161	jaodan	$⊢ (A \subseteq ℝ^{} \land (A \subseteq ℝ \lor −∞ \in A)) \to \exists x \in ℝ^{} (\forall y \in A \neg y < x \land \forall y \in ℝ^{*} (x < y \to \exists z \in A z < y))$

Metamath Proof Explorer

Theorem xrinfmsslem

Proof