Theorem sup3exmid 8852

Description: If any inhabited set of real numbers bounded from above has a supremum, excluded middle follows. (Contributed by Jim Kingdon, 2-Apr-2023.)

Hypothesis

Ref	Expression
sup3exmid.ex	⊢ ((𝑢 ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ 𝑢 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧)))

Assertion

Ref	Expression
sup3exmid	⊢ DECID 𝜑

Distinct variable groups:   𝑥,𝑧   𝜑,𝑢,𝑤   𝜑,𝑥,𝑦,𝑧,𝑢

Proof of Theorem sup3exmid

Dummy variables 𝑎 𝑏 𝑗 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0lt1 8025	. . . 4 ⊢ 0 < 1
2		0re 7899	. . . . 5 ⊢ 0 ∈ ℝ
3		1re 7898	. . . . 5 ⊢ 1 ∈ ℝ
4		lttri3 7978	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
5	4	adantl 275	. . . . . . 7 ⊢ ((⊤ ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
6		elrabi 2879	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ {0, 1})
7		elpri 3599	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {0, 1} → (𝑘 = 0 ∨ 𝑘 = 1))
8	6, 7	syl 14	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑘 = 0 ∨ 𝑘 = 1))
9		eleq1 2229	. . . . . . . . . . . . 13 ⊢ (𝑘 = 0 → (𝑘 ∈ ℝ ↔ 0 ∈ ℝ))
10	2, 9	mpbiri 167	. . . . . . . . . . . 12 ⊢ (𝑘 = 0 → 𝑘 ∈ ℝ)
11		eleq1 2229	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → (𝑘 ∈ ℝ ↔ 1 ∈ ℝ))
12	3, 11	mpbiri 167	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → 𝑘 ∈ ℝ)
13	10, 12	jaoi 706	. . . . . . . . . . 11 ⊢ ((𝑘 = 0 ∨ 𝑘 = 1) → 𝑘 ∈ ℝ)
14	8, 13	syl 14	. . . . . . . . . 10 ⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ ℝ)
15	14	ssriv 3146	. . . . . . . . 9 ⊢ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ
16		eqid 2165	. . . . . . . . . . . 12 ⊢ 0 = 0
17	16	orci 721	. . . . . . . . . . 11 ⊢ (0 = 0 ∨ 𝜑)
18	2	elexi 2738	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
19	18	prid1 3682	. . . . . . . . . . . 12 ⊢ 0 ∈ {0, 1}
20		eqeq1 2172	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 0 → (𝑗 = 0 ↔ 0 = 0))
21	20	orbi1d 781	. . . . . . . . . . . . 13 ⊢ (𝑗 = 0 → ((𝑗 = 0 ∨ 𝜑) ↔ (0 = 0 ∨ 𝜑)))
22	21	elrab3 2883	. . . . . . . . . . . 12 ⊢ (0 ∈ {0, 1} → (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (0 = 0 ∨ 𝜑)))
23	19, 22	ax-mp 5	. . . . . . . . . . 11 ⊢ (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (0 = 0 ∨ 𝜑))
24	17, 23	mpbir 145	. . . . . . . . . 10 ⊢ 0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}
25		elex2 2742	. . . . . . . . . 10 ⊢ (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)})
26	24, 25	ax-mp 5	. . . . . . . . 9 ⊢ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}
27		elrabi 2879	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑦 ∈ {0, 1})
28		elpri 3599	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {0, 1} → (𝑦 = 0 ∨ 𝑦 = 1))
29		0le1 8379	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 1
30		breq1 3985	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 0 → (𝑦 ≤ 1 ↔ 0 ≤ 1))
31	29, 30	mpbiri 167	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 0 → 𝑦 ≤ 1)
32	3	eqlei2 7993	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 1 → 𝑦 ≤ 1)
33	31, 32	jaoi 706	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 0 ∨ 𝑦 = 1) → 𝑦 ≤ 1)
34	28, 33	syl 14	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {0, 1} → 𝑦 ≤ 1)
35	27, 34	syl 14	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑦 ≤ 1)
36	35	rgen 2519	. . . . . . . . . 10 ⊢ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1
37		breq2 3986	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 1))
38	37	ralbidv 2466	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1))
39	38	rspcev 2830	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥)
40	3, 36, 39	mp2an 423	. . . . . . . . 9 ⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥
41		prexg 4189	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ∈ V)
42	2, 3, 41	mp2an 423	. . . . . . . . . . 11 ⊢ {0, 1} ∈ V
43	42	rabex 4126	. . . . . . . . . 10 ⊢ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∈ V
44		sseq1 3165	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑢 ⊆ ℝ ↔ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ))
45		eleq2 2230	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑤 ∈ 𝑢 ↔ 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}))
46	45	exbidv 1813	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑤 𝑤 ∈ 𝑢 ↔ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}))
47		raleq 2661	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥))
48	47	rexbidv 2467	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥))
49	44, 46, 48	3anbi123d 1302	. . . . . . . . . . 11 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((𝑢 ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ 𝑢 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥) ↔ ({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥)))
50		raleq 2661	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ 𝑢 ¬ 𝑥 < 𝑦 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦))
51		rexeq 2662	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑧 ∈ 𝑢 𝑦 < 𝑧 ↔ ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))
52	51	imbi2d 229	. . . . . . . . . . . . . 14 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧) ↔ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
53	52	ralbidv 2466	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
54	50, 53	anbi12d 465	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((∀𝑦 ∈ 𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧)) ↔ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))))
55	54	rexbidv 2467	. . . . . . . . . . 11 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧)) ↔ ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))))
56	49, 55	imbi12d 233	. . . . . . . . . 10 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (((𝑢 ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ 𝑢 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧))) ↔ (({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))))
57		sup3exmid.ex	. . . . . . . . . 10 ⊢ ((𝑢 ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ 𝑢 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧)))
58	43, 56, 57	vtocl 2780	. . . . . . . . 9 ⊢ (({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
59	15, 26, 40, 58	mp3an 1327	. . . . . . . 8 ⊢ ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))
60	59	a1i 9	. . . . . . 7 ⊢ (⊤ → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
61	5, 60	supclti 6963	. . . . . 6 ⊢ (⊤ → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ)
62	61	mptru 1352	. . . . 5 ⊢ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ
63		axltwlin 7966	. . . . 5 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ) → (0 < 1 → (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1)))
64	2, 3, 62, 63	mp3an 1327	. . . 4 ⊢ (0 < 1 → (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1))
65	1, 64	ax-mp 5	. . 3 ⊢ (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1)
66	5, 60	suplubti 6965	. . . . . . . 8 ⊢ (⊤ → ((0 ∈ ℝ ∧ 0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < )) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧))
67	66	mptru 1352	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ 0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < )) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧)
68	2, 67	mpan 421	. . . . . 6 ⊢ (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧)
69		df-rex 2450	. . . . . 6 ⊢ (∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧 ↔ ∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧))
70	68, 69	sylib 121	. . . . 5 ⊢ (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → ∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧))
71		eqeq1 2172	. . . . . . . . 9 ⊢ (𝑗 = 𝑧 → (𝑗 = 0 ↔ 𝑧 = 0))
72	71	orbi1d 781	. . . . . . . 8 ⊢ (𝑗 = 𝑧 → ((𝑗 = 0 ∨ 𝜑) ↔ (𝑧 = 0 ∨ 𝜑)))
73	72	elrab 2882	. . . . . . 7 ⊢ (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)))
74		simpr 109	. . . . . . . . . 10 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 0 < 𝑧)
75	74	gt0ne0d 8410	. . . . . . . . 9 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝑧 ≠ 0)
76	75	neneqd 2357	. . . . . . . 8 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → ¬ 𝑧 = 0)
77		simplr 520	. . . . . . . 8 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → (𝑧 = 0 ∨ 𝜑))
78		orel1 715	. . . . . . . 8 ⊢ (¬ 𝑧 = 0 → ((𝑧 = 0 ∨ 𝜑) → 𝜑))
79	76, 77, 78	sylc 62	. . . . . . 7 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝜑)
80	73, 79	sylanb 282	. . . . . 6 ⊢ ((𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑)
81	80	exlimiv 1586	. . . . 5 ⊢ (∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑)
82	70, 81	syl 14	. . . 4 ⊢ (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → 𝜑)
83	3	ltnri 7991	. . . . . 6 ⊢ ¬ 1 < 1
84		iba 298	. . . . . . . . . . . 12 ⊢ ((𝑧 = 0 ∨ 𝜑) → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))))
85	84	olcs 726	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))))
86	73, 85	bitr4id 198	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ 𝑧 ∈ {0, 1}))
87	86	eqrdv 2163	. . . . . . . . 9 ⊢ (𝜑 → {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} = {0, 1})
88	87	supeq1d 6952	. . . . . . . 8 ⊢ (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = sup({0, 1}, ℝ, < ))
89	3	a1i 9	. . . . . . . . . 10 ⊢ (⊤ → 1 ∈ ℝ)
90	3	elexi 2738	. . . . . . . . . . . 12 ⊢ 1 ∈ V
91	90	prid2 3683	. . . . . . . . . . 11 ⊢ 1 ∈ {0, 1}
92	91	a1i 9	. . . . . . . . . 10 ⊢ (⊤ → 1 ∈ {0, 1})
93		elpri 3599	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ {0, 1} → (𝑧 = 0 ∨ 𝑧 = 1))
94	2, 3	lenlti 7999	. . . . . . . . . . . . . . 15 ⊢ (0 ≤ 1 ↔ ¬ 1 < 0)
95	29, 94	mpbi 144	. . . . . . . . . . . . . 14 ⊢ ¬ 1 < 0
96		breq2 3986	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 0 → (1 < 𝑧 ↔ 1 < 0))
97	95, 96	mtbiri 665	. . . . . . . . . . . . 13 ⊢ (𝑧 = 0 → ¬ 1 < 𝑧)
98		breq2 3986	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 1 → (1 < 𝑧 ↔ 1 < 1))
99	83, 98	mtbiri 665	. . . . . . . . . . . . 13 ⊢ (𝑧 = 1 → ¬ 1 < 𝑧)
100	97, 99	jaoi 706	. . . . . . . . . . . 12 ⊢ ((𝑧 = 0 ∨ 𝑧 = 1) → ¬ 1 < 𝑧)
101	93, 100	syl 14	. . . . . . . . . . 11 ⊢ (𝑧 ∈ {0, 1} → ¬ 1 < 𝑧)
102	101	adantl 275	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑧 ∈ {0, 1}) → ¬ 1 < 𝑧)
103	5, 89, 92, 102	supmaxti 6969	. . . . . . . . 9 ⊢ (⊤ → sup({0, 1}, ℝ, < ) = 1)
104	103	mptru 1352	. . . . . . . 8 ⊢ sup({0, 1}, ℝ, < ) = 1
105	88, 104	eqtrdi 2215	. . . . . . 7 ⊢ (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = 1)
106	105	breq1d 3992	. . . . . 6 ⊢ (𝜑 → (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 ↔ 1 < 1))
107	83, 106	mtbiri 665	. . . . 5 ⊢ (𝜑 → ¬ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1)
108	107	con2i 617	. . . 4 ⊢ (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 → ¬ 𝜑)
109	82, 108	orim12i 749	. . 3 ⊢ ((0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1) → (𝜑 ∨ ¬ 𝜑))
110	65, 109	ax-mp 5	. 2 ⊢ (𝜑 ∨ ¬ 𝜑)
111		df-dc 825	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
112	110, 111	mpbir 145	1 ⊢ DECID 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 824   ∧ w3a 968   = wceq 1343  ⊤wtru 1344  ∃wex 1480   ∈ wcel 2136  ∀wral 2444  ∃wrex 2445  {crab 2448  Vcvv 2726   ⊆ wss 3116  {cpr 3577   class class class wbr 3982  supcsup 6947  ℝcr 7752  0cc0 7753  1c1 7754   < clt 7933   ≤ cle 7934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-13 2138  ax-14 2139  ax-ext 2147  ax-sep 4100  ax-pow 4153  ax-pr 4187  ax-un 4411  ax-setind 4514  ax-cnex 7844  ax-resscn 7845  ax-1re 7847  ax-addrcl 7850  ax-0lt1 7859  ax-rnegex 7862  ax-pre-ltirr 7865  ax-pre-ltwlin 7866  ax-pre-lttrn 7867  ax-pre-apti 7868

This theorem depends on definitions:  df-bi 116  df-dc 825  df-3an 970  df-tru 1346  df-fal 1349  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ne 2337  df-nel 2432  df-ral 2449  df-rex 2450  df-reu 2451  df-rmo 2452  df-rab 2453  df-v 2728  df-sbc 2952  df-dif 3118  df-un 3120  df-in 3122  df-ss 3129  df-pw 3561  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-br 3983  df-opab 4044  df-xp 4610  df-cnv 4612  df-iota 5153  df-riota 5798  df-sup 6949  df-pnf 7935  df-mnf 7936  df-xr 7937  df-ltxr 7938  df-le 7939

This theorem is referenced by: (None)