ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sup3exmid GIF version

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.
StepHypRef Expression
1 0lt1 7812 . . . 4 0 < 1
2 0re 7690 . . . . 5 0 ∈ ℝ
3 1re 7689 . . . . 5 1 ∈ ℝ
4 lttri3 7767 . . . . . . . 8 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
54adantl 273 . . . . . . 7 ((⊤ ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
6 elrabi 2806 . . . . . . . . . . . 12 (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ {0, 1})
7 elpri 3516 . . . . . . . . . . . 12 (𝑘 ∈ {0, 1} → (𝑘 = 0 ∨ 𝑘 = 1))
86, 7syl 14 . . . . . . . . . . 11 (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑘 = 0 ∨ 𝑘 = 1))
9 eleq1 2177 . . . . . . . . . . . . 13 (𝑘 = 0 → (𝑘 ∈ ℝ ↔ 0 ∈ ℝ))
102, 9mpbiri 167 . . . . . . . . . . . 12 (𝑘 = 0 → 𝑘 ∈ ℝ)
11 eleq1 2177 . . . . . . . . . . . . 13 (𝑘 = 1 → (𝑘 ∈ ℝ ↔ 1 ∈ ℝ))
123, 11mpbiri 167 . . . . . . . . . . . 12 (𝑘 = 1 → 𝑘 ∈ ℝ)
1310, 12jaoi 688 . . . . . . . . . . 11 ((𝑘 = 0 ∨ 𝑘 = 1) → 𝑘 ∈ ℝ)
148, 13syl 14 . . . . . . . . . 10 (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ ℝ)
1514ssriv 3067 . . . . . . . . 9 {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ
16 eqid 2115 . . . . . . . . . . . 12 0 = 0
1716orci 703 . . . . . . . . . . 11 (0 = 0 ∨ 𝜑)
182elexi 2669 . . . . . . . . . . . . 13 0 ∈ V
1918prid1 3595 . . . . . . . . . . . 12 0 ∈ {0, 1}
20 eqeq1 2121 . . . . . . . . . . . . . 14 (𝑗 = 0 → (𝑗 = 0 ↔ 0 = 0))
2120orbi1d 763 . . . . . . . . . . . . 13 (𝑗 = 0 → ((𝑗 = 0 ∨ 𝜑) ↔ (0 = 0 ∨ 𝜑)))
2221elrab3 2810 . . . . . . . . . . . 12 (0 ∈ {0, 1} → (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (0 = 0 ∨ 𝜑)))
2319, 22ax-mp 7 . . . . . . . . . . 11 (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (0 = 0 ∨ 𝜑))
2417, 23mpbir 145 . . . . . . . . . 10 0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}
25 elex2 2673 . . . . . . . . . 10 (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)})
2624, 25ax-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))
3129, 30mpbiri 167 . . . . . . . . . . . . . 14 (𝑦 = 0 → 𝑦 ≤ 1)
323eqlei2 7781 . . . . . . . . . . . . . 14 (𝑦 = 1 → 𝑦 ≤ 1)
3331, 32jaoi 688 . . . . . . . . . . . . 13 ((𝑦 = 0 ∨ 𝑦 = 1) → 𝑦 ≤ 1)
3428, 33syl 14 . . . . . . . . . . . 12 (𝑦 ∈ {0, 1} → 𝑦 ≤ 1)
3527, 34syl 14 . . . . . . . . . . 11 (𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑦 ≤ 1)
3635rgen 2459 . . . . . . . . . 10 𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1
37 breq2 3899 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑦𝑥𝑦 ≤ 1))
3837ralbidv 2411 . . . . . . . . . . 11 (𝑥 = 1 → (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1))
3938rspcev 2760 . . . . . . . . . 10 ((1 ∈ ℝ ∧ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥)
403, 36, 39mp2an 420 . . . . . . . . 9 𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥
41 prexg 4093 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ∈ V)
422, 3, 41mp2an 420 . . . . . . . . . . 11 {0, 1} ∈ V
4342rabex 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 ∨ 𝜑)}))
4645exbidv 1779 . . . . . . . . . . . 12 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑤 𝑤𝑢 ↔ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}))
47 raleq 2600 . . . . . . . . . . . . 13 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦𝑢 𝑦𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥))
4847rexbidv 2412 . . . . . . . . . . . 12 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑥 ∈ ℝ ∀𝑦𝑢 𝑦𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥))
4944, 46, 483anbi123d 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 ∨ 𝜑)}𝑦 < 𝑧))
5251imbi2d 229 . . . . . . . . . . . . . 14 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((𝑦 < 𝑥 → ∃𝑧𝑢 𝑦 < 𝑧) ↔ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
5352ralbidv 2411 . . . . . . . . . . . . 13 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝑢 𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
5450, 53anbi12d 462 . . . . . . . . . . . 12 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((∀𝑦𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝑢 𝑦 < 𝑧)) ↔ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))))
5554rexbidv 2412 . . . . . . . . . . 11 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑥 ∈ ℝ (∀𝑦𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝑢 𝑦 < 𝑧)) ↔ ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))))
5649, 55imbi12d 233 . . . . . . . . . 10 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (((𝑢 ⊆ ℝ ∧ ∃𝑤 𝑤𝑢 ∧ ∃𝑥 ∈ ℝ ∀𝑦𝑢 𝑦𝑥) → ∃𝑥 ∈ ℝ (∀𝑦𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝑢 𝑦 < 𝑧))) ↔ (({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))))
57 sup3exmid.ex . . . . . . . . . 10 ((𝑢 ⊆ ℝ ∧ ∃𝑤 𝑤𝑢 ∧ ∃𝑥 ∈ ℝ ∀𝑦𝑢 𝑦𝑥) → ∃𝑥 ∈ ℝ (∀𝑦𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝑢 𝑦 < 𝑧)))
5843, 56, 57vtocl 2711 . . . . . . . . 9 (({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
5915, 26, 40, 58mp3an 1298 . . . . . . . 8 𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))
6059a1i 9 . . . . . . 7 (⊤ → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
615, 60supclti 6837 . . . . . 6 (⊤ → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ)
6261mptru 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)))
642, 3, 62, 63mp3an 1298 . . . 4 (0 < 1 → (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1))
651, 64ax-mp 7 . . 3 (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1)
665, 60suplubti 6839 . . . . . . . 8 (⊤ → ((0 ∈ ℝ ∧ 0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < )) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧))
6766mptru 1323 . . . . . . 7 ((0 ∈ ℝ ∧ 0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < )) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧)
682, 67mpan 418 . . . . . 6 (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧)
69 df-rex 2396 . . . . . 6 (∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧 ↔ ∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧))
7068, 69sylib 121 . . . . 5 (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → ∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧))
71 eqeq1 2121 . . . . . . . . 9 (𝑗 = 𝑧 → (𝑗 = 0 ↔ 𝑧 = 0))
7271orbi1d 763 . . . . . . . 8 (𝑗 = 𝑧 → ((𝑗 = 0 ∨ 𝜑) ↔ (𝑧 = 0 ∨ 𝜑)))
7372elrab 2809 . . . . . . 7 (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)))
74 simpr 109 . . . . . . . . . 10 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 0 < 𝑧)
7574gt0ne0d 8193 . . . . . . . . 9 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝑧 ≠ 0)
7675neneqd 2303 . . . . . . . 8 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → ¬ 𝑧 = 0)
77 simplr 502 . . . . . . . 8 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → (𝑧 = 0 ∨ 𝜑))
78 orel1 697 . . . . . . . 8 𝑧 = 0 → ((𝑧 = 0 ∨ 𝜑) → 𝜑))
7976, 77, 78sylc 62 . . . . . . 7 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝜑)
8073, 79sylanb 280 . . . . . 6 ((𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑)
8180exlimiv 1560 . . . . 5 (∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑)
8270, 81syl 14 . . . 4 (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → 𝜑)
833ltnri 7779 . . . . . 6 ¬ 1 < 1
84 iba 296 . . . . . . . . . . . 12 ((𝑧 = 0 ∨ 𝜑) → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))))
8584olcs 708 . . . . . . . . . . 11 (𝜑 → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))))
8685, 73syl6rbbr 198 . . . . . . . . . 10 (𝜑 → (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ 𝑧 ∈ {0, 1}))
8786eqrdv 2113 . . . . . . . . 9 (𝜑 → {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} = {0, 1})
8887supeq1d 6826 . . . . . . . 8 (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = sup({0, 1}, ℝ, < ))
893a1i 9 . . . . . . . . . 10 (⊤ → 1 ∈ ℝ)
903elexi 2669 . . . . . . . . . . . 12 1 ∈ V
9190prid2 3596 . . . . . . . . . . 11 1 ∈ {0, 1}
9291a1i 9 . . . . . . . . . 10 (⊤ → 1 ∈ {0, 1})
93 elpri 3516 . . . . . . . . . . . 12 (𝑧 ∈ {0, 1} → (𝑧 = 0 ∨ 𝑧 = 1))
942, 3lenlti 7787 . . . . . . . . . . . . . . 15 (0 ≤ 1 ↔ ¬ 1 < 0)
9529, 94mpbi 144 . . . . . . . . . . . . . 14 ¬ 1 < 0
96 breq2 3899 . . . . . . . . . . . . . 14 (𝑧 = 0 → (1 < 𝑧 ↔ 1 < 0))
9795, 96mtbiri 647 . . . . . . . . . . . . 13 (𝑧 = 0 → ¬ 1 < 𝑧)
98 breq2 3899 . . . . . . . . . . . . . 14 (𝑧 = 1 → (1 < 𝑧 ↔ 1 < 1))
9983, 98mtbiri 647 . . . . . . . . . . . . 13 (𝑧 = 1 → ¬ 1 < 𝑧)
10097, 99jaoi 688 . . . . . . . . . . . 12 ((𝑧 = 0 ∨ 𝑧 = 1) → ¬ 1 < 𝑧)
10193, 100syl 14 . . . . . . . . . . 11 (𝑧 ∈ {0, 1} → ¬ 1 < 𝑧)
102101adantl 273 . . . . . . . . . 10 ((⊤ ∧ 𝑧 ∈ {0, 1}) → ¬ 1 < 𝑧)
1035, 89, 92, 102supmaxti 6843 . . . . . . . . 9 (⊤ → sup({0, 1}, ℝ, < ) = 1)
104103mptru 1323 . . . . . . . 8 sup({0, 1}, ℝ, < ) = 1
10588, 104syl6eq 2163 . . . . . . 7 (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = 1)
106105breq1d 3905 . . . . . 6 (𝜑 → (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 ↔ 1 < 1))
10783, 106mtbiri 647 . . . . 5 (𝜑 → ¬ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1)
108107con2i 599 . . . 4 (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 → ¬ 𝜑)
10982, 108orim12i 731 . . 3 ((0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1) → (𝜑 ∨ ¬ 𝜑))
11065, 109ax-mp 7 . 2 (𝜑 ∨ ¬ 𝜑)
111 df-dc 803 . 2 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
112110, 111mpbir 145 1 DECID 𝜑
Colors of variables: wff set class
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)
  Copyright terms: Public domain W3C validator