ax-pre-sup

Description: A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, justified by Theorem axpre-sup . Note: Normally new proofs would use axsup . (New usage is discouraged.) (Contributed by NM, 13-Oct-2005)

		Ref	Expression
	Assertion	ax-pre-sup	$⊢ (A \subseteq ℝ \land 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))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$class A$
1		cr	$class ℝ$
2	0 1	wss	$wff A \subseteq ℝ$
3		c0	$class \emptyset$
4	0 3	wne	$wff A \neq \emptyset$
5		vx	$setvar x$
6		vy	$setvar y$
7	6	cv	$setvar y$
8		cltrr	$class <_{ℝ}$
9	5	cv	$setvar x$
10	7 9 8	wbr	$wff y <_{ℝ} x$
11	10 6 0	wral	$wff \forall y \in A y <_{ℝ} x$
12	11 5 1	wrex	$wff \exists x \in ℝ \forall y \in A y <_{ℝ} x$
13	2 4 12	w3a	$wff (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y <_{ℝ} x)$
14	9 7 8	wbr	$wff x <_{ℝ} y$
15	14	wn	$wff \neg x <_{ℝ} y$
16	15 6 0	wral	$wff \forall y \in A \neg x <_{ℝ} y$
17		vz	$setvar z$
18	17	cv	$setvar z$
19	7 18 8	wbr	$wff y <_{ℝ} z$
20	19 17 0	wrex	$wff \exists z \in A y <_{ℝ} z$
21	10 20	wi	$wff (y <_{ℝ} x \to \exists z \in A y <_{ℝ} z)$
22	21 6 1	wral	$wff \forall y \in ℝ (y <_{ℝ} x \to \exists z \in A y <_{ℝ} z)$
23	16 22	wa	$wff (\forall y \in A \neg x <_{ℝ} y \land \forall y \in ℝ (y <_{ℝ} x \to \exists z \in A y <_{ℝ} z))$
24	23 5 1	wrex	$wff \exists x \in ℝ (\forall y \in A \neg x <_{ℝ} y \land \forall y \in ℝ (y <_{ℝ} x \to \exists z \in A y <_{ℝ} z))$
25	13 24	wi	$wff ((A \subseteq ℝ \land 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

Axiom ax-pre-sup

Detailed syntax breakdown