Theorem sup3exmid 8903

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 8074	. . . 4 ⊢ 0 < 1
2		0re 7948	. . . . 5 ⊢ 0 ∈ ℝ
3		1re 7947	. . . . 5 ⊢ 1 ∈ ℝ
4		lttri3 8027	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
5	4	adantl 277	. . . . . . 7 ⊢ ((⊤ ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
6		elrabi 2890	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ {0, 1})
7		elpri 3614	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {0, 1} → (𝑘 = 0 ∨ 𝑘 = 1))
8	6, 7	syl 14	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑘 = 0 ∨ 𝑘 = 1))
9		eleq1 2240	. . . . . . . . . . . . 13 ⊢ (𝑘 = 0 → (𝑘 ∈ ℝ ↔ 0 ∈ ℝ))
10	2, 9	mpbiri 168	. . . . . . . . . . . 12 ⊢ (𝑘 = 0 → 𝑘 ∈ ℝ)
11		eleq1 2240	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → (𝑘 ∈ ℝ ↔ 1 ∈ ℝ))
12	3, 11	mpbiri 168	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → 𝑘 ∈ ℝ)
13	10, 12	jaoi 716	. . . . . . . . . . 11 ⊢ ((𝑘 = 0 ∨ 𝑘 = 1) → 𝑘 ∈ ℝ)
14	8, 13	syl 14	. . . . . . . . . 10 ⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ ℝ)
15	14	ssriv 3159	. . . . . . . . 9 ⊢ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ
16		eqid 2177	. . . . . . . . . . . 12 ⊢ 0 = 0
17	16	orci 731	. . . . . . . . . . 11 ⊢ (0 = 0 ∨ 𝜑)
18	2	elexi 2749	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
19	18	prid1 3697	. . . . . . . . . . . 12 ⊢ 0 ∈ {0, 1}
20		eqeq1 2184	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 0 → (𝑗 = 0 ↔ 0 = 0))
21	20	orbi1d 791	. . . . . . . . . . . . 13 ⊢ (𝑗 = 0 → ((𝑗 = 0 ∨ 𝜑) ↔ (0 = 0 ∨ 𝜑)))
22	21	elrab3 2894	. . . . . . . . . . . 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 2753	. . . . . . . . . 10 ⊢ (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)})
26	24, 25	ax-mp 5	. . . . . . . . 9 ⊢ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}
27		elrabi 2890	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑦 ∈ {0, 1})
28		elpri 3614	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {0, 1} → (𝑦 = 0 ∨ 𝑦 = 1))
29		0le1 8428	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 1
30		breq1 4003	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 0 → (𝑦 ≤ 1 ↔ 0 ≤ 1))
31	29, 30	mpbiri 168	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 0 → 𝑦 ≤ 1)
32	3	eqlei2 8042	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 1 → 𝑦 ≤ 1)
33	31, 32	jaoi 716	. . . . . . . . . . . . 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 2530	. . . . . . . . . 10 ⊢ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1
37		breq2 4004	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 1))
38	37	ralbidv 2477	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1))
39	38	rspcev 2841	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥)
40	3, 36, 39	mp2an 426	. . . . . . . . 9 ⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥
41		prexg 4208	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ∈ V)
42	2, 3, 41	mp2an 426	. . . . . . . . . . 11 ⊢ {0, 1} ∈ V
43	42	rabex 4144	. . . . . . . . . 10 ⊢ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∈ V
44		sseq1 3178	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑢 ⊆ ℝ ↔ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ))
45		eleq2 2241	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑤 ∈ 𝑢 ↔ 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}))
46	45	exbidv 1825	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑤 𝑤 ∈ 𝑢 ↔ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}))
47		raleq 2672	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥))
48	47	rexbidv 2478	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥))
49	44, 46, 48	3anbi123d 1312	. . . . . . . . . . 11 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((𝑢 ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ 𝑢 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥) ↔ ({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥)))
50		raleq 2672	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ 𝑢 ¬ 𝑥 < 𝑦 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦))
51		rexeq 2673	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑧 ∈ 𝑢 𝑦 < 𝑧 ↔ ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))
52	51	imbi2d 230	. . . . . . . . . . . . . 14 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧) ↔ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
53	52	ralbidv 2477	. . . . . . . . . . . . 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 2478	. . . . . . . . . . 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 2791	. . . . . . . . 9 ⊢ (({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
59	15, 26, 40, 58	mp3an 1337	. . . . . . . 8 ⊢ ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))
60	59	a1i 9	. . . . . . 7 ⊢ (⊤ → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
61	5, 60	supclti 6991	. . . . . 6 ⊢ (⊤ → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ)
62	61	mptru 1362	. . . . 5 ⊢ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ
63		axltwlin 8015	. . . . 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 1337	. . . 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 6993	. . . . . . . 8 ⊢ (⊤ → ((0 ∈ ℝ ∧ 0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < )) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧))
67	66	mptru 1362	. . . . . . 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 2461	. . . . . 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 2184	. . . . . . . . 9 ⊢ (𝑗 = 𝑧 → (𝑗 = 0 ↔ 𝑧 = 0))
72	71	orbi1d 791	. . . . . . . 8 ⊢ (𝑗 = 𝑧 → ((𝑗 = 0 ∨ 𝜑) ↔ (𝑧 = 0 ∨ 𝜑)))
73	72	elrab 2893	. . . . . . 7 ⊢ (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)))
74		simpr 110	. . . . . . . . . 10 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 0 < 𝑧)
75	74	gt0ne0d 8459	. . . . . . . . 9 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝑧 ≠ 0)
76	75	neneqd 2368	. . . . . . . 8 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → ¬ 𝑧 = 0)
77		simplr 528	. . . . . . . 8 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → (𝑧 = 0 ∨ 𝜑))
78		orel1 725	. . . . . . . 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 1598	. . . . 5 ⊢ (∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑)
82	70, 81	syl 14	. . . 4 ⊢ (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → 𝜑)
83	3	ltnri 8040	. . . . . 6 ⊢ ¬ 1 < 1
84		iba 300	. . . . . . . . . . . 12 ⊢ ((𝑧 = 0 ∨ 𝜑) → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))))
85	84	olcs 736	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))))
86	73, 85	bitr4id 199	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ 𝑧 ∈ {0, 1}))
87	86	eqrdv 2175	. . . . . . . . 9 ⊢ (𝜑 → {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} = {0, 1})
88	87	supeq1d 6980	. . . . . . . 8 ⊢ (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = sup({0, 1}, ℝ, < ))
89	3	a1i 9	. . . . . . . . . 10 ⊢ (⊤ → 1 ∈ ℝ)
90	3	elexi 2749	. . . . . . . . . . . 12 ⊢ 1 ∈ V
91	90	prid2 3698	. . . . . . . . . . 11 ⊢ 1 ∈ {0, 1}
92	91	a1i 9	. . . . . . . . . 10 ⊢ (⊤ → 1 ∈ {0, 1})
93		elpri 3614	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ {0, 1} → (𝑧 = 0 ∨ 𝑧 = 1))
94	2, 3	lenlti 8048	. . . . . . . . . . . . . . 15 ⊢ (0 ≤ 1 ↔ ¬ 1 < 0)
95	29, 94	mpbi 145	. . . . . . . . . . . . . 14 ⊢ ¬ 1 < 0
96		breq2 4004	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 0 → (1 < 𝑧 ↔ 1 < 0))
97	95, 96	mtbiri 675	. . . . . . . . . . . . 13 ⊢ (𝑧 = 0 → ¬ 1 < 𝑧)
98		breq2 4004	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 1 → (1 < 𝑧 ↔ 1 < 1))
99	83, 98	mtbiri 675	. . . . . . . . . . . . 13 ⊢ (𝑧 = 1 → ¬ 1 < 𝑧)
100	97, 99	jaoi 716	. . . . . . . . . . . 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 6997	. . . . . . . . 9 ⊢ (⊤ → sup({0, 1}, ℝ, < ) = 1)
104	103	mptru 1362	. . . . . . . 8 ⊢ sup({0, 1}, ℝ, < ) = 1
105	88, 104	eqtrdi 2226	. . . . . . 7 ⊢ (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = 1)
106	105	breq1d 4010	. . . . . 6 ⊢ (𝜑 → (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 ↔ 1 < 1))
107	83, 106	mtbiri 675	. . . . 5 ⊢ (𝜑 → ¬ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1)
108	107	con2i 627	. . . 4 ⊢ (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 → ¬ 𝜑)
109	82, 108	orim12i 759	. . 3 ⊢ ((0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1) → (𝜑 ∨ ¬ 𝜑))
110	65, 109	ax-mp 5	. 2 ⊢ (𝜑 ∨ ¬ 𝜑)
111		df-dc 835	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
112	110, 111	mpbir 146	1 ⊢ DECID 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 708  DECID wdc 834   ∧ w3a 978   = wceq 1353  ⊤wtru 1354  ∃wex 1492   ∈ wcel 2148  ∀wral 2455  ∃wrex 2456  {crab 2459  Vcvv 2737   ⊆ wss 3129  {cpr 3592   class class class wbr 4000  supcsup 6975  ℝcr 7801  0cc0 7802  1c1 7803   < clt 7982   ≤ cle 7983

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-cnex 7893  ax-resscn 7894  ax-1re 7896  ax-addrcl 7899  ax-0lt1 7908  ax-rnegex 7911  ax-pre-ltirr 7914  ax-pre-ltwlin 7915  ax-pre-lttrn 7916  ax-pre-apti 7917

This theorem depends on definitions:  df-bi 117  df-dc 835  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-xp 4629  df-cnv 4631  df-iota 5174  df-riota 5825  df-sup 6977  df-pnf 7984  df-mnf 7985  df-xr 7986  df-ltxr 7987  df-le 7988

This theorem is referenced by: (None)