supxrre

Description: The real and extended real suprema match when the real supremum exists. (Contributed by NM, 18-Oct-2005) (Proof shortened by Mario Carneiro, 7-Sep-2014)

		Ref	Expression
	Assertion	supxrre	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ^{*} <) = sup (A ℝ <)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to A \subseteq ℝ$
2		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
3	1 2	sstrdi	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to A \subseteq ℝ^{*}$
4		supxrcl	$⊢ A \subseteq ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{*}$
5	3 4	syl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ^{} <) \in ℝ^{}$
6		suprcl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) \in ℝ$
7	6	rexrd	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) \in ℝ^{*}$
8	6	leidd	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) \leq sup (A ℝ <)$
9		suprleub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land sup (A ℝ <) \in ℝ) \to (sup (A ℝ <) \leq sup (A ℝ <) \leftrightarrow \forall z \in A z \leq sup (A ℝ <))$
10	6 9	mpdan	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to (sup (A ℝ <) \leq sup (A ℝ <) \leftrightarrow \forall z \in A z \leq sup (A ℝ <))$
11		supxrleub	$⊢ (A \subseteq ℝ^{} \land sup (A ℝ <) \in ℝ^{}) \to (sup (A ℝ^{*} <) \leq sup (A ℝ <) \leftrightarrow \forall z \in A z \leq sup (A ℝ <))$
12	3 7 11	syl2anc	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to (sup (A ℝ^{*} <) \leq sup (A ℝ <) \leftrightarrow \forall z \in A z \leq sup (A ℝ <))$
13	10 12	bitr4d	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to (sup (A ℝ <) \leq sup (A ℝ <) \leftrightarrow sup (A ℝ^{*} <) \leq sup (A ℝ <))$
14	8 13	mpbid	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ^{*} <) \leq sup (A ℝ <)$
15	5	xrleidd	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ^{} <) \leq sup (A ℝ^{} <)$
16		supxrleub	$⊢ (A \subseteq ℝ^{} \land sup (A ℝ^{} <) \in ℝ^{}) \to (sup (A ℝ^{} <) \leq sup (A ℝ^{} <) \leftrightarrow \forall x \in A x \leq sup (A ℝ^{} <))$
17	3 5 16	syl2anc	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to (sup (A ℝ^{} <) \leq sup (A ℝ^{} <) \leftrightarrow \forall x \in A x \leq sup (A ℝ^{*} <))$
18		simp2	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to A \neq \emptyset$
19		n0	$⊢ A \neq \emptyset \leftrightarrow \exists z z \in A$
20	18 19	sylib	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to \exists z z \in A$
21		mnfxr	$⊢ −∞ \in ℝ^{*}$
22	21	a1i	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land z \in A) \to −∞ \in ℝ^{*}$
23	1	sselda	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land z \in A) \to z \in ℝ$
24	23	rexrd	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land z \in A) \to z \in ℝ^{*}$
25	5	adantr	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land z \in A) \to sup (A ℝ^{} <) \in ℝ^{}$
26	23	mnfltd	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land z \in A) \to −∞ < z$
27		supxrub	$⊢ (A \subseteq ℝ^{} \land z \in A) \to z \leq sup (A ℝ^{} <)$
28	3 27	sylan	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land z \in A) \to z \leq sup (A ℝ^{*} <)$
29	22 24 25 26 28	xrltletrd	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land z \in A) \to −∞ < sup (A ℝ^{*} <)$
30	20 29	exlimddv	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to −∞ < sup (A ℝ^{*} <)$
31		xrre	$⊢ ((sup (A ℝ^{} <) \in ℝ^{} \land sup (A ℝ <) \in ℝ) \land (−∞ < sup (A ℝ^{} <) \land sup (A ℝ^{} <) \leq sup (A ℝ <))) \to sup (A ℝ^{*} <) \in ℝ$
32	5 6 30 14 31	syl22anc	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ^{*} <) \in ℝ$
33		suprleub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land sup (A ℝ^{} <) \in ℝ) \to (sup (A ℝ <) \leq sup (A ℝ^{} <) \leftrightarrow \forall x \in A x \leq sup (A ℝ^{*} <))$
34	32 33	mpdan	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to (sup (A ℝ <) \leq sup (A ℝ^{} <) \leftrightarrow \forall x \in A x \leq sup (A ℝ^{} <))$
35	17 34	bitr4d	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to (sup (A ℝ^{} <) \leq sup (A ℝ^{} <) \leftrightarrow sup (A ℝ <) \leq sup (A ℝ^{*} <))$
36	15 35	mpbid	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) \leq sup (A ℝ^{*} <)$
37	5 7 14 36	xrletrid	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ^{*} <) = sup (A ℝ <)$

Metamath Proof Explorer

Theorem supxrre

Proof