Theorem sup3exmid 8625

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 7812	. . . 4 ⊢ 0 < 1
2		0re 7690	. . . . 5 ⊢ 0 ∈ ℝ
3		1re 7689	. . . . 5 ⊢ 1 ∈ ℝ
4		lttri3 7767	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
5	4	adantl 273	. . . . . . 7 ⊢ ((⊤ ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
6		elrabi 2806	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ {0, 1})
7		elpri 3516	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {0, 1} → (𝑘 = 0 ∨ 𝑘 = 1))
8	6, 7	syl 14	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑘 = 0 ∨ 𝑘 = 1))
9		eleq1 2177	. . . . . . . . . . . . 13 ⊢ (𝑘 = 0 → (𝑘 ∈ ℝ ↔ 0 ∈ ℝ))
10	2, 9	mpbiri 167	. . . . . . . . . . . 12 ⊢ (𝑘 = 0 → 𝑘 ∈ ℝ)
11		eleq1 2177	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → (𝑘 ∈ ℝ ↔ 1 ∈ ℝ))
12	3, 11	mpbiri 167	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → 𝑘 ∈ ℝ)
13	10, 12	jaoi 688	. . . . . . . . . . 11 ⊢ ((𝑘 = 0 ∨ 𝑘 = 1) → 𝑘 ∈ ℝ)
14	8, 13	syl 14	. . . . . . . . . 10 ⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ ℝ)
15	14	ssriv 3067	. . . . . . . . 9 ⊢ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ
16		eqid 2115	. . . . . . . . . . . 12 ⊢ 0 = 0
17	16	orci 703	. . . . . . . . . . 11 ⊢ (0 = 0 ∨ 𝜑)
18	2	elexi 2669	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
19	18	prid1 3595	. . . . . . . . . . . 12 ⊢ 0 ∈ {0, 1}
20		eqeq1 2121	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 0 → (𝑗 = 0 ↔ 0 = 0))
21	20	orbi1d 763	. . . . . . . . . . . . 13 ⊢ (𝑗 = 0 → ((𝑗 = 0 ∨ 𝜑) ↔ (0 = 0 ∨ 𝜑)))
22	21	elrab3 2810	. . . . . . . . . . . 12 ⊢ (0 ∈ {0, 1} → (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (0 = 0 ∨ 𝜑)))
23	19, 22	ax-mp 7	. . . . . . . . . . 11 ⊢ (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (0 = 0 ∨ 𝜑))
24	17, 23	mpbir 145	. . . . . . . . . 10 ⊢ 0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}
25		elex2 2673	. . . . . . . . . 10 ⊢ (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)})
26	24, 25	ax-mp 7	. . . . . . . . 9 ⊢ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}
27		elrabi 2806	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑦 ∈ {0, 1})
28		elpri 3516	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {0, 1} → (𝑦 = 0 ∨ 𝑦 = 1))
29		0le1 8162	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 1
30		breq1 3898	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 0 → (𝑦 ≤ 1 ↔ 0 ≤ 1))
31	29, 30	mpbiri 167	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 0 → 𝑦 ≤ 1)
32	3	eqlei2 7781	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 1 → 𝑦 ≤ 1)
33	31, 32	jaoi 688	. . . . . . . . . . . . 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 2459	. . . . . . . . . 10 ⊢ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1
37		breq2 3899	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 1))
38	37	ralbidv 2411	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1))
39	38	rspcev 2760	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥)
40	3, 36, 39	mp2an 420	. . . . . . . . 9 ⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥
41		prexg 4093	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ∈ V)
42	2, 3, 41	mp2an 420	. . . . . . . . . . 11 ⊢ {0, 1} ∈ V
43	42	rabex 4032	. . . . . . . . . 10 ⊢ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∈ V
44		sseq1 3086	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑢 ⊆ ℝ ↔ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ))
45		eleq2 2178	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑤 ∈ 𝑢 ↔ 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}))
46	45	exbidv 1779	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑤 𝑤 ∈ 𝑢 ↔ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}))
47		raleq 2600	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥))
48	47	rexbidv 2412	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥))
49	44, 46, 48	3anbi123d 1273	. . . . . . . . . . 11 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((𝑢 ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ 𝑢 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥) ↔ ({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥)))
50		raleq 2600	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ 𝑢 ¬ 𝑥 < 𝑦 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦))
51		rexeq 2601	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑧 ∈ 𝑢 𝑦 < 𝑧 ↔ ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))
52	51	imbi2d 229	. . . . . . . . . . . . . 14 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧) ↔ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
53	52	ralbidv 2411	. . . . . . . . . . . . 13 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
54	50, 53	anbi12d 462	. . . . . . . . . . . 12 ⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((∀𝑦 ∈ 𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧)) ↔ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))))
55	54	rexbidv 2412	. . . . . . . . . . 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 2711	. . . . . . . . 9 ⊢ (({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
59	15, 26, 40, 58	mp3an 1298	. . . . . . . 8 ⊢ ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))
60	59	a1i 9	. . . . . . 7 ⊢ (⊤ → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
61	5, 60	supclti 6837	. . . . . 6 ⊢ (⊤ → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ)
62	61	mptru 1323	. . . . 5 ⊢ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ
63		axltwlin 7756	. . . . 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 1298	. . . 4 ⊢ (0 < 1 → (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1))
65	1, 64	ax-mp 7	. . 3 ⊢ (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1)
66	5, 60	suplubti 6839	. . . . . . . 8 ⊢ (⊤ → ((0 ∈ ℝ ∧ 0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < )) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧))
67	66	mptru 1323	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ 0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < )) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧)
68	2, 67	mpan 418	. . . . . 6 ⊢ (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧)
69		df-rex 2396	. . . . . 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 2121	. . . . . . . . 9 ⊢ (𝑗 = 𝑧 → (𝑗 = 0 ↔ 𝑧 = 0))
72	71	orbi1d 763	. . . . . . . 8 ⊢ (𝑗 = 𝑧 → ((𝑗 = 0 ∨ 𝜑) ↔ (𝑧 = 0 ∨ 𝜑)))
73	72	elrab 2809	. . . . . . 7 ⊢ (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)))
74		simpr 109	. . . . . . . . . 10 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 0 < 𝑧)
75	74	gt0ne0d 8193	. . . . . . . . 9 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝑧 ≠ 0)
76	75	neneqd 2303	. . . . . . . 8 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → ¬ 𝑧 = 0)
77		simplr 502	. . . . . . . 8 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → (𝑧 = 0 ∨ 𝜑))
78		orel1 697	. . . . . . . 8 ⊢ (¬ 𝑧 = 0 → ((𝑧 = 0 ∨ 𝜑) → 𝜑))
79	76, 77, 78	sylc 62	. . . . . . 7 ⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝜑)
80	73, 79	sylanb 280	. . . . . 6 ⊢ ((𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑)
81	80	exlimiv 1560	. . . . 5 ⊢ (∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑)
82	70, 81	syl 14	. . . 4 ⊢ (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → 𝜑)
83	3	ltnri 7779	. . . . . 6 ⊢ ¬ 1 < 1
84		iba 296	. . . . . . . . . . . 12 ⊢ ((𝑧 = 0 ∨ 𝜑) → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))))
85	84	olcs 708	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))))
86	85, 73	syl6rbbr 198	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ 𝑧 ∈ {0, 1}))
87	86	eqrdv 2113	. . . . . . . . 9 ⊢ (𝜑 → {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} = {0, 1})
88	87	supeq1d 6826	. . . . . . . 8 ⊢ (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = sup({0, 1}, ℝ, < ))
89	3	a1i 9	. . . . . . . . . 10 ⊢ (⊤ → 1 ∈ ℝ)
90	3	elexi 2669	. . . . . . . . . . . 12 ⊢ 1 ∈ V
91	90	prid2 3596	. . . . . . . . . . 11 ⊢ 1 ∈ {0, 1}
92	91	a1i 9	. . . . . . . . . 10 ⊢ (⊤ → 1 ∈ {0, 1})
93		elpri 3516	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ {0, 1} → (𝑧 = 0 ∨ 𝑧 = 1))
94	2, 3	lenlti 7787	. . . . . . . . . . . . . . 15 ⊢ (0 ≤ 1 ↔ ¬ 1 < 0)
95	29, 94	mpbi 144	. . . . . . . . . . . . . 14 ⊢ ¬ 1 < 0
96		breq2 3899	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 0 → (1 < 𝑧 ↔ 1 < 0))
97	95, 96	mtbiri 647	. . . . . . . . . . . . 13 ⊢ (𝑧 = 0 → ¬ 1 < 𝑧)
98		breq2 3899	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 1 → (1 < 𝑧 ↔ 1 < 1))
99	83, 98	mtbiri 647	. . . . . . . . . . . . 13 ⊢ (𝑧 = 1 → ¬ 1 < 𝑧)
100	97, 99	jaoi 688	. . . . . . . . . . . 12 ⊢ ((𝑧 = 0 ∨ 𝑧 = 1) → ¬ 1 < 𝑧)
101	93, 100	syl 14	. . . . . . . . . . 11 ⊢ (𝑧 ∈ {0, 1} → ¬ 1 < 𝑧)
102	101	adantl 273	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑧 ∈ {0, 1}) → ¬ 1 < 𝑧)
103	5, 89, 92, 102	supmaxti 6843	. . . . . . . . 9 ⊢ (⊤ → sup({0, 1}, ℝ, < ) = 1)
104	103	mptru 1323	. . . . . . . 8 ⊢ sup({0, 1}, ℝ, < ) = 1
105	88, 104	syl6eq 2163	. . . . . . 7 ⊢ (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = 1)
106	105	breq1d 3905	. . . . . 6 ⊢ (𝜑 → (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 ↔ 1 < 1))
107	83, 106	mtbiri 647	. . . . 5 ⊢ (𝜑 → ¬ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1)
108	107	con2i 599	. . . 4 ⊢ (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 → ¬ 𝜑)
109	82, 108	orim12i 731	. . 3 ⊢ ((0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1) → (𝜑 ∨ ¬ 𝜑))
110	65, 109	ax-mp 7	. 2 ⊢ (𝜑 ∨ ¬ 𝜑)
111		df-dc 803	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
112	110, 111	mpbir 145	1 ⊢ DECID 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 680  DECID wdc 802   ∧ w3a 945   = wceq 1314  ⊤wtru 1315  ∃wex 1451   ∈ wcel 1463  ∀wral 2390  ∃wrex 2391  {crab 2394  Vcvv 2657   ⊆ wss 3037  {cpr 3494   class class class wbr 3895  supcsup 6821  ℝcr 7546  0cc0 7547  1c1 7548   < clt 7724   ≤ cle 7725

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4006  ax-pow 4058  ax-pr 4091  ax-un 4315  ax-setind 4412  ax-cnex 7636  ax-resscn 7637  ax-1re 7639  ax-addrcl 7642  ax-0lt1 7651  ax-rnegex 7654  ax-pre-ltirr 7657  ax-pre-ltwlin 7658  ax-pre-lttrn 7659  ax-pre-apti 7660

This theorem depends on definitions:  df-bi 116  df-dc 803  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-ne 2283  df-nel 2378  df-ral 2395  df-rex 2396  df-reu 2397  df-rmo 2398  df-rab 2399  df-v 2659  df-sbc 2879  df-dif 3039  df-un 3041  df-in 3043  df-ss 3050  df-pw 3478  df-sn 3499  df-pr 3500  df-op 3502  df-uni 3703  df-br 3896  df-opab 3950  df-xp 4505  df-cnv 4507  df-iota 5046  df-riota 5684  df-sup 6823  df-pnf 7726  df-mnf 7727  df-xr 7728  df-ltxr 7729  df-le 7730

This theorem is referenced by: (None)