supminfxrrnmpt

Description: The indexed supremum of a set of reals is the negation of the indexed infimum of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	supminfxrrnmpt.x	$⊢ Ⅎ x φ$
	supminfxrrnmpt.b	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
Assertion	supminfxrrnmpt	$⊢ φ \to sup (ran (x \in A ⟼ B) ℝ^{} <) = - inf (ran (x \in A ⟼ - B) ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		supminfxrrnmpt.x	$⊢ Ⅎ x φ$
2		supminfxrrnmpt.b	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
3		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
4	1 3 2	rnmptssd	$⊢ φ \to ran (x \in A ⟼ B) \subseteq ℝ^{*}$
5	4	supminfxr2	$⊢ φ \to sup (ran (x \in A ⟼ B) ℝ^{} <) = - inf (\{y \in ℝ^{} \| - y \in ran (x \in A ⟼ B)\} ℝ^{*} <)$
6		xnegex	$⊢ - y \in V$
7	3	elrnmpt	$⊢ - y \in V \to (- y \in ran (x \in A ⟼ B) \leftrightarrow \exists x \in A - y = B)$
8	6 7	ax-mp	$⊢ - y \in ran (x \in A ⟼ B) \leftrightarrow \exists x \in A - y = B$
9	8	biimpi	$⊢ - y \in ran (x \in A ⟼ B) \to \exists x \in A - y = B$
10		eqid	$⊢ (x \in A ⟼ - B) = (x \in A ⟼ - B)$
11		xnegneg	$⊢ y \in ℝ^{*} \to - (- y) = y$
12	11	eqcomd	$⊢ y \in ℝ^{*} \to y = - (- y)$
13	12	adantr	$⊢ (y \in ℝ^{*} \land - y = B) \to y = - (- y)$
14		xnegeq	$⊢ - y = B \to - (- y) = - B$
15	14	adantl	$⊢ (y \in ℝ^{*} \land - y = B) \to - (- y) = - B$
16	13 15	eqtrd	$⊢ (y \in ℝ^{*} \land - y = B) \to y = - B$
17	16	ex	$⊢ y \in ℝ^{*} \to (- y = B \to y = - B)$
18	17	reximdv	$⊢ y \in ℝ^{*} \to (\exists x \in A - y = B \to \exists x \in A y = - B)$
19	18	imp	$⊢ (y \in ℝ^{*} \land \exists x \in A - y = B) \to \exists x \in A y = - B$
20		simpl	$⊢ (y \in ℝ^{} \land \exists x \in A - y = B) \to y \in ℝ^{}$
21	10 19 20	elrnmptd	$⊢ (y \in ℝ^{*} \land \exists x \in A - y = B) \to y \in ran (x \in A ⟼ - B)$
22	9 21	sylan2	$⊢ (y \in ℝ^{*} \land - y \in ran (x \in A ⟼ B)) \to y \in ran (x \in A ⟼ - B)$
23	22	ex	$⊢ y \in ℝ^{*} \to (- y \in ran (x \in A ⟼ B) \to y \in ran (x \in A ⟼ - B))$
24	23	rgen	$⊢ \forall y \in ℝ^{*} (- y \in ran (x \in A ⟼ B) \to y \in ran (x \in A ⟼ - B))$
25		rabss	$⊢ \{y \in ℝ^{} \| - y \in ran (x \in A ⟼ B)\} \subseteq ran (x \in A ⟼ - B) \leftrightarrow \forall y \in ℝ^{} (- y \in ran (x \in A ⟼ B) \to y \in ran (x \in A ⟼ - B))$
26	25	biimpri	$⊢ \forall y \in ℝ^{} (- y \in ran (x \in A ⟼ B) \to y \in ran (x \in A ⟼ - B)) \to \{y \in ℝ^{} \| - y \in ran (x \in A ⟼ B)\} \subseteq ran (x \in A ⟼ - B)$
27	24 26	ax-mp	$⊢ \{y \in ℝ^{*} \| - y \in ran (x \in A ⟼ B)\} \subseteq ran (x \in A ⟼ - B)$
28	27	a1i	$⊢ φ \to \{y \in ℝ^{*} \| - y \in ran (x \in A ⟼ B)\} \subseteq ran (x \in A ⟼ - B)$
29		nfcv	$⊢ \underline{Ⅎ} x (- y)$
30		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
31	30	nfrn	$⊢ \underline{Ⅎ} x ran (x \in A ⟼ B)$
32	29 31	nfel	$⊢ Ⅎ x - y \in ran (x \in A ⟼ B)$
33		nfcv	$⊢ \underline{Ⅎ} x ℝ^{*}$
34	32 33	nfrabw	$⊢ \underline{Ⅎ} x \{y \in ℝ^{*} \| - y \in ran (x \in A ⟼ B)\}$
35		xnegeq	$⊢ y = - B \to - y = - (- B)$
36	35	eleq1d	$⊢ y = - B \to (- y \in ran (x \in A ⟼ B) \leftrightarrow - (- B) \in ran (x \in A ⟼ B))$
37	2	xnegcld	$⊢ (φ \land x \in A) \to - B \in ℝ^{*}$
38		xnegneg	$⊢ B \in ℝ^{*} \to - (- B) = B$
39	2 38	syl	$⊢ (φ \land x \in A) \to - (- B) = B$
40		simpr	$⊢ (φ \land x \in A) \to x \in A$
41	3 40 2	elrnmpt1d	$⊢ (φ \land x \in A) \to B \in ran (x \in A ⟼ B)$
42	39 41	eqeltrd	$⊢ (φ \land x \in A) \to - (- B) \in ran (x \in A ⟼ B)$
43	36 37 42	elrabd	$⊢ (φ \land x \in A) \to - B \in \{y \in ℝ^{*} \| - y \in ran (x \in A ⟼ B)\}$
44	1 34 10 43	rnmptssdf	$⊢ φ \to ran (x \in A ⟼ - B) \subseteq \{y \in ℝ^{*} \| - y \in ran (x \in A ⟼ B)\}$
45	28 44	eqssd	$⊢ φ \to \{y \in ℝ^{*} \| - y \in ran (x \in A ⟼ B)\} = ran (x \in A ⟼ - B)$
46	45	infeq1d	$⊢ φ \to inf (\{y \in ℝ^{} \| - y \in ran (x \in A ⟼ B)\} ℝ^{} <) = inf (ran (x \in A ⟼ - B) ℝ^{*} <)$
47	46	xnegeqd	$⊢ φ \to - inf (\{y \in ℝ^{} \| - y \in ran (x \in A ⟼ B)\} ℝ^{} <) = - inf (ran (x \in A ⟼ - B) ℝ^{*} <)$
48	5 47	eqtrd	$⊢ φ \to sup (ran (x \in A ⟼ B) ℝ^{} <) = - inf (ran (x \in A ⟼ - B) ℝ^{} <)$

Metamath Proof Explorer

Theorem supminfxrrnmpt

Proof