Axiom ax-pre-suploc 7870

Description: An inhabited, bounded-above, located set of reals has a supremum.

Locatedness here means that given 𝑥 < 𝑦, either there is an element of the set greater than 𝑥, or 𝑦 is an upper bound.

Although this and ax-caucvg 7869 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7869.

(Contributed by Jim Kingdon, 23-Jan-2024.)

Assertion

Ref	Expression
ax-pre-suploc	⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))

Distinct variable group:   𝑥,𝐴,𝑦,𝑧

Detailed syntax breakdown of Axiom ax-pre-suploc

Step	Hyp	Ref	Expression
1		cA	. . . . 5 class 𝐴
2		cr 7748	. . . . 5 class ℝ
3	1, 2	wss 3115	. . . 4 wff 𝐴 ⊆ ℝ
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1342	. . . . . 6 class 𝑥
6	5, 1	wcel 2136	. . . . 5 wff 𝑥 ∈ 𝐴
7	6, 4	wex 1480	. . . 4 wff ∃𝑥 𝑥 ∈ 𝐴
8	3, 7	wa 103	. . 3 wff (𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴)
9		vy	. . . . . . . 8 setvar 𝑦
10	9	cv 1342	. . . . . . 7 class 𝑦
11		cltrr 7753	. . . . . . 7 class <ℝ
12	10, 5, 11	wbr 3981	. . . . . 6 wff 𝑦 <ℝ 𝑥
13	12, 9, 1	wral 2443	. . . . 5 wff ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥
14	13, 4, 2	wrex 2444	. . . 4 wff ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥
15	5, 10, 11	wbr 3981	. . . . . . 7 wff 𝑥 <ℝ 𝑦
16		vz	. . . . . . . . . . 11 setvar 𝑧
17	16	cv 1342	. . . . . . . . . 10 class 𝑧
18	5, 17, 11	wbr 3981	. . . . . . . . 9 wff 𝑥 <ℝ 𝑧
19	18, 16, 1	wrex 2444	. . . . . . . 8 wff ∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧
20	17, 10, 11	wbr 3981	. . . . . . . . 9 wff 𝑧 <ℝ 𝑦
21	20, 16, 1	wral 2443	. . . . . . . 8 wff ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦
22	19, 21	wo 698	. . . . . . 7 wff (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)
23	15, 22	wi 4	. . . . . 6 wff (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦))
24	23, 9, 2	wral 2443	. . . . 5 wff ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦))
25	24, 4, 2	wral 2443	. . . 4 wff ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦))
26	14, 25	wa 103	. . 3 wff (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)))
27	8, 26	wa 103	. 2 wff ((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦))))
28	15	wn 3	. . . . 5 wff ¬ 𝑥 <ℝ 𝑦
29	28, 9, 1	wral 2443	. . . 4 wff ∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦
30	10, 17, 11	wbr 3981	. . . . . . 7 wff 𝑦 <ℝ 𝑧
31	30, 16, 1	wrex 2444	. . . . . 6 wff ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧
32	12, 31	wi 4	. . . . 5 wff (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)
33	32, 9, 2	wral 2443	. . . 4 wff ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)
34	29, 33	wa 103	. . 3 wff (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))
35	34, 4, 2	wrex 2444	. 2 wff ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))
36	27, 35	wi 4	1 wff (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))

This axiom is referenced by:  axsuploc  7967