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

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.
StepHypRef Expression
1 0lt1 8074 . . . 4 0 < 1
2 0re 7948 . . . . 5 0 ∈ ℝ
3 1re 7947 . . . . 5 1 ∈ ℝ
4 lttri3 8027 . . . . . . . 8 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
54adantl 277 . . . . . . 7 ((⊤ ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎)))
6 elrabi 2890 . . . . . . . . . . . 12 (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ {0, 1})
7 elpri 3614 . . . . . . . . . . . 12 (𝑘 ∈ {0, 1} → (𝑘 = 0 ∨ 𝑘 = 1))
86, 7syl 14 . . . . . . . . . . 11 (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑘 = 0 ∨ 𝑘 = 1))
9 eleq1 2240 . . . . . . . . . . . . 13 (𝑘 = 0 → (𝑘 ∈ ℝ ↔ 0 ∈ ℝ))
102, 9mpbiri 168 . . . . . . . . . . . 12 (𝑘 = 0 → 𝑘 ∈ ℝ)
11 eleq1 2240 . . . . . . . . . . . . 13 (𝑘 = 1 → (𝑘 ∈ ℝ ↔ 1 ∈ ℝ))
123, 11mpbiri 168 . . . . . . . . . . . 12 (𝑘 = 1 → 𝑘 ∈ ℝ)
1310, 12jaoi 716 . . . . . . . . . . 11 ((𝑘 = 0 ∨ 𝑘 = 1) → 𝑘 ∈ ℝ)
148, 13syl 14 . . . . . . . . . 10 (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ ℝ)
1514ssriv 3159 . . . . . . . . 9 {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ
16 eqid 2177 . . . . . . . . . . . 12 0 = 0
1716orci 731 . . . . . . . . . . 11 (0 = 0 ∨ 𝜑)
182elexi 2749 . . . . . . . . . . . . 13 0 ∈ V
1918prid1 3697 . . . . . . . . . . . 12 0 ∈ {0, 1}
20 eqeq1 2184 . . . . . . . . . . . . . 14 (𝑗 = 0 → (𝑗 = 0 ↔ 0 = 0))
2120orbi1d 791 . . . . . . . . . . . . 13 (𝑗 = 0 → ((𝑗 = 0 ∨ 𝜑) ↔ (0 = 0 ∨ 𝜑)))
2221elrab3 2894 . . . . . . . . . . . 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 2753 . . . . . . . . . 10 (0 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)})
2624, 25ax-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))
3129, 30mpbiri 168 . . . . . . . . . . . . . 14 (𝑦 = 0 → 𝑦 ≤ 1)
323eqlei2 8042 . . . . . . . . . . . . . 14 (𝑦 = 1 → 𝑦 ≤ 1)
3331, 32jaoi 716 . . . . . . . . . . . . 13 ((𝑦 = 0 ∨ 𝑦 = 1) → 𝑦 ≤ 1)
3428, 33syl 14 . . . . . . . . . . . 12 (𝑦 ∈ {0, 1} → 𝑦 ≤ 1)
3527, 34syl 14 . . . . . . . . . . 11 (𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑦 ≤ 1)
3635rgen 2530 . . . . . . . . . 10 𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1
37 breq2 4004 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑦𝑥𝑦 ≤ 1))
3837ralbidv 2477 . . . . . . . . . . 11 (𝑥 = 1 → (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1))
3938rspcev 2841 . . . . . . . . . 10 ((1 ∈ ℝ ∧ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥)
403, 36, 39mp2an 426 . . . . . . . . 9 𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥
41 prexg 4208 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ∈ V)
422, 3, 41mp2an 426 . . . . . . . . . . 11 {0, 1} ∈ V
4342rabex 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 ∨ 𝜑)}))
4645exbidv 1825 . . . . . . . . . . . 12 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑤 𝑤𝑢 ↔ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}))
47 raleq 2672 . . . . . . . . . . . . 13 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦𝑢 𝑦𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥))
4847rexbidv 2478 . . . . . . . . . . . 12 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑥 ∈ ℝ ∀𝑦𝑢 𝑦𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥))
4944, 46, 483anbi123d 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 ∨ 𝜑)}𝑦 < 𝑧))
5251imbi2d 230 . . . . . . . . . . . . . 14 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((𝑦 < 𝑥 → ∃𝑧𝑢 𝑦 < 𝑧) ↔ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
5352ralbidv 2477 . . . . . . . . . . . . 13 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝑢 𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
5450, 53anbi12d 473 . . . . . . . . . . . 12 (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((∀𝑦𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝑢 𝑦 < 𝑧)) ↔ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))))
5554rexbidv 2478 . . . . . . . . . . 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 2791 . . . . . . . . 9 (({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
5915, 26, 40, 58mp3an 1337 . . . . . . . 8 𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))
6059a1i 9 . . . . . . 7 (⊤ → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))
615, 60supclti 6991 . . . . . 6 (⊤ → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈ ℝ)
6261mptru 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)))
642, 3, 62, 63mp3an 1337 . . . 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 6993 . . . . . . . 8 (⊤ → ((0 ∈ ℝ ∧ 0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < )) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧))
6766mptru 1362 . . . . . . 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 2461 . . . . . 6 (∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧 ↔ ∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧))
7068, 69sylib 122 . . . . 5 (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → ∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧))
71 eqeq1 2184 . . . . . . . . 9 (𝑗 = 𝑧 → (𝑗 = 0 ↔ 𝑧 = 0))
7271orbi1d 791 . . . . . . . 8 (𝑗 = 𝑧 → ((𝑗 = 0 ∨ 𝜑) ↔ (𝑧 = 0 ∨ 𝜑)))
7372elrab 2893 . . . . . . 7 (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)))
74 simpr 110 . . . . . . . . . 10 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 0 < 𝑧)
7574gt0ne0d 8459 . . . . . . . . 9 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝑧 ≠ 0)
7675neneqd 2368 . . . . . . . 8 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → ¬ 𝑧 = 0)
77 simplr 528 . . . . . . . 8 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → (𝑧 = 0 ∨ 𝜑))
78 orel1 725 . . . . . . . 8 𝑧 = 0 → ((𝑧 = 0 ∨ 𝜑) → 𝜑))
7976, 77, 78sylc 62 . . . . . . 7 (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝜑)
8073, 79sylanb 284 . . . . . 6 ((𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑)
8180exlimiv 1598 . . . . 5 (∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑)
8270, 81syl 14 . . . 4 (0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → 𝜑)
833ltnri 8040 . . . . . 6 ¬ 1 < 1
84 iba 300 . . . . . . . . . . . 12 ((𝑧 = 0 ∨ 𝜑) → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))))
8584olcs 736 . . . . . . . . . . 11 (𝜑 → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))))
8673, 85bitr4id 199 . . . . . . . . . 10 (𝜑 → (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ 𝑧 ∈ {0, 1}))
8786eqrdv 2175 . . . . . . . . 9 (𝜑 → {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} = {0, 1})
8887supeq1d 6980 . . . . . . . 8 (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = sup({0, 1}, ℝ, < ))
893a1i 9 . . . . . . . . . 10 (⊤ → 1 ∈ ℝ)
903elexi 2749 . . . . . . . . . . . 12 1 ∈ V
9190prid2 3698 . . . . . . . . . . 11 1 ∈ {0, 1}
9291a1i 9 . . . . . . . . . 10 (⊤ → 1 ∈ {0, 1})
93 elpri 3614 . . . . . . . . . . . 12 (𝑧 ∈ {0, 1} → (𝑧 = 0 ∨ 𝑧 = 1))
942, 3lenlti 8048 . . . . . . . . . . . . . . 15 (0 ≤ 1 ↔ ¬ 1 < 0)
9529, 94mpbi 145 . . . . . . . . . . . . . 14 ¬ 1 < 0
96 breq2 4004 . . . . . . . . . . . . . 14 (𝑧 = 0 → (1 < 𝑧 ↔ 1 < 0))
9795, 96mtbiri 675 . . . . . . . . . . . . 13 (𝑧 = 0 → ¬ 1 < 𝑧)
98 breq2 4004 . . . . . . . . . . . . . 14 (𝑧 = 1 → (1 < 𝑧 ↔ 1 < 1))
9983, 98mtbiri 675 . . . . . . . . . . . . 13 (𝑧 = 1 → ¬ 1 < 𝑧)
10097, 99jaoi 716 . . . . . . . . . . . 12 ((𝑧 = 0 ∨ 𝑧 = 1) → ¬ 1 < 𝑧)
10193, 100syl 14 . . . . . . . . . . 11 (𝑧 ∈ {0, 1} → ¬ 1 < 𝑧)
102101adantl 277 . . . . . . . . . 10 ((⊤ ∧ 𝑧 ∈ {0, 1}) → ¬ 1 < 𝑧)
1035, 89, 92, 102supmaxti 6997 . . . . . . . . 9 (⊤ → sup({0, 1}, ℝ, < ) = 1)
104103mptru 1362 . . . . . . . 8 sup({0, 1}, ℝ, < ) = 1
10588, 104eqtrdi 2226 . . . . . . 7 (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = 1)
106105breq1d 4010 . . . . . 6 (𝜑 → (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 ↔ 1 < 1))
10783, 106mtbiri 675 . . . . 5 (𝜑 → ¬ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1)
108107con2i 627 . . . 4 (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 → ¬ 𝜑)
10982, 108orim12i 759 . . 3 ((0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1) → (𝜑 ∨ ¬ 𝜑))
11065, 109ax-mp 5 . 2 (𝜑 ∨ ¬ 𝜑)
111 df-dc 835 . 2 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
112110, 111mpbir 146 1 DECID 𝜑
Colors of variables: wff set class
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)
  Copyright terms: Public domain W3C validator