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

Theorem sup3exmid 8928
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 8098 . . . 4 0 < 1
2 0re 7971 . . . . 5 0 ∈ ℝ
3 1re 7970 . . . . 5 1 ∈ ℝ
4 lttri3 8051 . . . . . . . 8 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
54adantl 277 . . . . . . 7 ((⊤ ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
6 elrabi 2902 . . . . . . . . . . . 12 (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ {0, 1})
7 elpri 3627 . . . . . . . . . . . 12 (𝑘 ∈ {0, 1} → (𝑘 = 0 ∨ 𝑘 = 1))
86, 7syl 14 . . . . . . . . . . 11 (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑘 = 0 ∨ 𝑘 = 1))
9 eleq1 2250 . . . . . . . . . . . . 13 (𝑘 = 0 → (𝑘 ∈ ℝ ↔ 0 ∈ ℝ))
102, 9mpbiri 168 . . . . . . . . . . . 12 (𝑘 = 0 → 𝑘 ∈ ℝ)
11 eleq1 2250 . . . . . . . . . . . . 13 (𝑘 = 1 → (𝑘 ∈ ℝ ↔ 1 ∈ ℝ))
123, 11mpbiri 168 . . . . . . . . . . . 12 (𝑘 = 1 → 𝑘 ∈ ℝ)
1310, 12jaoi 717 . . . . . . . . . . 11 ((𝑘 = 0 ∨ 𝑘 = 1) → 𝑘 ∈ ℝ)
148, 13syl 14 . . . . . . . . . 10 (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ ℝ)
1514ssriv 3171 . . . . . . . . 9 {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ
16 eqid 2187 . . . . . . . . . . . 12 0 = 0
1716orci 732 . . . . . . . . . . 11 (0 = 0 ∨ 𝜑)
182elexi 2761 . . . . . . . . . . . . 13 0 ∈ V
1918prid1 3710 . . . . . . . . . . . 12 0 ∈ {0, 1}
20 eqeq1 2194 . . . . . . . . . . . . . 14 (𝑗 = 0 → (𝑗 = 0 ↔ 0 = 0))
2120orbi1d 792 . . . . . . . . . . . . 13 (𝑗 = 0 → ((𝑗 = 0 ∨ 𝜑) ↔ (0 = 0 ∨ 𝜑)))
2221elrab3 2906 . . . . . . . . . . . 12 (0 ∈ {0, 1} → (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (0 = 0 ∨ 𝜑)))
2319, 22ax-mp 5 . . . . . . . . . . 11 (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (0 = 0 ∨ 𝜑))
2417, 23mpbir 146 . . . . . . . . . 10 0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}
25 elex2 2765 . . . . . . . . . 10 (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)})
2624, 25ax-mp 5 . . . . . . . . 9 𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}
27 elrabi 2902 . . . . . . . . . . . 12 (𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑦 ∈ {0, 1})
28 elpri 3627 . . . . . . . . . . . . 13 (𝑦 ∈ {0, 1} → (𝑦 = 0 ∨ 𝑦 = 1))
29 0le1 8452 . . . . . . . . . . . . . . 15 0 ≤ 1
30 breq1 4018 . . . . . . . . . . . . . . 15 (𝑦 = 0 → (𝑦 ≤ 1 ↔ 0 ≤ 1))
3129, 30mpbiri 168 . . . . . . . . . . . . . 14 (𝑦 = 0 → 𝑦 ≤ 1)
323eqlei2 8066 . . . . . . . . . . . . . 14 (𝑦 = 1 → 𝑦 ≤ 1)
3331, 32jaoi 717 . . . . . . . . . . . . 13 ((𝑦 = 0 ∨ 𝑦 = 1) → 𝑦 ≤ 1)
3428, 33syl 14 . . . . . . . . . . . 12 (𝑦 ∈ {0, 1} → 𝑦 ≤ 1)
3527, 34syl 14 . . . . . . . . . . 11 (𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑦 ≤ 1)
3635rgen 2540 . . . . . . . . . 10 𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1
37 breq2 4019 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑦𝑥𝑦 ≤ 1))
3837ralbidv 2487 . . . . . . . . . . 11 (𝑥 = 1 → (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1))
3938rspcev 2853 . . . . . . . . . 10 ((1 ∈ ℝ ∧ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥)
403, 36, 39mp2an 426 . . . . . . . . 9 𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥
41 prexg 4223 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ∈ V)
422, 3, 41mp2an 426 . . . . . . . . . . 11 {0, 1} ∈ V
4342rabex 4159 . . . . . . . . . 10 {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∈ V
44 sseq1 3190 . . . . . . . . . . . 12 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑢 ⊆ ℝ ↔ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ))
45 eleq2 2251 . . . . . . . . . . . . 13 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑤𝑢𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}))
4645exbidv 1835 . . . . . . . . . . . 12 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑤 𝑤𝑢 ↔ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}))
47 raleq 2683 . . . . . . . . . . . . 13 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦𝑢 𝑦𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥))
4847rexbidv 2488 . . . . . . . . . . . 12 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑥 ∈ ℝ ∀𝑦𝑢 𝑦𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥))
4944, 46, 483anbi123d 1322 . . . . . . . . . . 11 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((𝑢 ⊆ ℝ ∧ ∃𝑤 𝑤𝑢 ∧ ∃𝑥 ∈ ℝ ∀𝑦𝑢 𝑦𝑥) ↔ ({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥)))
50 raleq 2683 . . . . . . . . . . . . 13 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦𝑢 ¬ 𝑥 < 𝑦 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦))
51 rexeq 2684 . . . . . . . . . . . . . . 15 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑧𝑢 𝑦 < 𝑧 ↔ ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))
5251imbi2d 230 . . . . . . . . . . . . . 14 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((𝑦 < 𝑥 → ∃𝑧𝑢 𝑦 < 𝑧) ↔ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
5352ralbidv 2487 . . . . . . . . . . . . 13 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝑢 𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
5450, 53anbi12d 473 . . . . . . . . . . . 12 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((∀𝑦𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝑢 𝑦 < 𝑧)) ↔ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))))
5554rexbidv 2488 . . . . . . . . . . 11 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑥 ∈ ℝ (∀𝑦𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝑢 𝑦 < 𝑧)) ↔ ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))))
5649, 55imbi12d 234 . . . . . . . . . 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 2803 . . . . . . . . 9 (({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
5915, 26, 40, 58mp3an 1347 . . . . . . . 8 𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))
6059a1i 9 . . . . . . 7 (⊤ → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
615, 60supclti 7011 . . . . . 6 (⊤ → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ)
6261mptru 1372 . . . . 5 sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ
63 axltwlin 8039 . . . . 5 ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ) → (0 < 1 → (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1)))
642, 3, 62, 63mp3an 1347 . . . 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 7013 . . . . . . . 8 (⊤ → ((0 ∈ ℝ ∧ 0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < )) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧))
6766mptru 1372 . . . . . . 7 ((0 ∈ ℝ ∧ 0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < )) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧)
682, 67mpan 424 . . . . . 6 (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧)
69 df-rex 2471 . . . . . 6 (∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧 ↔ ∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧))
7068, 69sylib 122 . . . . 5 (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → ∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧))
71 eqeq1 2194 . . . . . . . . 9 (𝑗 = 𝑧 → (𝑗 = 0 ↔ 𝑧 = 0))
7271orbi1d 792 . . . . . . . 8 (𝑗 = 𝑧 → ((𝑗 = 0 ∨ 𝜑) ↔ (𝑧 = 0 ∨ 𝜑)))
7372elrab 2905 . . . . . . 7 (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)))
74 simpr 110 . . . . . . . . . 10 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 0 < 𝑧)
7574gt0ne0d 8483 . . . . . . . . 9 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝑧 ≠ 0)
7675neneqd 2378 . . . . . . . 8 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → ¬ 𝑧 = 0)
77 simplr 528 . . . . . . . 8 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → (𝑧 = 0 ∨ 𝜑))
78 orel1 726 . . . . . . . 8 𝑧 = 0 → ((𝑧 = 0 ∨ 𝜑) → 𝜑))
7976, 77, 78sylc 62 . . . . . . 7 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝜑)
8073, 79sylanb 284 . . . . . 6 ((𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑)
8180exlimiv 1608 . . . . 5 (∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑)
8270, 81syl 14 . . . 4 (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → 𝜑)
833ltnri 8064 . . . . . 6 ¬ 1 < 1
84 iba 300 . . . . . . . . . . . 12 ((𝑧 = 0 ∨ 𝜑) → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))))
8584olcs 737 . . . . . . . . . . 11 (𝜑 → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))))
8673, 85bitr4id 199 . . . . . . . . . 10 (𝜑 → (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ 𝑧 ∈ {0, 1}))
8786eqrdv 2185 . . . . . . . . 9 (𝜑 → {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} = {0, 1})
8887supeq1d 7000 . . . . . . . 8 (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = sup({0, 1}, ℝ, < ))
893a1i 9 . . . . . . . . . 10 (⊤ → 1 ∈ ℝ)
903elexi 2761 . . . . . . . . . . . 12 1 ∈ V
9190prid2 3711 . . . . . . . . . . 11 1 ∈ {0, 1}
9291a1i 9 . . . . . . . . . 10 (⊤ → 1 ∈ {0, 1})
93 elpri 3627 . . . . . . . . . . . 12 (𝑧 ∈ {0, 1} → (𝑧 = 0 ∨ 𝑧 = 1))
942, 3lenlti 8072 . . . . . . . . . . . . . . 15 (0 ≤ 1 ↔ ¬ 1 < 0)
9529, 94mpbi 145 . . . . . . . . . . . . . 14 ¬ 1 < 0
96 breq2 4019 . . . . . . . . . . . . . 14 (𝑧 = 0 → (1 < 𝑧 ↔ 1 < 0))
9795, 96mtbiri 676 . . . . . . . . . . . . 13 (𝑧 = 0 → ¬ 1 < 𝑧)
98 breq2 4019 . . . . . . . . . . . . . 14 (𝑧 = 1 → (1 < 𝑧 ↔ 1 < 1))
9983, 98mtbiri 676 . . . . . . . . . . . . 13 (𝑧 = 1 → ¬ 1 < 𝑧)
10097, 99jaoi 717 . . . . . . . . . . . 12 ((𝑧 = 0 ∨ 𝑧 = 1) → ¬ 1 < 𝑧)
10193, 100syl 14 . . . . . . . . . . 11 (𝑧 ∈ {0, 1} → ¬ 1 < 𝑧)
102101adantl 277 . . . . . . . . . 10 ((⊤ ∧ 𝑧 ∈ {0, 1}) → ¬ 1 < 𝑧)
1035, 89, 92, 102supmaxti 7017 . . . . . . . . 9 (⊤ → sup({0, 1}, ℝ, < ) = 1)
104103mptru 1372 . . . . . . . 8 sup({0, 1}, ℝ, < ) = 1
10588, 104eqtrdi 2236 . . . . . . 7 (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = 1)
106105breq1d 4025 . . . . . 6 (𝜑 → (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 ↔ 1 < 1))
10783, 106mtbiri 676 . . . . 5 (𝜑 → ¬ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1)
108107con2i 628 . . . 4 (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 → ¬ 𝜑)
10982, 108orim12i 760 . . 3 ((0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1) → (𝜑 ∨ ¬ 𝜑))
11065, 109ax-mp 5 . 2 (𝜑 ∨ ¬ 𝜑)
111 df-dc 836 . 2 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
112110, 111mpbir 146 1 DECID 𝜑
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 709  DECID wdc 835  w3a 979   = wceq 1363  wtru 1364  wex 1502  wcel 2158  wral 2465  wrex 2466  {crab 2469  Vcvv 2749  wss 3141  {cpr 3605   class class class wbr 4015  supcsup 6995  cr 7824  0cc0 7825  1c1 7826   < clt 8006  cle 8007
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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-cnex 7916  ax-resscn 7917  ax-1re 7919  ax-addrcl 7922  ax-0lt1 7931  ax-rnegex 7934  ax-pre-ltirr 7937  ax-pre-ltwlin 7938  ax-pre-lttrn 7939  ax-pre-apti 7940
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-br 4016  df-opab 4077  df-xp 4644  df-cnv 4646  df-iota 5190  df-riota 5844  df-sup 6997  df-pnf 8008  df-mnf 8009  df-xr 8010  df-ltxr 8011  df-le 8012
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator