supminfxr2

Description: The extended real suprema of a set of extended reals is the extended real negative of the extended real infima of that set's image under extended real negation. (Contributed by Glauco Siliprandi, 2-Jan-2022)

		Ref	Expression
	Hypothesis	supminfxr2.1	$⊢ φ \to A \subseteq ℝ^{*}$
	Assertion	supminfxr2	$⊢ φ \to sup (A ℝ^{} <) = - inf (\{x \in ℝ^{} \| - x \in A\} ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		supminfxr2.1	$⊢ φ \to A \subseteq ℝ^{*}$
2		xnegmnf	$⊢ - −∞ = +∞$
3	2	eqcomi	$⊢ +∞ = - −∞$
4	3	a1i	$⊢ (φ \land +∞ \in A) \to +∞ = - −∞$
5		supxrpnf	$⊢ (A \subseteq ℝ^{} \land +∞ \in A) \to sup (A ℝ^{} <) = +∞$
6	1 5	sylan	$⊢ (φ \land +∞ \in A) \to sup (A ℝ^{*} <) = +∞$
7		ssrab2	$⊢ \{y \in ℝ^{} \| - y \in A\} \subseteq ℝ^{}$
8	7	a1i	$⊢ +∞ \in A \to \{y \in ℝ^{} \| - y \in A\} \subseteq ℝ^{}$
9		xnegeq	$⊢ y = −∞ \to - y = - −∞$
10	2	a1i	$⊢ y = −∞ \to - −∞ = +∞$
11	9 10	eqtrd	$⊢ y = −∞ \to - y = +∞$
12	11	eleq1d	$⊢ y = −∞ \to (- y \in A \leftrightarrow +∞ \in A)$
13		mnfxr	$⊢ −∞ \in ℝ^{*}$
14	13	a1i	$⊢ +∞ \in A \to −∞ \in ℝ^{*}$
15		id	$⊢ +∞ \in A \to +∞ \in A$
16	12 14 15	elrabd	$⊢ +∞ \in A \to −∞ \in \{y \in ℝ^{*} \| - y \in A\}$
17		infxrmnf	$⊢ (\{y \in ℝ^{} \| - y \in A\} \subseteq ℝ^{} \land −∞ \in \{y \in ℝ^{} \| - y \in A\}) \to inf (\{y \in ℝ^{} \| - y \in A\} ℝ^{*} <) = −∞$
18	8 16 17	syl2anc	$⊢ +∞ \in A \to inf (\{y \in ℝ^{} \| - y \in A\} ℝ^{} <) = −∞$
19	18	adantl	$⊢ (φ \land +∞ \in A) \to inf (\{y \in ℝ^{} \| - y \in A\} ℝ^{} <) = −∞$
20	19	xnegeqd	$⊢ (φ \land +∞ \in A) \to - inf (\{y \in ℝ^{} \| - y \in A\} ℝ^{} <) = - −∞$
21	4 6 20	3eqtr4d	$⊢ (φ \land +∞ \in A) \to sup (A ℝ^{} <) = - inf (\{y \in ℝ^{} \| - y \in A\} ℝ^{*} <)$
22	1	ssdifssd	$⊢ φ \to A ∖ \{−∞\} \subseteq ℝ^{*}$
23	22	adantr	$⊢ (φ \land \neg +∞ \in A) \to A ∖ \{−∞\} \subseteq ℝ^{*}$
24		difssd	$⊢ \neg +∞ \in A \to A ∖ \{−∞\} \subseteq A$
25		id	$⊢ \neg +∞ \in A \to \neg +∞ \in A$
26		ssnel	$⊢ (A ∖ \{−∞\} \subseteq A \land \neg +∞ \in A) \to \neg +∞ \in (A ∖ \{−∞\})$
27	24 25 26	syl2anc	$⊢ \neg +∞ \in A \to \neg +∞ \in (A ∖ \{−∞\})$
28	27	adantl	$⊢ (φ \land \neg +∞ \in A) \to \neg +∞ \in (A ∖ \{−∞\})$
29		neldifsnd	$⊢ (φ \land \neg +∞ \in A) \to \neg −∞ \in (A ∖ \{−∞\})$
30	23 28 29	xrssre	$⊢ (φ \land \neg +∞ \in A) \to A ∖ \{−∞\} \subseteq ℝ$
31	30	supminfxr	$⊢ (φ \land \neg +∞ \in A) \to sup (A ∖ \{−∞\} ℝ^{} <) = - inf (\{y \in ℝ \| - y \in (A ∖ \{−∞\})\} ℝ^{} <)$
32		supxrmnf2	$⊢ A \subseteq ℝ^{} \to sup (A ∖ \{−∞\} ℝ^{} <) = sup (A ℝ^{*} <)$
33	1 32	syl	$⊢ φ \to sup (A ∖ \{−∞\} ℝ^{} <) = sup (A ℝ^{} <)$
34	33	eqcomd	$⊢ φ \to sup (A ℝ^{} <) = sup (A ∖ \{−∞\} ℝ^{} <)$
35	34	adantr	$⊢ (φ \land \neg +∞ \in A) \to sup (A ℝ^{} <) = sup (A ∖ \{−∞\} ℝ^{} <)$
36		rexr	$⊢ y \in ℝ \to y \in ℝ^{*}$
37	36	adantr	$⊢ (y \in ℝ \land - y \in (A ∖ \{−∞\})) \to y \in ℝ^{*}$
38		simpl	$⊢ (y \in ℝ \land - y \in (A ∖ \{−∞\})) \to y \in ℝ$
39	38	rexnegd	$⊢ (y \in ℝ \land - y \in (A ∖ \{−∞\})) \to - y = - y$
40		eldifi	$⊢ - y \in (A ∖ \{−∞\}) \to - y \in A$
41	40	adantl	$⊢ (y \in ℝ \land - y \in (A ∖ \{−∞\})) \to - y \in A$
42	39 41	eqeltrd	$⊢ (y \in ℝ \land - y \in (A ∖ \{−∞\})) \to - y \in A$
43	37 42	jca	$⊢ (y \in ℝ \land - y \in (A ∖ \{−∞\})) \to (y \in ℝ^{*} \land - y \in A)$
44		rabid	$⊢ y \in \{y \in ℝ^{} \| - y \in A\} \leftrightarrow (y \in ℝ^{} \land - y \in A)$
45	43 44	sylibr	$⊢ (y \in ℝ \land - y \in (A ∖ \{−∞\})) \to y \in \{y \in ℝ^{*} \| - y \in A\}$
46		renepnf	$⊢ y \in ℝ \to y \neq +∞$
47		elsni	$⊢ y \in \{+∞\} \to y = +∞$
48	47	necon3ai	$⊢ y \neq +∞ \to \neg y \in \{+∞\}$
49	46 48	syl	$⊢ y \in ℝ \to \neg y \in \{+∞\}$
50	38 49	syl	$⊢ (y \in ℝ \land - y \in (A ∖ \{−∞\})) \to \neg y \in \{+∞\}$
51	45 50	eldifd	$⊢ (y \in ℝ \land - y \in (A ∖ \{−∞\})) \to y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\})$
52	51	ex	$⊢ y \in ℝ \to (- y \in (A ∖ \{−∞\}) \to y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\}))$
53	52	rgen	$⊢ \forall y \in ℝ (- y \in (A ∖ \{−∞\}) \to y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\}))$
54	53	a1i	$⊢ \neg +∞ \in A \to \forall y \in ℝ (- y \in (A ∖ \{−∞\}) \to y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\}))$
55		nfrab1	$⊢ \underline{Ⅎ} y \{y \in ℝ^{*} \| - y \in A\}$
56		nfcv	$⊢ \underline{Ⅎ} y \{+∞\}$
57	55 56	nfdif	$⊢ \underline{Ⅎ} y (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\})$
58	57	rabssf	$⊢ \{y \in ℝ \| - y \in (A ∖ \{−∞\})\} \subseteq \{y \in ℝ^{} \| - y \in A\} ∖ \{+∞\} \leftrightarrow \forall y \in ℝ (- y \in (A ∖ \{−∞\}) \to y \in (\{y \in ℝ^{} \| - y \in A\} ∖ \{+∞\}))$
59	54 58	sylibr	$⊢ \neg +∞ \in A \to \{y \in ℝ \| - y \in (A ∖ \{−∞\})\} \subseteq \{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\}$
60		nfv	$⊢ Ⅎ y \neg +∞ \in A$
61		nfcv	$⊢ \underline{Ⅎ} y ℝ$
62		eldifi	$⊢ y \in (\{y \in ℝ^{} \| - y \in A\} ∖ \{+∞\}) \to y \in \{y \in ℝ^{} \| - y \in A\}$
63	7 62	sselid	$⊢ y \in (\{y \in ℝ^{} \| - y \in A\} ∖ \{+∞\}) \to y \in ℝ^{}$
64	63	adantl	$⊢ (\neg +∞ \in A \land y \in (\{y \in ℝ^{} \| - y \in A\} ∖ \{+∞\})) \to y \in ℝ^{}$
65	44	simprbi	$⊢ y \in \{y \in ℝ^{*} \| - y \in A\} \to - y \in A$
66	62 65	syl	$⊢ y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\}) \to - y \in A$
67	12	biimpac	$⊢ (- y \in A \land y = −∞) \to +∞ \in A$
68	67	adantll	$⊢ ((\neg +∞ \in A \land - y \in A) \land y = −∞) \to +∞ \in A$
69		simpll	$⊢ ((\neg +∞ \in A \land - y \in A) \land y = −∞) \to \neg +∞ \in A$
70	68 69	pm2.65da	$⊢ (\neg +∞ \in A \land - y \in A) \to \neg y = −∞$
71	70	neqned	$⊢ (\neg +∞ \in A \land - y \in A) \to y \neq −∞$
72	66 71	sylan2	$⊢ (\neg +∞ \in A \land y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\})) \to y \neq −∞$
73		eldifsni	$⊢ y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\}) \to y \neq +∞$
74	73	adantl	$⊢ (\neg +∞ \in A \land y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\})) \to y \neq +∞$
75	64 72 74	xrred	$⊢ (\neg +∞ \in A \land y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\})) \to y \in ℝ$
76	60 57 61 75	ssdf2	$⊢ \neg +∞ \in A \to \{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\} \subseteq ℝ$
77	75	rexnegd	$⊢ (\neg +∞ \in A \land y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\})) \to - y = - y$
78	66	adantl	$⊢ (\neg +∞ \in A \land y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\})) \to - y \in A$
79	63	adantr	$⊢ (y \in (\{y \in ℝ^{} \| - y \in A\} ∖ \{+∞\}) \land - y \in \{−∞\}) \to y \in ℝ^{}$
80		elsni	$⊢ - y \in \{−∞\} \to - y = −∞$
81	80	adantl	$⊢ (y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\}) \land - y \in \{−∞\}) \to - y = −∞$
82		xnegeq	$⊢ - y = −∞ \to - (- y) = - −∞$
83	2	a1i	$⊢ - y = −∞ \to - −∞ = +∞$
84	82 83	eqtr2d	$⊢ - y = −∞ \to +∞ = - (- y)$
85	84	adantl	$⊢ (y \in ℝ^{*} \land - y = −∞) \to +∞ = - (- y)$
86		xnegneg	$⊢ y \in ℝ^{*} \to - (- y) = y$
87	86	adantr	$⊢ (y \in ℝ^{*} \land - y = −∞) \to - (- y) = y$
88	85 87	eqtr2d	$⊢ (y \in ℝ^{*} \land - y = −∞) \to y = +∞$
89	79 81 88	syl2anc	$⊢ (y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\}) \land - y \in \{−∞\}) \to y = +∞$
90	73	neneqd	$⊢ y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\}) \to \neg y = +∞$
91	90	adantr	$⊢ (y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\}) \land - y \in \{−∞\}) \to \neg y = +∞$
92	89 91	pm2.65da	$⊢ y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\}) \to \neg - y \in \{−∞\}$
93	92	adantl	$⊢ (\neg +∞ \in A \land y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\})) \to \neg - y \in \{−∞\}$
94	78 93	eldifd	$⊢ (\neg +∞ \in A \land y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\})) \to - y \in (A ∖ \{−∞\})$
95	77 94	eqeltrrd	$⊢ (\neg +∞ \in A \land y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\})) \to - y \in (A ∖ \{−∞\})$
96	95	ralrimiva	$⊢ \neg +∞ \in A \to \forall y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\}) - y \in (A ∖ \{−∞\})$
97	76 96	jca	$⊢ \neg +∞ \in A \to (\{y \in ℝ^{} \| - y \in A\} ∖ \{+∞\} \subseteq ℝ \land \forall y \in (\{y \in ℝ^{} \| - y \in A\} ∖ \{+∞\}) - y \in (A ∖ \{−∞\}))$
98	57 61	ssrabf	$⊢ \{y \in ℝ^{} \| - y \in A\} ∖ \{+∞\} \subseteq \{y \in ℝ \| - y \in (A ∖ \{−∞\})\} \leftrightarrow (\{y \in ℝ^{} \| - y \in A\} ∖ \{+∞\} \subseteq ℝ \land \forall y \in (\{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\}) - y \in (A ∖ \{−∞\}))$
99	97 98	sylibr	$⊢ \neg +∞ \in A \to \{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\} \subseteq \{y \in ℝ \| - y \in (A ∖ \{−∞\})\}$
100	59 99	eqssd	$⊢ \neg +∞ \in A \to \{y \in ℝ \| - y \in (A ∖ \{−∞\})\} = \{y \in ℝ^{*} \| - y \in A\} ∖ \{+∞\}$
101	100	infeq1d	$⊢ \neg +∞ \in A \to inf (\{y \in ℝ \| - y \in (A ∖ \{−∞\})\} ℝ^{} <) = inf (\{y \in ℝ^{} \| - y \in A\} ∖ \{+∞\} ℝ^{*} <)$
102		infxrpnf2	$⊢ \{y \in ℝ^{} \| - y \in A\} \subseteq ℝ^{} \to inf (\{y \in ℝ^{} \| - y \in A\} ∖ \{+∞\} ℝ^{} <) = inf (\{y \in ℝ^{} \| - y \in A\} ℝ^{} <)$
103	7 102	ax-mp	$⊢ inf (\{y \in ℝ^{} \| - y \in A\} ∖ \{+∞\} ℝ^{} <) = inf (\{y \in ℝ^{} \| - y \in A\} ℝ^{} <)$
104	103	a1i	$⊢ \neg +∞ \in A \to inf (\{y \in ℝ^{} \| - y \in A\} ∖ \{+∞\} ℝ^{} <) = inf (\{y \in ℝ^{} \| - y \in A\} ℝ^{} <)$
105	101 104	eqtr2d	$⊢ \neg +∞ \in A \to inf (\{y \in ℝ^{} \| - y \in A\} ℝ^{} <) = inf (\{y \in ℝ \| - y \in (A ∖ \{−∞\})\} ℝ^{*} <)$
106	105	xnegeqd	$⊢ \neg +∞ \in A \to - inf (\{y \in ℝ^{} \| - y \in A\} ℝ^{} <) = - inf (\{y \in ℝ \| - y \in (A ∖ \{−∞\})\} ℝ^{*} <)$
107	106	adantl	$⊢ (φ \land \neg +∞ \in A) \to - inf (\{y \in ℝ^{} \| - y \in A\} ℝ^{} <) = - inf (\{y \in ℝ \| - y \in (A ∖ \{−∞\})\} ℝ^{*} <)$
108	31 35 107	3eqtr4d	$⊢ (φ \land \neg +∞ \in A) \to sup (A ℝ^{} <) = - inf (\{y \in ℝ^{} \| - y \in A\} ℝ^{*} <)$
109	21 108	pm2.61dan	$⊢ φ \to sup (A ℝ^{} <) = - inf (\{y \in ℝ^{} \| - y \in A\} ℝ^{*} <)$
110		xnegeq	$⊢ y = x \to - y = - x$
111	110	eleq1d	$⊢ y = x \to (- y \in A \leftrightarrow - x \in A)$
112	111	cbvrabv	$⊢ \{y \in ℝ^{} \| - y \in A\} = \{x \in ℝ^{} \| - x \in A\}$
113	112	infeq1i	$⊢ inf (\{y \in ℝ^{} \| - y \in A\} ℝ^{} <) = inf (\{x \in ℝ^{} \| - x \in A\} ℝ^{} <)$
114	113	xnegeqi	$⊢ - inf (\{y \in ℝ^{} \| - y \in A\} ℝ^{} <) = - inf (\{x \in ℝ^{} \| - x \in A\} ℝ^{} <)$
115	114	a1i	$⊢ φ \to - inf (\{y \in ℝ^{} \| - y \in A\} ℝ^{} <) = - inf (\{x \in ℝ^{} \| - x \in A\} ℝ^{} <)$
116	109 115	eqtrd	$⊢ φ \to sup (A ℝ^{} <) = - inf (\{x \in ℝ^{} \| - x \in A\} ℝ^{*} <)$

Metamath Proof Explorer

Theorem supminfxr2

Proof