axpre-sup

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. Note: The more general version with ordering on extended reals is axsup . This construction-dependent theorem should not be referenced directly; instead, use ax-pre-sup . (Contributed by NM, 19-May-1996) (Revised by Mario Carneiro, 16-Jun-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	axpre-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))$

Proof

Step	Hyp	Ref	Expression
1		elreal2	$⊢ x \in ℝ \leftrightarrow (1^{st} (x) \in 𝑹 \land x = ⟨1^{st} (x), 0_{𝑹}⟩)$
2	1	simplbi	$⊢ x \in ℝ \to 1^{st} (x) \in 𝑹$
3	2	adantl	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land x \in ℝ) \to 1^{st} (x) \in 𝑹$
4		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
5		fof	$⊢ 1^{st} : V \underset{onto}{⟶} V \to 1^{st} : V ⟶ V$
6		ffn	$⊢ 1^{st} : V ⟶ V \to 1^{st} Fn V$
7	4 5 6	mp2b	$⊢ 1^{st} Fn V$
8		ssv	$⊢ A \subseteq V$
9		fvelimab	$⊢ (1^{st} Fn V \land A \subseteq V) \to (w \in 1^{st} [A] \leftrightarrow \exists y \in A 1^{st} (y) = w)$
10	7 8 9	mp2an	$⊢ w \in 1^{st} [A] \leftrightarrow \exists y \in A 1^{st} (y) = w$
11		r19.29	$⊢ (\forall y \in A y <_{ℝ} x \land \exists y \in A 1^{st} (y) = w) \to \exists y \in A (y <_{ℝ} x \land 1^{st} (y) = w)$
12		ssel2	$⊢ (A \subseteq ℝ \land y \in A) \to y \in ℝ$
13		ltresr2	$⊢ (y \in ℝ \land x \in ℝ) \to (y <_{ℝ} x \leftrightarrow 1^{st} (y) <_{𝑹} 1^{st} (x))$
14		breq1	$⊢ 1^{st} (y) = w \to (1^{st} (y) <_{𝑹} 1^{st} (x) \leftrightarrow w <_{𝑹} 1^{st} (x))$
15	13 14	sylan9bb	$⊢ ((y \in ℝ \land x \in ℝ) \land 1^{st} (y) = w) \to (y <_{ℝ} x \leftrightarrow w <_{𝑹} 1^{st} (x))$
16	15	biimpd	$⊢ ((y \in ℝ \land x \in ℝ) \land 1^{st} (y) = w) \to (y <_{ℝ} x \to w <_{𝑹} 1^{st} (x))$
17	16	exp31	$⊢ y \in ℝ \to (x \in ℝ \to (1^{st} (y) = w \to (y <_{ℝ} x \to w <_{𝑹} 1^{st} (x))))$
18	12 17	syl	$⊢ (A \subseteq ℝ \land y \in A) \to (x \in ℝ \to (1^{st} (y) = w \to (y <_{ℝ} x \to w <_{𝑹} 1^{st} (x))))$
19	18	imp4b	$⊢ ((A \subseteq ℝ \land y \in A) \land x \in ℝ) \to ((1^{st} (y) = w \land y <_{ℝ} x) \to w <_{𝑹} 1^{st} (x))$
20	19	ancomsd	$⊢ ((A \subseteq ℝ \land y \in A) \land x \in ℝ) \to ((y <_{ℝ} x \land 1^{st} (y) = w) \to w <_{𝑹} 1^{st} (x))$
21	20	an32s	$⊢ ((A \subseteq ℝ \land x \in ℝ) \land y \in A) \to ((y <_{ℝ} x \land 1^{st} (y) = w) \to w <_{𝑹} 1^{st} (x))$
22	21	rexlimdva	$⊢ (A \subseteq ℝ \land x \in ℝ) \to (\exists y \in A (y <_{ℝ} x \land 1^{st} (y) = w) \to w <_{𝑹} 1^{st} (x))$
23	11 22	syl5	$⊢ (A \subseteq ℝ \land x \in ℝ) \to ((\forall y \in A y <_{ℝ} x \land \exists y \in A 1^{st} (y) = w) \to w <_{𝑹} 1^{st} (x))$
24	23	expd	$⊢ (A \subseteq ℝ \land x \in ℝ) \to (\forall y \in A y <_{ℝ} x \to (\exists y \in A 1^{st} (y) = w \to w <_{𝑹} 1^{st} (x)))$
25	10 24	syl7bi	$⊢ (A \subseteq ℝ \land x \in ℝ) \to (\forall y \in A y <_{ℝ} x \to (w \in 1^{st} [A] \to w <_{𝑹} 1^{st} (x)))$
26	25	impr	$⊢ (A \subseteq ℝ \land (x \in ℝ \land \forall y \in A y <_{ℝ} x)) \to (w \in 1^{st} [A] \to w <_{𝑹} 1^{st} (x))$
27	26	adantlr	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land (x \in ℝ \land \forall y \in A y <_{ℝ} x)) \to (w \in 1^{st} [A] \to w <_{𝑹} 1^{st} (x))$
28	27	ralrimiv	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land (x \in ℝ \land \forall y \in A y <_{ℝ} x)) \to \forall w \in 1^{st} [A] w <_{𝑹} 1^{st} (x)$
29	28	expr	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land x \in ℝ) \to (\forall y \in A y <_{ℝ} x \to \forall w \in 1^{st} [A] w <_{𝑹} 1^{st} (x))$
30		brralrspcev	$⊢ (1^{st} (x) \in 𝑹 \land \forall w \in 1^{st} [A] w <_{𝑹} 1^{st} (x)) \to \exists v \in 𝑹 \forall w \in 1^{st} [A] w <_{𝑹} v$
31	3 29 30	syl6an	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land x \in ℝ) \to (\forall y \in A y <_{ℝ} x \to \exists v \in 𝑹 \forall w \in 1^{st} [A] w <_{𝑹} v)$
32	31	rexlimdva	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (\exists x \in ℝ \forall y \in A y <_{ℝ} x \to \exists v \in 𝑹 \forall w \in 1^{st} [A] w <_{𝑹} v)$
33		n0	$⊢ A \neq \emptyset \leftrightarrow \exists y y \in A$
34		fnfvima	$⊢ (1^{st} Fn V \land A \subseteq V \land y \in A) \to 1^{st} (y) \in 1^{st} [A]$
35	7 8 34	mp3an12	$⊢ y \in A \to 1^{st} (y) \in 1^{st} [A]$
36	35	ne0d	$⊢ y \in A \to 1^{st} [A] \neq \emptyset$
37	36	exlimiv	$⊢ \exists y y \in A \to 1^{st} [A] \neq \emptyset$
38	33 37	sylbi	$⊢ A \neq \emptyset \to 1^{st} [A] \neq \emptyset$
39		supsr	$⊢ (1^{st} [A] \neq \emptyset \land \exists v \in 𝑹 \forall w \in 1^{st} [A] w <_{𝑹} v) \to \exists v \in 𝑹 (\forall w \in 1^{st} [A] \neg v <_{𝑹} w \land \forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u))$
40	39	ex	$⊢ 1^{st} [A] \neq \emptyset \to (\exists v \in 𝑹 \forall w \in 1^{st} [A] w <_{𝑹} v \to \exists v \in 𝑹 (\forall w \in 1^{st} [A] \neg v <_{𝑹} w \land \forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u)))$
41	38 40	syl	$⊢ A \neq \emptyset \to (\exists v \in 𝑹 \forall w \in 1^{st} [A] w <_{𝑹} v \to \exists v \in 𝑹 (\forall w \in 1^{st} [A] \neg v <_{𝑹} w \land \forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u)))$
42	41	adantl	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (\exists v \in 𝑹 \forall w \in 1^{st} [A] w <_{𝑹} v \to \exists v \in 𝑹 (\forall w \in 1^{st} [A] \neg v <_{𝑹} w \land \forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u)))$
43		breq2	$⊢ w = 1^{st} (y) \to (v <_{𝑹} w \leftrightarrow v <_{𝑹} 1^{st} (y))$
44	43	notbid	$⊢ w = 1^{st} (y) \to (\neg v <_{𝑹} w \leftrightarrow \neg v <_{𝑹} 1^{st} (y))$
45	44	rspccv	$⊢ \forall w \in 1^{st} [A] \neg v <_{𝑹} w \to (1^{st} (y) \in 1^{st} [A] \to \neg v <_{𝑹} 1^{st} (y))$
46	35 45	syl5com	$⊢ y \in A \to (\forall w \in 1^{st} [A] \neg v <_{𝑹} w \to \neg v <_{𝑹} 1^{st} (y))$
47	46	adantl	$⊢ (A \subseteq ℝ \land y \in A) \to (\forall w \in 1^{st} [A] \neg v <_{𝑹} w \to \neg v <_{𝑹} 1^{st} (y))$
48		elreal2	$⊢ y \in ℝ \leftrightarrow (1^{st} (y) \in 𝑹 \land y = ⟨1^{st} (y), 0_{𝑹}⟩)$
49	48	simprbi	$⊢ y \in ℝ \to y = ⟨1^{st} (y), 0_{𝑹}⟩$
50	49	breq2d	$⊢ y \in ℝ \to (⟨v, 0_{𝑹}⟩ <_{ℝ} y \leftrightarrow ⟨v, 0_{𝑹}⟩ <_{ℝ} ⟨1^{st} (y), 0_{𝑹}⟩)$
51		ltresr	$⊢ ⟨v, 0_{𝑹}⟩ <_{ℝ} ⟨1^{st} (y), 0_{𝑹}⟩ \leftrightarrow v <_{𝑹} 1^{st} (y)$
52	50 51	bitrdi	$⊢ y \in ℝ \to (⟨v, 0_{𝑹}⟩ <_{ℝ} y \leftrightarrow v <_{𝑹} 1^{st} (y))$
53	12 52	syl	$⊢ (A \subseteq ℝ \land y \in A) \to (⟨v, 0_{𝑹}⟩ <_{ℝ} y \leftrightarrow v <_{𝑹} 1^{st} (y))$
54	53	notbid	$⊢ (A \subseteq ℝ \land y \in A) \to (\neg ⟨v, 0_{𝑹}⟩ <_{ℝ} y \leftrightarrow \neg v <_{𝑹} 1^{st} (y))$
55	47 54	sylibrd	$⊢ (A \subseteq ℝ \land y \in A) \to (\forall w \in 1^{st} [A] \neg v <_{𝑹} w \to \neg ⟨v, 0_{𝑹}⟩ <_{ℝ} y)$
56	55	ralrimdva	$⊢ A \subseteq ℝ \to (\forall w \in 1^{st} [A] \neg v <_{𝑹} w \to \forall y \in A \neg ⟨v, 0_{𝑹}⟩ <_{ℝ} y)$
57	56	ad2antrr	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land v \in 𝑹) \to (\forall w \in 1^{st} [A] \neg v <_{𝑹} w \to \forall y \in A \neg ⟨v, 0_{𝑹}⟩ <_{ℝ} y)$
58	49	breq1d	$⊢ y \in ℝ \to (y <_{ℝ} ⟨v, 0_{𝑹}⟩ \leftrightarrow ⟨1^{st} (y), 0_{𝑹}⟩ <_{ℝ} ⟨v, 0_{𝑹}⟩)$
59		ltresr	$⊢ ⟨1^{st} (y), 0_{𝑹}⟩ <_{ℝ} ⟨v, 0_{𝑹}⟩ \leftrightarrow 1^{st} (y) <_{𝑹} v$
60	58 59	bitrdi	$⊢ y \in ℝ \to (y <_{ℝ} ⟨v, 0_{𝑹}⟩ \leftrightarrow 1^{st} (y) <_{𝑹} v)$
61	48	simplbi	$⊢ y \in ℝ \to 1^{st} (y) \in 𝑹$
62		breq1	$⊢ w = 1^{st} (y) \to (w <_{𝑹} v \leftrightarrow 1^{st} (y) <_{𝑹} v)$
63		breq1	$⊢ w = 1^{st} (y) \to (w <_{𝑹} u \leftrightarrow 1^{st} (y) <_{𝑹} u)$
64	63	rexbidv	$⊢ w = 1^{st} (y) \to (\exists u \in 1^{st} [A] w <_{𝑹} u \leftrightarrow \exists u \in 1^{st} [A] 1^{st} (y) <_{𝑹} u)$
65	62 64	imbi12d	$⊢ w = 1^{st} (y) \to ((w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u) \leftrightarrow (1^{st} (y) <_{𝑹} v \to \exists u \in 1^{st} [A] 1^{st} (y) <_{𝑹} u))$
66	65	rspccv	$⊢ \forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u) \to (1^{st} (y) \in 𝑹 \to (1^{st} (y) <_{𝑹} v \to \exists u \in 1^{st} [A] 1^{st} (y) <_{𝑹} u))$
67	61 66	syl5	$⊢ \forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u) \to (y \in ℝ \to (1^{st} (y) <_{𝑹} v \to \exists u \in 1^{st} [A] 1^{st} (y) <_{𝑹} u))$
68	67	com3l	$⊢ y \in ℝ \to (1^{st} (y) <_{𝑹} v \to (\forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u) \to \exists u \in 1^{st} [A] 1^{st} (y) <_{𝑹} u))$
69	60 68	sylbid	$⊢ y \in ℝ \to (y <_{ℝ} ⟨v, 0_{𝑹}⟩ \to (\forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u) \to \exists u \in 1^{st} [A] 1^{st} (y) <_{𝑹} u))$
70	69	adantr	$⊢ (y \in ℝ \land A \subseteq ℝ) \to (y <_{ℝ} ⟨v, 0_{𝑹}⟩ \to (\forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u) \to \exists u \in 1^{st} [A] 1^{st} (y) <_{𝑹} u))$
71		fvelimab	$⊢ (1^{st} Fn V \land A \subseteq V) \to (u \in 1^{st} [A] \leftrightarrow \exists z \in A 1^{st} (z) = u)$
72	7 8 71	mp2an	$⊢ u \in 1^{st} [A] \leftrightarrow \exists z \in A 1^{st} (z) = u$
73		ssel2	$⊢ (A \subseteq ℝ \land z \in A) \to z \in ℝ$
74		ltresr2	$⊢ (y \in ℝ \land z \in ℝ) \to (y <_{ℝ} z \leftrightarrow 1^{st} (y) <_{𝑹} 1^{st} (z))$
75	73 74	sylan2	$⊢ (y \in ℝ \land (A \subseteq ℝ \land z \in A)) \to (y <_{ℝ} z \leftrightarrow 1^{st} (y) <_{𝑹} 1^{st} (z))$
76		breq2	$⊢ 1^{st} (z) = u \to (1^{st} (y) <_{𝑹} 1^{st} (z) \leftrightarrow 1^{st} (y) <_{𝑹} u)$
77	75 76	sylan9bb	$⊢ ((y \in ℝ \land (A \subseteq ℝ \land z \in A)) \land 1^{st} (z) = u) \to (y <_{ℝ} z \leftrightarrow 1^{st} (y) <_{𝑹} u)$
78	77	exbiri	$⊢ (y \in ℝ \land (A \subseteq ℝ \land z \in A)) \to (1^{st} (z) = u \to (1^{st} (y) <_{𝑹} u \to y <_{ℝ} z))$
79	78	expr	$⊢ (y \in ℝ \land A \subseteq ℝ) \to (z \in A \to (1^{st} (z) = u \to (1^{st} (y) <_{𝑹} u \to y <_{ℝ} z)))$
80	79	com4r	$⊢ 1^{st} (y) <_{𝑹} u \to ((y \in ℝ \land A \subseteq ℝ) \to (z \in A \to (1^{st} (z) = u \to y <_{ℝ} z)))$
81	80	imp	$⊢ (1^{st} (y) <_{𝑹} u \land (y \in ℝ \land A \subseteq ℝ)) \to (z \in A \to (1^{st} (z) = u \to y <_{ℝ} z))$
82	81	reximdvai	$⊢ (1^{st} (y) <_{𝑹} u \land (y \in ℝ \land A \subseteq ℝ)) \to (\exists z \in A 1^{st} (z) = u \to \exists z \in A y <_{ℝ} z)$
83	72 82	syl5bi	$⊢ (1^{st} (y) <_{𝑹} u \land (y \in ℝ \land A \subseteq ℝ)) \to (u \in 1^{st} [A] \to \exists z \in A y <_{ℝ} z)$
84	83	expcom	$⊢ (y \in ℝ \land A \subseteq ℝ) \to (1^{st} (y) <_{𝑹} u \to (u \in 1^{st} [A] \to \exists z \in A y <_{ℝ} z))$
85	84	com23	$⊢ (y \in ℝ \land A \subseteq ℝ) \to (u \in 1^{st} [A] \to (1^{st} (y) <_{𝑹} u \to \exists z \in A y <_{ℝ} z))$
86	85	rexlimdv	$⊢ (y \in ℝ \land A \subseteq ℝ) \to (\exists u \in 1^{st} [A] 1^{st} (y) <_{𝑹} u \to \exists z \in A y <_{ℝ} z)$
87	70 86	syl6d	$⊢ (y \in ℝ \land A \subseteq ℝ) \to (y <_{ℝ} ⟨v, 0_{𝑹}⟩ \to (\forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u) \to \exists z \in A y <_{ℝ} z))$
88	87	com23	$⊢ (y \in ℝ \land A \subseteq ℝ) \to (\forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u) \to (y <_{ℝ} ⟨v, 0_{𝑹}⟩ \to \exists z \in A y <_{ℝ} z))$
89	88	ex	$⊢ y \in ℝ \to (A \subseteq ℝ \to (\forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u) \to (y <_{ℝ} ⟨v, 0_{𝑹}⟩ \to \exists z \in A y <_{ℝ} z)))$
90	89	com3l	$⊢ A \subseteq ℝ \to (\forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u) \to (y \in ℝ \to (y <_{ℝ} ⟨v, 0_{𝑹}⟩ \to \exists z \in A y <_{ℝ} z)))$
91	90	ad2antrr	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land v \in 𝑹) \to (\forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u) \to (y \in ℝ \to (y <_{ℝ} ⟨v, 0_{𝑹}⟩ \to \exists z \in A y <_{ℝ} z)))$
92	91	ralrimdv	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land v \in 𝑹) \to (\forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u) \to \forall y \in ℝ (y <_{ℝ} ⟨v, 0_{𝑹}⟩ \to \exists z \in A y <_{ℝ} z))$
93		opelreal	$⊢ ⟨v, 0_{𝑹}⟩ \in ℝ \leftrightarrow v \in 𝑹$
94	93	biimpri	$⊢ v \in 𝑹 \to ⟨v, 0_{𝑹}⟩ \in ℝ$
95	94	adantl	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land v \in 𝑹) \to ⟨v, 0_{𝑹}⟩ \in ℝ$
96		breq1	$⊢ x = ⟨v, 0_{𝑹}⟩ \to (x <_{ℝ} y \leftrightarrow ⟨v, 0_{𝑹}⟩ <_{ℝ} y)$
97	96	notbid	$⊢ x = ⟨v, 0_{𝑹}⟩ \to (\neg x <_{ℝ} y \leftrightarrow \neg ⟨v, 0_{𝑹}⟩ <_{ℝ} y)$
98	97	ralbidv	$⊢ x = ⟨v, 0_{𝑹}⟩ \to (\forall y \in A \neg x <_{ℝ} y \leftrightarrow \forall y \in A \neg ⟨v, 0_{𝑹}⟩ <_{ℝ} y)$
99		breq2	$⊢ x = ⟨v, 0_{𝑹}⟩ \to (y <_{ℝ} x \leftrightarrow y <_{ℝ} ⟨v, 0_{𝑹}⟩)$
100	99	imbi1d	$⊢ x = ⟨v, 0_{𝑹}⟩ \to ((y <_{ℝ} x \to \exists z \in A y <_{ℝ} z) \leftrightarrow (y <_{ℝ} ⟨v, 0_{𝑹}⟩ \to \exists z \in A y <_{ℝ} z))$
101	100	ralbidv	$⊢ x = ⟨v, 0_{𝑹}⟩ \to (\forall y \in ℝ (y <_{ℝ} x \to \exists z \in A y <_{ℝ} z) \leftrightarrow \forall y \in ℝ (y <_{ℝ} ⟨v, 0_{𝑹}⟩ \to \exists z \in A y <_{ℝ} z))$
102	98 101	anbi12d	$⊢ x = ⟨v, 0_{𝑹}⟩ \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 ⟨v, 0_{𝑹}⟩ <_{ℝ} y \land \forall y \in ℝ (y <_{ℝ} ⟨v, 0_{𝑹}⟩ \to \exists z \in A y <_{ℝ} z)))$
103	102	rspcev	$⊢ (⟨v, 0_{𝑹}⟩ \in ℝ \land (\forall y \in A \neg ⟨v, 0_{𝑹}⟩ <_{ℝ} y \land \forall y \in ℝ (y <_{ℝ} ⟨v, 0_{𝑹}⟩ \to \exists z \in A y <_{ℝ} z))) \to \exists x \in ℝ (\forall y \in A \neg x <_{ℝ} y \land \forall y \in ℝ (y <_{ℝ} x \to \exists z \in A y <_{ℝ} z))$
104	103	ex	$⊢ ⟨v, 0_{𝑹}⟩ \in ℝ \to ((\forall y \in A \neg ⟨v, 0_{𝑹}⟩ <_{ℝ} y \land \forall y \in ℝ (y <_{ℝ} ⟨v, 0_{𝑹}⟩ \to \exists z \in A y <_{ℝ} z)) \to \exists x \in ℝ (\forall y \in A \neg x <_{ℝ} y \land \forall y \in ℝ (y <_{ℝ} x \to \exists z \in A y <_{ℝ} z)))$
105	95 104	syl	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land v \in 𝑹) \to ((\forall y \in A \neg ⟨v, 0_{𝑹}⟩ <_{ℝ} y \land \forall y \in ℝ (y <_{ℝ} ⟨v, 0_{𝑹}⟩ \to \exists z \in A y <_{ℝ} z)) \to \exists x \in ℝ (\forall y \in A \neg x <_{ℝ} y \land \forall y \in ℝ (y <_{ℝ} x \to \exists z \in A y <_{ℝ} z)))$
106	57 92 105	syl2and	$⊢ ((A \subseteq ℝ \land A \neq \emptyset) \land v \in 𝑹) \to ((\forall w \in 1^{st} [A] \neg v <_{𝑹} w \land \forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u)) \to \exists x \in ℝ (\forall y \in A \neg x <_{ℝ} y \land \forall y \in ℝ (y <_{ℝ} x \to \exists z \in A y <_{ℝ} z)))$
107	106	rexlimdva	$⊢ (A \subseteq ℝ \land A \neq \emptyset) \to (\exists v \in 𝑹 (\forall w \in 1^{st} [A] \neg v <_{𝑹} w \land \forall w \in 𝑹 (w <_{𝑹} v \to \exists u \in 1^{st} [A] w <_{𝑹} u)) \to \exists x \in ℝ (\forall y \in A \neg x <_{ℝ} y \land \forall y \in ℝ (y <_{ℝ} x \to \exists z \in A y <_{ℝ} z)))$
108	32 42 107	3syld	$⊢ (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)))$
109	108	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 axpre-sup

Proof