infrenegsup

Description: The infimum of a set of reals A is the negative of the supremum of the negatives of its elements. The antecedent ensures that A is nonempty and has a lower bound. (Contributed by NM, 14-Jun-2005) (Revised by AV, 4-Sep-2020)

		Ref	Expression
	Assertion	infrenegsup	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to sup (A ℝ <) = - sup (\{z \in ℝ \| - z \in A\} ℝ <)$

Proof

Step	Hyp	Ref	Expression
1		infrecl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to sup (A ℝ <) \in ℝ$
2	1	recnd	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to sup (A ℝ <) \in ℂ$
3	2	negnegd	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to - (- sup (A ℝ <)) = sup (A ℝ <)$
4		negeq	$⊢ w = z \to - w = - z$
5	4	cbvmptv	$⊢ (w \in ℝ ⟼ - w) = (z \in ℝ ⟼ - z)$
6	5	mptpreima	$⊢ {(w \in ℝ ⟼ - w)}^{-1} [A] = \{z \in ℝ \| - z \in A\}$
7		eqid	$⊢ (w \in ℝ ⟼ - w) = (w \in ℝ ⟼ - w)$
8	7	negiso	$⊢ ((w \in ℝ ⟼ - w) {Isom}_{<, <^{-1}} (ℝ, ℝ) \land {(w \in ℝ ⟼ - w)}^{-1} = (w \in ℝ ⟼ - w))$
9	8	simpri	$⊢ {(w \in ℝ ⟼ - w)}^{-1} = (w \in ℝ ⟼ - w)$
10	9	imaeq1i	$⊢ {(w \in ℝ ⟼ - w)}^{-1} [A] = (w \in ℝ ⟼ - w) [A]$
11	6 10	eqtr3i	$⊢ \{z \in ℝ \| - z \in A\} = (w \in ℝ ⟼ - w) [A]$
12	11	supeq1i	$⊢ sup (\{z \in ℝ \| - z \in A\} ℝ <) = sup ((w \in ℝ ⟼ - w) [A] ℝ <)$
13	8	simpli	$⊢ (w \in ℝ ⟼ - w) {Isom}_{<, <^{-1}} (ℝ, ℝ)$
14		isocnv	$⊢ (w \in ℝ ⟼ - w) {Isom}_{<, <^{-1}} (ℝ, ℝ) \to {(w \in ℝ ⟼ - w)}^{-1} {Isom}_{<^{-1}, <} (ℝ, ℝ)$
15	13 14	ax-mp	$⊢ {(w \in ℝ ⟼ - w)}^{-1} {Isom}_{<^{-1}, <} (ℝ, ℝ)$
16		isoeq1	$⊢ {(w \in ℝ ⟼ - w)}^{-1} = (w \in ℝ ⟼ - w) \to ({(w \in ℝ ⟼ - w)}^{-1} {Isom}_{<^{-1}, <} (ℝ, ℝ) \leftrightarrow (w \in ℝ ⟼ - w) {Isom}_{<^{-1}, <} (ℝ, ℝ))$
17	9 16	ax-mp	$⊢ {(w \in ℝ ⟼ - w)}^{-1} {Isom}_{<^{-1}, <} (ℝ, ℝ) \leftrightarrow (w \in ℝ ⟼ - w) {Isom}_{<^{-1}, <} (ℝ, ℝ)$
18	15 17	mpbi	$⊢ (w \in ℝ ⟼ - w) {Isom}_{<^{-1}, <} (ℝ, ℝ)$
19	18	a1i	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to (w \in ℝ ⟼ - w) {Isom}_{<^{-1}, <} (ℝ, ℝ)$
20		simp1	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to A \subseteq ℝ$
21		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))$
22		vex	$⊢ x \in V$
23		vex	$⊢ y \in V$
24	22 23	brcnv	$⊢ x <^{-1} y \leftrightarrow y < x$
25	24	notbii	$⊢ \neg x <^{-1} y \leftrightarrow \neg y < x$
26	25	ralbii	$⊢ \forall y \in A \neg x <^{-1} y \leftrightarrow \forall y \in A \neg y < x$
27	23 22	brcnv	$⊢ y <^{-1} x \leftrightarrow x < y$
28		vex	$⊢ z \in V$
29	23 28	brcnv	$⊢ y <^{-1} z \leftrightarrow z < y$
30	29	rexbii	$⊢ \exists z \in A y <^{-1} z \leftrightarrow \exists z \in A z < y$
31	27 30	imbi12i	$⊢ (y <^{-1} x \to \exists z \in A y <^{-1} z) \leftrightarrow (x < y \to \exists z \in A z < y)$
32	31	ralbii	$⊢ \forall y \in ℝ (y <^{-1} x \to \exists z \in A y <^{-1} z) \leftrightarrow \forall y \in ℝ (x < y \to \exists z \in A z < y)$
33	26 32	anbi12i	$⊢ (\forall y \in A \neg x <^{-1} y \land \forall y \in ℝ (y <^{-1} x \to \exists z \in A y <^{-1} z)) \leftrightarrow (\forall y \in A \neg y < x \land \forall y \in ℝ (x < y \to \exists z \in A z < y))$
34	33	rexbii	$⊢ \exists x \in ℝ (\forall y \in A \neg x <^{-1} y \land \forall y \in ℝ (y <^{-1} x \to \exists z \in A y <^{-1} z)) \leftrightarrow \exists x \in ℝ (\forall y \in A \neg y < x \land \forall y \in ℝ (x < y \to \exists z \in A z < y))$
35	21 34	sylibr	$⊢ (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 x <^{-1} y \land \forall y \in ℝ (y <^{-1} x \to \exists z \in A y <^{-1} z))$
36		gtso	$⊢ <^{-1} Or ℝ$
37	36	a1i	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to <^{-1} Or ℝ$
38	19 20 35 37	supiso	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to sup ((w \in ℝ ⟼ - w) [A] ℝ <) = (w \in ℝ ⟼ - w) (sup (A, ℝ, <^{-1}))$
39	12 38	syl5eq	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to sup (\{z \in ℝ \| - z \in A\} ℝ <) = (w \in ℝ ⟼ - w) (sup (A, ℝ, <^{-1}))$
40		df-inf	$⊢ sup (A ℝ <) = sup (A, ℝ, <^{-1})$
41	40	eqcomi	$⊢ sup (A, ℝ, <^{-1}) = sup (A ℝ <)$
42	41	fveq2i	$⊢ (w \in ℝ ⟼ - w) (sup (A, ℝ, <^{-1})) = (w \in ℝ ⟼ - w) (sup (A ℝ <))$
43		negeq	$⊢ w = sup (A ℝ <) \to - w = - sup (A ℝ <)$
44		negex	$⊢ - sup (A ℝ <) \in V$
45	43 7 44	fvmpt	$⊢ sup (A ℝ <) \in ℝ \to (w \in ℝ ⟼ - w) (sup (A ℝ <)) = - sup (A ℝ <)$
46	42 45	syl5eq	$⊢ sup (A ℝ <) \in ℝ \to (w \in ℝ ⟼ - w) (sup (A, ℝ, <^{-1})) = - sup (A ℝ <)$
47	1 46	syl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to (w \in ℝ ⟼ - w) (sup (A, ℝ, <^{-1})) = - sup (A ℝ <)$
48	39 47	eqtr2d	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to - sup (A ℝ <) = sup (\{z \in ℝ \| - z \in A\} ℝ <)$
49	48	negeqd	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to - (- sup (A ℝ <)) = - sup (\{z \in ℝ \| - z \in A\} ℝ <)$
50	3 49	eqtr3d	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A x \leq y) \to sup (A ℝ <) = - sup (\{z \in ℝ \| - z \in A\} ℝ <)$

Metamath Proof Explorer

Theorem infrenegsup

Proof