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

Theorem sup3exmid 8766
 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 7940 . . . 4 0 < 1
2 0re 7817 . . . . 5 0 ∈ ℝ
3 1re 7816 . . . . 5 1 ∈ ℝ
4 lttri3 7895 . . . . . . . 8 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
54adantl 275 . . . . . . 7 ((⊤ ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
6 elrabi 2842 . . . . . . . . . . . 12 (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ {0, 1})
7 elpri 3556 . . . . . . . . . . . 12 (𝑘 ∈ {0, 1} → (𝑘 = 0 ∨ 𝑘 = 1))
86, 7syl 14 . . . . . . . . . . 11 (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑘 = 0 ∨ 𝑘 = 1))
9 eleq1 2203 . . . . . . . . . . . . 13 (𝑘 = 0 → (𝑘 ∈ ℝ ↔ 0 ∈ ℝ))
102, 9mpbiri 167 . . . . . . . . . . . 12 (𝑘 = 0 → 𝑘 ∈ ℝ)
11 eleq1 2203 . . . . . . . . . . . . 13 (𝑘 = 1 → (𝑘 ∈ ℝ ↔ 1 ∈ ℝ))
123, 11mpbiri 167 . . . . . . . . . . . 12 (𝑘 = 1 → 𝑘 ∈ ℝ)
1310, 12jaoi 706 . . . . . . . . . . 11 ((𝑘 = 0 ∨ 𝑘 = 1) → 𝑘 ∈ ℝ)
148, 13syl 14 . . . . . . . . . 10 (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ ℝ)
1514ssriv 3107 . . . . . . . . 9 {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ
16 eqid 2140 . . . . . . . . . . . 12 0 = 0
1716orci 721 . . . . . . . . . . 11 (0 = 0 ∨ 𝜑)
182elexi 2702 . . . . . . . . . . . . 13 0 ∈ V
1918prid1 3638 . . . . . . . . . . . 12 0 ∈ {0, 1}
20 eqeq1 2147 . . . . . . . . . . . . . 14 (𝑗 = 0 → (𝑗 = 0 ↔ 0 = 0))
2120orbi1d 781 . . . . . . . . . . . . 13 (𝑗 = 0 → ((𝑗 = 0 ∨ 𝜑) ↔ (0 = 0 ∨ 𝜑)))
2221elrab3 2846 . . . . . . . . . . . 12 (0 ∈ {0, 1} → (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (0 = 0 ∨ 𝜑)))
2319, 22ax-mp 5 . . . . . . . . . . 11 (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (0 = 0 ∨ 𝜑))
2417, 23mpbir 145 . . . . . . . . . 10 0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}
25 elex2 2706 . . . . . . . . . 10 (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)})
2624, 25ax-mp 5 . . . . . . . . 9 𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}
27 elrabi 2842 . . . . . . . . . . . 12 (𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑦 ∈ {0, 1})
28 elpri 3556 . . . . . . . . . . . . 13 (𝑦 ∈ {0, 1} → (𝑦 = 0 ∨ 𝑦 = 1))
29 0le1 8294 . . . . . . . . . . . . . . 15 0 ≤ 1
30 breq1 3941 . . . . . . . . . . . . . . 15 (𝑦 = 0 → (𝑦 ≤ 1 ↔ 0 ≤ 1))
3129, 30mpbiri 167 . . . . . . . . . . . . . 14 (𝑦 = 0 → 𝑦 ≤ 1)
323eqlei2 7909 . . . . . . . . . . . . . 14 (𝑦 = 1 → 𝑦 ≤ 1)
3331, 32jaoi 706 . . . . . . . . . . . . 13 ((𝑦 = 0 ∨ 𝑦 = 1) → 𝑦 ≤ 1)
3428, 33syl 14 . . . . . . . . . . . 12 (𝑦 ∈ {0, 1} → 𝑦 ≤ 1)
3527, 34syl 14 . . . . . . . . . . 11 (𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑦 ≤ 1)
3635rgen 2489 . . . . . . . . . 10 𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1
37 breq2 3942 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑦𝑥𝑦 ≤ 1))
3837ralbidv 2439 . . . . . . . . . . 11 (𝑥 = 1 → (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1))
3938rspcev 2794 . . . . . . . . . 10 ((1 ∈ ℝ ∧ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥)
403, 36, 39mp2an 423 . . . . . . . . 9 𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥
41 prexg 4143 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ∈ V)
422, 3, 41mp2an 423 . . . . . . . . . . 11 {0, 1} ∈ V
4342rabex 4081 . . . . . . . . . 10 {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∈ V
44 sseq1 3126 . . . . . . . . . . . 12 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑢 ⊆ ℝ ↔ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ))
45 eleq2 2204 . . . . . . . . . . . . 13 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑤𝑢𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}))
4645exbidv 1798 . . . . . . . . . . . 12 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑤 𝑤𝑢 ↔ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}))
47 raleq 2630 . . . . . . . . . . . . 13 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦𝑢 𝑦𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥))
4847rexbidv 2440 . . . . . . . . . . . 12 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑥 ∈ ℝ ∀𝑦𝑢 𝑦𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥))
4944, 46, 483anbi123d 1291 . . . . . . . . . . 11 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((𝑢 ⊆ ℝ ∧ ∃𝑤 𝑤𝑢 ∧ ∃𝑥 ∈ ℝ ∀𝑦𝑢 𝑦𝑥) ↔ ({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥)))
50 raleq 2630 . . . . . . . . . . . . 13 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦𝑢 ¬ 𝑥 < 𝑦 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦))
51 rexeq 2631 . . . . . . . . . . . . . . 15 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑧𝑢 𝑦 < 𝑧 ↔ ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))
5251imbi2d 229 . . . . . . . . . . . . . 14 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((𝑦 < 𝑥 → ∃𝑧𝑢 𝑦 < 𝑧) ↔ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
5352ralbidv 2439 . . . . . . . . . . . . 13 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝑢 𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
5450, 53anbi12d 465 . . . . . . . . . . . 12 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((∀𝑦𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝑢 𝑦 < 𝑧)) ↔ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))))
5554rexbidv 2440 . . . . . . . . . . 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 2744 . . . . . . . . 9 (({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
5915, 26, 40, 58mp3an 1316 . . . . . . . 8 𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))
6059a1i 9 . . . . . . 7 (⊤ → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
615, 60supclti 6901 . . . . . 6 (⊤ → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ)
6261mptru 1341 . . . . 5 sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ
63 axltwlin 7883 . . . . 5 ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ) → (0 < 1 → (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1)))
642, 3, 62, 63mp3an 1316 . . . 4 (0 < 1 → (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1))
651, 64ax-mp 5 . . 3 (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1)
665, 60suplubti 6903 . . . . . . . 8 (⊤ → ((0 ∈ ℝ ∧ 0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < )) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧))
6766mptru 1341 . . . . . . 7 ((0 ∈ ℝ ∧ 0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < )) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧)
682, 67mpan 421 . . . . . 6 (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧)
69 df-rex 2423 . . . . . 6 (∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧 ↔ ∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧))
7068, 69sylib 121 . . . . 5 (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → ∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧))
71 eqeq1 2147 . . . . . . . . 9 (𝑗 = 𝑧 → (𝑗 = 0 ↔ 𝑧 = 0))
7271orbi1d 781 . . . . . . . 8 (𝑗 = 𝑧 → ((𝑗 = 0 ∨ 𝜑) ↔ (𝑧 = 0 ∨ 𝜑)))
7372elrab 2845 . . . . . . 7 (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)))
74 simpr 109 . . . . . . . . . 10 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 0 < 𝑧)
7574gt0ne0d 8325 . . . . . . . . 9 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝑧 ≠ 0)
7675neneqd 2330 . . . . . . . 8 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → ¬ 𝑧 = 0)
77 simplr 520 . . . . . . . 8 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → (𝑧 = 0 ∨ 𝜑))
78 orel1 715 . . . . . . . 8 𝑧 = 0 → ((𝑧 = 0 ∨ 𝜑) → 𝜑))
7976, 77, 78sylc 62 . . . . . . 7 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝜑)
8073, 79sylanb 282 . . . . . 6 ((𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑)
8180exlimiv 1578 . . . . 5 (∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑)
8270, 81syl 14 . . . 4 (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → 𝜑)
833ltnri 7907 . . . . . 6 ¬ 1 < 1
84 iba 298 . . . . . . . . . . . 12 ((𝑧 = 0 ∨ 𝜑) → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))))
8584olcs 726 . . . . . . . . . . 11 (𝜑 → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))))
8673, 85bitr4id 198 . . . . . . . . . 10 (𝜑 → (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ 𝑧 ∈ {0, 1}))
8786eqrdv 2138 . . . . . . . . 9 (𝜑 → {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} = {0, 1})
8887supeq1d 6890 . . . . . . . 8 (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = sup({0, 1}, ℝ, < ))
893a1i 9 . . . . . . . . . 10 (⊤ → 1 ∈ ℝ)
903elexi 2702 . . . . . . . . . . . 12 1 ∈ V
9190prid2 3639 . . . . . . . . . . 11 1 ∈ {0, 1}
9291a1i 9 . . . . . . . . . 10 (⊤ → 1 ∈ {0, 1})
93 elpri 3556 . . . . . . . . . . . 12 (𝑧 ∈ {0, 1} → (𝑧 = 0 ∨ 𝑧 = 1))
942, 3lenlti 7915 . . . . . . . . . . . . . . 15 (0 ≤ 1 ↔ ¬ 1 < 0)
9529, 94mpbi 144 . . . . . . . . . . . . . 14 ¬ 1 < 0
96 breq2 3942 . . . . . . . . . . . . . 14 (𝑧 = 0 → (1 < 𝑧 ↔ 1 < 0))
9795, 96mtbiri 665 . . . . . . . . . . . . 13 (𝑧 = 0 → ¬ 1 < 𝑧)
98 breq2 3942 . . . . . . . . . . . . . 14 (𝑧 = 1 → (1 < 𝑧 ↔ 1 < 1))
9983, 98mtbiri 665 . . . . . . . . . . . . 13 (𝑧 = 1 → ¬ 1 < 𝑧)
10097, 99jaoi 706 . . . . . . . . . . . 12 ((𝑧 = 0 ∨ 𝑧 = 1) → ¬ 1 < 𝑧)
10193, 100syl 14 . . . . . . . . . . 11 (𝑧 ∈ {0, 1} → ¬ 1 < 𝑧)
102101adantl 275 . . . . . . . . . 10 ((⊤ ∧ 𝑧 ∈ {0, 1}) → ¬ 1 < 𝑧)
1035, 89, 92, 102supmaxti 6907 . . . . . . . . 9 (⊤ → sup({0, 1}, ℝ, < ) = 1)
104103mptru 1341 . . . . . . . 8 sup({0, 1}, ℝ, < ) = 1
10588, 104eqtrdi 2189 . . . . . . 7 (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = 1)
106105breq1d 3948 . . . . . 6 (𝜑 → (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 ↔ 1 < 1))
10783, 106mtbiri 665 . . . . 5 (𝜑 → ¬ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1)
108107con2i 617 . . . 4 (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 → ¬ 𝜑)
10982, 108orim12i 749 . . 3 ((0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1) → (𝜑 ∨ ¬ 𝜑))
11065, 109ax-mp 5 . 2 (𝜑 ∨ ¬ 𝜑)
111 df-dc 821 . 2 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
112110, 111mpbir 145 1 DECID 𝜑
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 820   ∧ w3a 963   = wceq 1332  ⊤wtru 1333  ∃wex 1469   ∈ wcel 1481  ∀wral 2417  ∃wrex 2418  {crab 2421  Vcvv 2690   ⊆ wss 3077  {cpr 3534   class class class wbr 3938  supcsup 6885  ℝcr 7670  0cc0 7671  1c1 7672   < clt 7851   ≤ cle 7852 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4055  ax-pow 4107  ax-pr 4141  ax-un 4365  ax-setind 4462  ax-cnex 7762  ax-resscn 7763  ax-1re 7765  ax-addrcl 7768  ax-0lt1 7777  ax-rnegex 7780  ax-pre-ltirr 7783  ax-pre-ltwlin 7784  ax-pre-lttrn 7785  ax-pre-apti 7786 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rmo 2425  df-rab 2426  df-v 2692  df-sbc 2915  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-br 3939  df-opab 3999  df-xp 4556  df-cnv 4558  df-iota 5099  df-riota 5741  df-sup 6887  df-pnf 7853  df-mnf 7854  df-xr 7855  df-ltxr 7856  df-le 7857 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator