Theorem sup3exmid 8934

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 8104	. . . 4 ⊢ 0 < 1
2		0re 7977	. . . . 5 ⊢ 0 ∈ ℝ
3		1re 7976	. . . . 5 ⊢ 1 ∈ ℝ
4		lttri3 8057	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
5	4	adantl 277	. . . . . . 7 ⊢ ((⊤ ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
6		elrabi 2905	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ {0, 1})
7		elpri 3630	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {0, 1} → (𝑘 = 0 ∨ 𝑘 = 1))
8	6, 7	syl 14	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑘 = 0 ∨ 𝑘 = 1))
9		eleq1 2252	. . . . . . . . . . . . 13 ⊢ (𝑘 = 0 → (𝑘 ∈ ℝ ↔ 0 ∈ ℝ))
10	2, 9	mpbiri 168	. . . . . . . . . . . 12 ⊢ (𝑘 = 0 → 𝑘 ∈ ℝ)
11		eleq1 2252	. . . . . . . . . . . . 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 3174	. . . . . . . . 9 ⊢ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ
16		eqid 2189	. . . . . . . . . . . 12 ⊢ 0 = 0
17	16	orci 732	. . . . . . . . . . 11 ⊢ (0 = 0 ∨ 𝜑)
18	2	elexi 2764	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
19	18	prid1 3713	. . . . . . . . . . . 12 ⊢ 0 ∈ {0, 1}
20		eqeq1 2196	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 0 → (𝑗 = 0 ↔ 0 = 0))
21	20	orbi1d 792	. . . . . . . . . . . . 13 ⊢ (𝑗 = 0 → ((𝑗 = 0 ∨ 𝜑) ↔ (0 = 0 ∨ 𝜑)))
22	21	elrab3 2909	. . . . . . . . . . . 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 2768	. . . . . . . . . 10 ⊢ (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)})
26	24, 25	ax-mp 5	. . . . . . . . 9 ⊢ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}
27		elrabi 2905	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑦 ∈ {0, 1})
28		elpri 3630	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {0, 1} → (𝑦 = 0 ∨ 𝑦 = 1))
29		0le1 8458	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 1
30		breq1 4021	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 0 → (𝑦 ≤ 1 ↔ 0 ≤ 1))
31	29, 30	mpbiri 168	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 0 → 𝑦 ≤ 1)
32	3	eqlei2 8072	. . . . . . . . . . . . . 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 2543	. . . . . . . . . 10 ⊢ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1
37		breq2 4022	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 1))
38	37	ralbidv 2490	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1))
39	38	rspcev 2856	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥)
40	3, 36, 39	mp2an 426	. . . . . . . . 9 ⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥
41		prexg 4226	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ∈ V)
42	2, 3, 41	mp2an 426	. . . . . . . . . . 11 ⊢ {0, 1} ∈ V
43	42	rabex 4162	. . . . . . . . . 10 ⊢ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∈ V
44		sseq1 3193	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑢 ⊆ ℝ ↔ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ))
45		eleq2 2253	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑤 ∈ 𝑢 ↔ 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}))
46	45	exbidv 1836	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑤 𝑤 ∈ 𝑢 ↔ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}))
47		raleq 2686	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥))
48	47	rexbidv 2491	. . . . . . . . . . . 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 2686	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ 𝑢 ¬ 𝑥 < 𝑦 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦))
51		rexeq 2687	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑧 ∈ 𝑢 𝑦 < 𝑧 ↔ ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))
52	51	imbi2d 230	. . . . . . . . . . . . . 14 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧) ↔ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
53	52	ralbidv 2490	. . . . . . . . . . . . 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 2491	. . . . . . . . . . 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 2806	. . . . . . . . 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 7017	. . . . . 6 ⊢ (⊤ → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ)
62	61	mptru 1373	. . . . 5 ⊢ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ
63		axltwlin 8045	. . . . 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 7019	. . . . . . . 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 2474	. . . . . 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 2196	. . . . . . . . 9 ⊢ (𝑗 = 𝑧 → (𝑗 = 0 ↔ 𝑧 = 0))
72	71	orbi1d 792	. . . . . . . 8 ⊢ (𝑗 = 𝑧 → ((𝑗 = 0 ∨ 𝜑) ↔ (𝑧 = 0 ∨ 𝜑)))
73	72	elrab 2908	. . . . . . 7 ⊢ (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)))
74		simpr 110	. . . . . . . . . 10 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 0 < 𝑧)
75	74	gt0ne0d 8489	. . . . . . . . 9 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝑧 ≠ 0)
76	75	neneqd 2381	. . . . . . . 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 1609	. . . . 5 ⊢ (∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑)
82	70, 81	syl 14	. . . 4 ⊢ (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → 𝜑)
83	3	ltnri 8070	. . . . . 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 2187	. . . . . . . . 9 ⊢ (𝜑 → {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} = {0, 1})
88	87	supeq1d 7006	. . . . . . . 8 ⊢ (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = sup({0, 1}, ℝ, < ))
89	3	a1i 9	. . . . . . . . . 10 ⊢ (⊤ → 1 ∈ ℝ)
90	3	elexi 2764	. . . . . . . . . . . 12 ⊢ 1 ∈ V
91	90	prid2 3714	. . . . . . . . . . 11 ⊢ 1 ∈ {0, 1}
92	91	a1i 9	. . . . . . . . . 10 ⊢ (⊤ → 1 ∈ {0, 1})
93		elpri 3630	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ {0, 1} → (𝑧 = 0 ∨ 𝑧 = 1))
94	2, 3	lenlti 8078	. . . . . . . . . . . . . . 15 ⊢ (0 ≤ 1 ↔ ¬ 1 < 0)
95	29, 94	mpbi 145	. . . . . . . . . . . . . 14 ⊢ ¬ 1 < 0
96		breq2 4022	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 0 → (1 < 𝑧 ↔ 1 < 0))
97	95, 96	mtbiri 676	. . . . . . . . . . . . 13 ⊢ (𝑧 = 0 → ¬ 1 < 𝑧)
98		breq2 4022	. . . . . . . . . . . . . 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 7023	. . . . . . . . 9 ⊢ (⊤ → sup({0, 1}, ℝ, < ) = 1)
104	103	mptru 1373	. . . . . . . 8 ⊢ sup({0, 1}, ℝ, < ) = 1
105	88, 104	eqtrdi 2238	. . . . . . 7 ⊢ (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = 1)
106	105	breq1d 4028	. . . . . 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 1503   ∈ wcel 2160  ∀wral 2468  ∃wrex 2469  {crab 2472  Vcvv 2752   ⊆ wss 3144  {cpr 3608   class class class wbr 4018  supcsup 7001  ℝcr 7830  0cc0 7831  1c1 7832   < clt 8012   ≤ cle 8013

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-cnex 7922  ax-resscn 7923  ax-1re 7925  ax-addrcl 7928  ax-0lt1 7937  ax-rnegex 7940  ax-pre-ltirr 7943  ax-pre-ltwlin 7944  ax-pre-lttrn 7945  ax-pre-apti 7946

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2754  df-sbc 2978  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-opab 4080  df-xp 4647  df-cnv 4649  df-iota 5193  df-riota 5848  df-sup 7003  df-pnf 8014  df-mnf 8015  df-xr 8016  df-ltxr 8017  df-le 8018

This theorem is referenced by: (None)