supsr

Description: A nonempty, bounded set of signed reals has a supremum. (Contributed by NM, 21-May-1996) (Revised by Mario Carneiro, 15-Jun-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	supsr	$⊢ (A \neq \emptyset \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} 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))$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ A \neq \emptyset \leftrightarrow \exists u u \in A$
2		ltrelsr	$⊢ <_{𝑹} \subseteq 𝑹 \times 𝑹$
3	2	brel	$⊢ y <_{𝑹} x \to (y \in 𝑹 \land x \in 𝑹)$
4	3	simpld	$⊢ y <_{𝑹} x \to y \in 𝑹$
5	4	ralimi	$⊢ \forall y \in A y <_{𝑹} x \to \forall y \in A y \in 𝑹$
6		dfss3	$⊢ A \subseteq 𝑹 \leftrightarrow \forall y \in A y \in 𝑹$
7	5 6	sylibr	$⊢ \forall y \in A y <_{𝑹} x \to A \subseteq 𝑹$
8	7	sseld	$⊢ \forall y \in A y <_{𝑹} x \to (u \in A \to u \in 𝑹)$
9	8	rexlimivw	$⊢ \exists x \in 𝑹 \forall y \in A y <_{𝑹} x \to (u \in A \to u \in 𝑹)$
10	9	impcom	$⊢ (u \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \to u \in 𝑹$
11		eleq1	$⊢ u = if (u \in 𝑹, u, 1_{𝑹}) \to (u \in A \leftrightarrow if (u \in 𝑹, u, 1_{𝑹}) \in A)$
12	11	anbi1d	$⊢ u = if (u \in 𝑹, u, 1_{𝑹}) \to ((u \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x) \leftrightarrow (if (u \in 𝑹, u, 1_{𝑹}) \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} x))$
13	12	imbi1d	$⊢ u = if (u \in 𝑹, u, 1_{𝑹}) \to (((u \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} 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))) \leftrightarrow ((if (u \in 𝑹, u, 1_{𝑹}) \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} 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))))$
14		opeq1	$⊢ v = w \to ⟨v, 1_{𝑷}⟩ = ⟨w, 1_{𝑷}⟩$
15	14	eceq1d	$⊢ v = w \to [⟨v, 1_{𝑷}⟩] ~_{𝑹} = [⟨w, 1_{𝑷}⟩] ~_{𝑹}$
16	15	oveq2d	$⊢ v = w \to if (u \in 𝑹, u, 1_{𝑹}) +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} = if (u \in 𝑹, u, 1_{𝑹}) +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹}$
17	16	eleq1d	$⊢ v = w \to (if (u \in 𝑹, u, 1_{𝑹}) +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} \in A \leftrightarrow if (u \in 𝑹, u, 1_{𝑹}) +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} \in A)$
18	17	cbvabv	$⊢ \{v \| if (u \in 𝑹, u, 1_{𝑹}) +_{𝑹} [⟨v, 1_{𝑷}⟩] ~_{𝑹} \in A\} = \{w \| if (u \in 𝑹, u, 1_{𝑹}) +_{𝑹} [⟨w, 1_{𝑷}⟩] ~_{𝑹} \in A\}$
19		1sr	$⊢ 1_{𝑹} \in 𝑹$
20	19	elimel	$⊢ if (u \in 𝑹, u, 1_{𝑹}) \in 𝑹$
21	18 20	supsrlem	$⊢ (if (u \in 𝑹, u, 1_{𝑹}) \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} 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))$
22	13 21	dedth	$⊢ u \in 𝑹 \to ((u \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} 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)))$
23	10 22	mpcom	$⊢ (u \in A \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} 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))$
24	23	ex	$⊢ u \in A \to (\exists x \in 𝑹 \forall y \in A y <_{𝑹} 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)))$
25	24	exlimiv	$⊢ \exists u u \in A \to (\exists x \in 𝑹 \forall y \in A y <_{𝑹} 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)))$
26	1 25	sylbi	$⊢ A \neq \emptyset \to (\exists x \in 𝑹 \forall y \in A y <_{𝑹} 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)))$
27	26	imp	$⊢ (A \neq \emptyset \land \exists x \in 𝑹 \forall y \in A y <_{𝑹} 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))$

Metamath Proof Explorer

Theorem supsr

Proof