xrsupsslem

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

Proof

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

Metamath Proof Explorer

Theorem xrsupsslem

Proof