Theorem sup3exmid 8984

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 8153	. . . 4 ⊢ 0 < 1
2		0re 8026	. . . . 5 ⊢ 0 ∈ ℝ
3		1re 8025	. . . . 5 ⊢ 1 ∈ ℝ
4		lttri3 8106	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
5	4	adantl 277	. . . . . . 7 ⊢ ((⊤ ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
6		elrabi 2917	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ {0, 1})
7		elpri 3645	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {0, 1} → (𝑘 = 0 ∨ 𝑘 = 1))
8	6, 7	syl 14	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑘 = 0 ∨ 𝑘 = 1))
9		eleq1 2259	. . . . . . . . . . . . 13 ⊢ (𝑘 = 0 → (𝑘 ∈ ℝ ↔ 0 ∈ ℝ))
10	2, 9	mpbiri 168	. . . . . . . . . . . 12 ⊢ (𝑘 = 0 → 𝑘 ∈ ℝ)
11		eleq1 2259	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → (𝑘 ∈ ℝ ↔ 1 ∈ ℝ))
12	3, 11	mpbiri 168	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → 𝑘 ∈ ℝ)
13	10, 12	jaoi 717	. . . . . . . . . . 11 ⊢ ((𝑘 = 0 ∨ 𝑘 = 1) → 𝑘 ∈ ℝ)
14	8, 13	syl 14	. . . . . . . . . 10 ⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ ℝ)
15	14	ssriv 3187	. . . . . . . . 9 ⊢ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ
16		eqid 2196	. . . . . . . . . . . 12 ⊢ 0 = 0
17	16	orci 732	. . . . . . . . . . 11 ⊢ (0 = 0 ∨ 𝜑)
18	2	elexi 2775	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
19	18	prid1 3728	. . . . . . . . . . . 12 ⊢ 0 ∈ {0, 1}
20		eqeq1 2203	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 0 → (𝑗 = 0 ↔ 0 = 0))
21	20	orbi1d 792	. . . . . . . . . . . . 13 ⊢ (𝑗 = 0 → ((𝑗 = 0 ∨ 𝜑) ↔ (0 = 0 ∨ 𝜑)))
22	21	elrab3 2921	. . . . . . . . . . . 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 146	. . . . . . . . . 10 ⊢ 0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}
25		elex2 2779	. . . . . . . . . 10 ⊢ (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)})
26	24, 25	ax-mp 5	. . . . . . . . 9 ⊢ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}
27		elrabi 2917	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑦 ∈ {0, 1})
28		elpri 3645	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {0, 1} → (𝑦 = 0 ∨ 𝑦 = 1))
29		0le1 8508	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 1
30		breq1 4036	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 0 → (𝑦 ≤ 1 ↔ 0 ≤ 1))
31	29, 30	mpbiri 168	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 0 → 𝑦 ≤ 1)
32	3	eqlei2 8121	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 1 → 𝑦 ≤ 1)
33	31, 32	jaoi 717	. . . . . . . . . . . . 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 2550	. . . . . . . . . 10 ⊢ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1
37		breq2 4037	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 1))
38	37	ralbidv 2497	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1))
39	38	rspcev 2868	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥)
40	3, 36, 39	mp2an 426	. . . . . . . . 9 ⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥
41		prexg 4244	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ∈ V)
42	2, 3, 41	mp2an 426	. . . . . . . . . . 11 ⊢ {0, 1} ∈ V
43	42	rabex 4177	. . . . . . . . . 10 ⊢ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∈ V
44		sseq1 3206	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑢 ⊆ ℝ ↔ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ))
45		eleq2 2260	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑤 ∈ 𝑢 ↔ 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}))
46	45	exbidv 1839	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑤 𝑤 ∈ 𝑢 ↔ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}))
47		raleq 2693	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥))
48	47	rexbidv 2498	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥))
49	44, 46, 48	3anbi123d 1323	. . . . . . . . . . 11 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((𝑢 ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ 𝑢 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥) ↔ ({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥)))
50		raleq 2693	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ 𝑢 ¬ 𝑥 < 𝑦 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦))
51		rexeq 2694	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑧 ∈ 𝑢 𝑦 < 𝑧 ↔ ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))
52	51	imbi2d 230	. . . . . . . . . . . . . 14 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧) ↔ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
53	52	ralbidv 2497	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
54	50, 53	anbi12d 473	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((∀𝑦 ∈ 𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧)) ↔ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))))
55	54	rexbidv 2498	. . . . . . . . . . 11 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧)) ↔ ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))))
56	49, 55	imbi12d 234	. . . . . . . . . 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 2818	. . . . . . . . 9 ⊢ (({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
59	15, 26, 40, 58	mp3an 1348	. . . . . . . 8 ⊢ ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))
60	59	a1i 9	. . . . . . 7 ⊢ (⊤ → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
61	5, 60	supclti 7064	. . . . . 6 ⊢ (⊤ → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ)
62	61	mptru 1373	. . . . 5 ⊢ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ
63		axltwlin 8094	. . . . 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 1348	. . . 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 7066	. . . . . . . 8 ⊢ (⊤ → ((0 ∈ ℝ ∧ 0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < )) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧))
67	66	mptru 1373	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ 0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < )) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧)
68	2, 67	mpan 424	. . . . . 6 ⊢ (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧)
69		df-rex 2481	. . . . . 6 ⊢ (∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧 ↔ ∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧))
70	68, 69	sylib 122	. . . . 5 ⊢ (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → ∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧))
71		eqeq1 2203	. . . . . . . . 9 ⊢ (𝑗 = 𝑧 → (𝑗 = 0 ↔ 𝑧 = 0))
72	71	orbi1d 792	. . . . . . . 8 ⊢ (𝑗 = 𝑧 → ((𝑗 = 0 ∨ 𝜑) ↔ (𝑧 = 0 ∨ 𝜑)))
73	72	elrab 2920	. . . . . . 7 ⊢ (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)))
74		simpr 110	. . . . . . . . . 10 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 0 < 𝑧)
75	74	gt0ne0d 8539	. . . . . . . . 9 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝑧 ≠ 0)
76	75	neneqd 2388	. . . . . . . 8 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → ¬ 𝑧 = 0)
77		simplr 528	. . . . . . . 8 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → (𝑧 = 0 ∨ 𝜑))
78		orel1 726	. . . . . . . 8 ⊢ (¬ 𝑧 = 0 → ((𝑧 = 0 ∨ 𝜑) → 𝜑))
79	76, 77, 78	sylc 62	. . . . . . 7 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝜑)
80	73, 79	sylanb 284	. . . . . 6 ⊢ ((𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑)
81	80	exlimiv 1612	. . . . 5 ⊢ (∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑)
82	70, 81	syl 14	. . . 4 ⊢ (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → 𝜑)
83	3	ltnri 8119	. . . . . 6 ⊢ ¬ 1 < 1
84		iba 300	. . . . . . . . . . . 12 ⊢ ((𝑧 = 0 ∨ 𝜑) → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))))
85	84	olcs 737	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))))
86	73, 85	bitr4id 199	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ 𝑧 ∈ {0, 1}))
87	86	eqrdv 2194	. . . . . . . . 9 ⊢ (𝜑 → {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} = {0, 1})
88	87	supeq1d 7053	. . . . . . . 8 ⊢ (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = sup({0, 1}, ℝ, < ))
89	3	a1i 9	. . . . . . . . . 10 ⊢ (⊤ → 1 ∈ ℝ)
90	3	elexi 2775	. . . . . . . . . . . 12 ⊢ 1 ∈ V
91	90	prid2 3729	. . . . . . . . . . 11 ⊢ 1 ∈ {0, 1}
92	91	a1i 9	. . . . . . . . . 10 ⊢ (⊤ → 1 ∈ {0, 1})
93		elpri 3645	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ {0, 1} → (𝑧 = 0 ∨ 𝑧 = 1))
94	2, 3	lenlti 8127	. . . . . . . . . . . . . . 15 ⊢ (0 ≤ 1 ↔ ¬ 1 < 0)
95	29, 94	mpbi 145	. . . . . . . . . . . . . 14 ⊢ ¬ 1 < 0
96		breq2 4037	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 0 → (1 < 𝑧 ↔ 1 < 0))
97	95, 96	mtbiri 676	. . . . . . . . . . . . 13 ⊢ (𝑧 = 0 → ¬ 1 < 𝑧)
98		breq2 4037	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 1 → (1 < 𝑧 ↔ 1 < 1))
99	83, 98	mtbiri 676	. . . . . . . . . . . . 13 ⊢ (𝑧 = 1 → ¬ 1 < 𝑧)
100	97, 99	jaoi 717	. . . . . . . . . . . 12 ⊢ ((𝑧 = 0 ∨ 𝑧 = 1) → ¬ 1 < 𝑧)
101	93, 100	syl 14	. . . . . . . . . . 11 ⊢ (𝑧 ∈ {0, 1} → ¬ 1 < 𝑧)
102	101	adantl 277	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑧 ∈ {0, 1}) → ¬ 1 < 𝑧)
103	5, 89, 92, 102	supmaxti 7070	. . . . . . . . 9 ⊢ (⊤ → sup({0, 1}, ℝ, < ) = 1)
104	103	mptru 1373	. . . . . . . 8 ⊢ sup({0, 1}, ℝ, < ) = 1
105	88, 104	eqtrdi 2245	. . . . . . 7 ⊢ (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = 1)
106	105	breq1d 4043	. . . . . 6 ⊢ (𝜑 → (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 ↔ 1 < 1))
107	83, 106	mtbiri 676	. . . . 5 ⊢ (𝜑 → ¬ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1)
108	107	con2i 628	. . . 4 ⊢ (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 → ¬ 𝜑)
109	82, 108	orim12i 760	. . 3 ⊢ ((0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1) → (𝜑 ∨ ¬ 𝜑))
110	65, 109	ax-mp 5	. 2 ⊢ (𝜑 ∨ ¬ 𝜑)
111		df-dc 836	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
112	110, 111	mpbir 146	1 ⊢ DECID 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 709  DECID wdc 835   ∧ w3a 980   = wceq 1364  ⊤wtru 1365  ∃wex 1506   ∈ wcel 2167  ∀wral 2475  ∃wrex 2476  {crab 2479  Vcvv 2763   ⊆ wss 3157  {cpr 3623   class class class wbr 4033  supcsup 7048  ℝcr 7878  0cc0 7879  1c1 7880   < clt 8061   ≤ cle 8062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-cnex 7970  ax-resscn 7971  ax-1re 7973  ax-addrcl 7976  ax-0lt1 7985  ax-rnegex 7988  ax-pre-ltirr 7991  ax-pre-ltwlin 7992  ax-pre-lttrn 7993  ax-pre-apti 7994

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rmo 2483  df-rab 2484  df-v 2765  df-sbc 2990  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-opab 4095  df-xp 4669  df-cnv 4671  df-iota 5219  df-riota 5877  df-sup 7050  df-pnf 8063  df-mnf 8064  df-xr 8065  df-ltxr 8066  df-le 8067

This theorem is referenced by: (None)