axsup

Description: A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-sup with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005)

		Ref	Expression
	Assertion	axsup	$⊢ (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))$

Proof

Step	Hyp	Ref	Expression
1		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))$
2	1	3expia	$⊢ (A \subseteq ℝ \land 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)))$
3		ssel2	$⊢ (A \subseteq ℝ \land y \in A) \to y \in ℝ$
4		ltxrlt	$⊢ (y \in ℝ \land x \in ℝ) \to (y < x \leftrightarrow y <_{ℝ} x)$
5	3 4	sylan	$⊢ ((A \subseteq ℝ \land y \in A) \land x \in ℝ) \to (y < x \leftrightarrow y <_{ℝ} x)$
6	5	an32s	$⊢ ((A \subseteq ℝ \land x \in ℝ) \land y \in A) \to (y < x \leftrightarrow y <_{ℝ} x)$
7	6	ralbidva	$⊢ (A \subseteq ℝ \land x \in ℝ) \to (\forall y \in A y < x \leftrightarrow \forall y \in A y <_{ℝ} x)$
8	7	rexbidva	$⊢ A \subseteq ℝ \to (\exists x \in ℝ \forall y \in A y < x \leftrightarrow \exists x \in ℝ \forall y \in A y <_{ℝ} x)$
9	8	adantr	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (\exists x \in ℝ \forall y \in A y < x \leftrightarrow \exists x \in ℝ \forall y \in A y <_{ℝ} x)$
10		ltxrlt	$⊢ (x \in ℝ \land y \in ℝ) \to (x < y \leftrightarrow x <_{ℝ} y)$
11	10	ancoms	$⊢ (y \in ℝ \land x \in ℝ) \to (x < y \leftrightarrow x <_{ℝ} y)$
12	3 11	sylan	$⊢ ((A \subseteq ℝ \land y \in A) \land x \in ℝ) \to (x < y \leftrightarrow x <_{ℝ} y)$
13	12	an32s	$⊢ ((A \subseteq ℝ \land x \in ℝ) \land y \in A) \to (x < y \leftrightarrow x <_{ℝ} y)$
14	13	notbid	$⊢ ((A \subseteq ℝ \land x \in ℝ) \land y \in A) \to (\neg x < y \leftrightarrow \neg x <_{ℝ} y)$
15	14	ralbidva	$⊢ (A \subseteq ℝ \land x \in ℝ) \to (\forall y \in A \neg x < y \leftrightarrow \forall y \in A \neg x <_{ℝ} y)$
16	4	ancoms	$⊢ (x \in ℝ \land y \in ℝ) \to (y < x \leftrightarrow y <_{ℝ} x)$
17	16	adantll	$⊢ ((A \subseteq ℝ \land x \in ℝ) \land y \in ℝ) \to (y < x \leftrightarrow y <_{ℝ} x)$
18		ssel2	$⊢ (A \subseteq ℝ \land z \in A) \to z \in ℝ$
19		ltxrlt	$⊢ (y \in ℝ \land z \in ℝ) \to (y < z \leftrightarrow y <_{ℝ} z)$
20	19	ancoms	$⊢ (z \in ℝ \land y \in ℝ) \to (y < z \leftrightarrow y <_{ℝ} z)$
21	18 20	sylan	$⊢ ((A \subseteq ℝ \land z \in A) \land y \in ℝ) \to (y < z \leftrightarrow y <_{ℝ} z)$
22	21	an32s	$⊢ ((A \subseteq ℝ \land y \in ℝ) \land z \in A) \to (y < z \leftrightarrow y <_{ℝ} z)$
23	22	rexbidva	$⊢ (A \subseteq ℝ \land y \in ℝ) \to (\exists z \in A y < z \leftrightarrow \exists z \in A y <_{ℝ} z)$
24	23	adantlr	$⊢ ((A \subseteq ℝ \land x \in ℝ) \land y \in ℝ) \to (\exists z \in A y < z \leftrightarrow \exists z \in A y <_{ℝ} z)$
25	17 24	imbi12d	$⊢ ((A \subseteq ℝ \land x \in ℝ) \land y \in ℝ) \to ((y < x \to \exists z \in A y < z) \leftrightarrow (y <_{ℝ} x \to \exists z \in A y <_{ℝ} z))$
26	25	ralbidva	$⊢ (A \subseteq ℝ \land x \in ℝ) \to (\forall y \in ℝ (y < x \to \exists z \in A y < z) \leftrightarrow \forall y \in ℝ (y <_{ℝ} x \to \exists z \in A y <_{ℝ} z))$
27	15 26	anbi12d	$⊢ (A \subseteq ℝ \land x \in ℝ) \to ((\forall y \in A \neg x < y \land \forall y \in ℝ (y < x \to \exists z \in A y < z)) \leftrightarrow (\forall y \in A \neg x <_{ℝ} y \land \forall y \in ℝ (y <_{ℝ} x \to \exists z \in A y <_{ℝ} z)))$
28	27	rexbidva	$⊢ A \subseteq ℝ \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 \exists x \in ℝ (\forall y \in A \neg x <_{ℝ} y \land \forall y \in ℝ (y <_{ℝ} x \to \exists z \in A y <_{ℝ} z)))$
29	28	adantr	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \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 \exists x \in ℝ (\forall y \in A \neg x <_{ℝ} y \land \forall y \in ℝ (y <_{ℝ} x \to \exists z \in A y <_{ℝ} z)))$
30	2 9 29	3imtr4d	$⊢ (A \subseteq ℝ \land 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)))$
31	30	3impia	$⊢ (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

Theorem axsup

Proof