Metamath Proof Explorer

Theorem sup3

Description: A version of the completeness axiom for reals. (Contributed by NM, 12-Oct-2004)

		Ref	Expression
	Assertion	sup3	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq 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		ssel	$⊢ A \subseteq ℝ \to (y \in A \to y \in ℝ)$
2		leloe	$⊢ (y \in ℝ \land x \in ℝ) \to (y \leq x \leftrightarrow (y < x \lor y = x))$
3	2	expcom	$⊢ x \in ℝ \to (y \in ℝ \to (y \leq x \leftrightarrow (y < x \lor y = x)))$
4	1 3	syl9	$⊢ A \subseteq ℝ \to (x \in ℝ \to (y \in A \to (y \leq x \leftrightarrow (y < x \lor y = x))))$
5	4	imp31	$⊢ ((A \subseteq ℝ \land x \in ℝ) \land y \in A) \to (y \leq x \leftrightarrow (y < x \lor y = x))$
6	5	ralbidva	$⊢ (A \subseteq ℝ \land x \in ℝ) \to (\forall y \in A y \leq x \leftrightarrow \forall y \in A (y < x \lor y = x))$
7	6	rexbidva	$⊢ A \subseteq ℝ \to (\exists x \in ℝ \forall y \in A y \leq x \leftrightarrow \exists x \in ℝ \forall y \in A (y < x \lor y = x))$
8	7	anbi2d	$⊢ A \subseteq ℝ \to ((A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \leftrightarrow (A \neq \emptyset \land \exists x \in ℝ \forall y \in A (y < x \lor y = x)))$
9	8	pm5.32i	$⊢ (A \subseteq ℝ \land (A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x)) \leftrightarrow (A \subseteq ℝ \land (A \neq \emptyset \land \exists x \in ℝ \forall y \in A (y < x \lor y = x)))$
10		3anass	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \leftrightarrow (A \subseteq ℝ \land (A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x))$
11		3anass	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A (y < x \lor y = x)) \leftrightarrow (A \subseteq ℝ \land (A \neq \emptyset \land \exists x \in ℝ \forall y \in A (y < x \lor y = x)))$
12	9 10 11	3bitr4i	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \leftrightarrow (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A (y < x \lor y = x))$
13		sup2	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A (y < x \lor 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	12 13	sylbi	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq 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))$