Step | Hyp | Ref
| Expression |
1 | | 0lt1 8074 |
. . . 4
⊢ 0 <
1 |
2 | | 0re 7948 |
. . . . 5
⊢ 0 ∈
ℝ |
3 | | 1re 7947 |
. . . . 5
⊢ 1 ∈
ℝ |
4 | | lttri3 8027 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 = 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎))) |
5 | 4 | adantl 277 |
. . . . . . 7
⊢
((⊤ ∧ (𝑎
∈ ℝ ∧ 𝑏
∈ ℝ)) → (𝑎
= 𝑏 ↔ (¬ 𝑎 < 𝑏 ∧ ¬ 𝑏 < 𝑎))) |
6 | | elrabi 2890 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ {0, 1}) |
7 | | elpri 3614 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ {0, 1} → (𝑘 = 0 ∨ 𝑘 = 1)) |
8 | 6, 7 | syl 14 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (𝑘 = 0 ∨ 𝑘 = 1)) |
9 | | eleq1 2240 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (𝑘 ∈ ℝ ↔ 0 ∈
ℝ)) |
10 | 2, 9 | mpbiri 168 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → 𝑘 ∈ ℝ) |
11 | | eleq1 2240 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1 → (𝑘 ∈ ℝ ↔ 1 ∈
ℝ)) |
12 | 3, 11 | mpbiri 168 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → 𝑘 ∈ ℝ) |
13 | 10, 12 | jaoi 716 |
. . . . . . . . . . 11
⊢ ((𝑘 = 0 ∨ 𝑘 = 1) → 𝑘 ∈ ℝ) |
14 | 8, 13 | syl 14 |
. . . . . . . . . 10
⊢ (𝑘 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → 𝑘 ∈ ℝ) |
15 | 14 | ssriv 3159 |
. . . . . . . . 9
⊢ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ |
16 | | eqid 2177 |
. . . . . . . . . . . 12
⊢ 0 =
0 |
17 | 16 | orci 731 |
. . . . . . . . . . 11
⊢ (0 = 0
∨ 𝜑) |
18 | 2 | elexi 2749 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
19 | 18 | prid1 3697 |
. . . . . . . . . . . 12
⊢ 0 ∈
{0, 1} |
20 | | eqeq1 2184 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 0 → (𝑗 = 0 ↔ 0 = 0)) |
21 | 20 | orbi1d 791 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 0 → ((𝑗 = 0 ∨ 𝜑) ↔ (0 = 0 ∨ 𝜑))) |
22 | 21 | elrab3 2894 |
. . . . . . . . . . . 12
⊢ (0 ∈
{0, 1} → (0 ∈ {𝑗
∈ {0, 1} ∣ (𝑗 =
0 ∨ 𝜑)} ↔ (0 = 0 ∨
𝜑))) |
23 | 19, 22 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (0 ∈
{𝑗 ∈ {0, 1} ∣
(𝑗 = 0 ∨ 𝜑)} ↔ (0 = 0 ∨ 𝜑)) |
24 | 17, 23 | mpbir 146 |
. . . . . . . . . 10
⊢ 0 ∈
{𝑗 ∈ {0, 1} ∣
(𝑗 = 0 ∨ 𝜑)} |
25 | | elex2 2753 |
. . . . . . . . . 10
⊢ (0 ∈
{𝑗 ∈ {0, 1} ∣
(𝑗 = 0 ∨ 𝜑)} → ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}) |
26 | 24, 25 | ax-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)) |
31 | 29, 30 | mpbiri 168 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 0 → 𝑦 ≤ 1) |
32 | 3 | eqlei2 8042 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 1 → 𝑦 ≤ 1) |
33 | 31, 32 | jaoi 716 |
. . . . . . . . . . . . 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 2530 |
. . . . . . . . . 10
⊢
∀𝑦 ∈
{𝑗 ∈ {0, 1} ∣
(𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1 |
37 | | breq2 4004 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 1)) |
38 | 37 | ralbidv 2477 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1)) |
39 | 38 | rspcev 2841 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥) |
40 | 3, 36, 39 | mp2an 426 |
. . . . . . . . 9
⊢
∃𝑥 ∈
ℝ ∀𝑦 ∈
{𝑗 ∈ {0, 1} ∣
(𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥 |
41 | | prexg 4208 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ) → {0, 1} ∈ V) |
42 | 2, 3, 41 | mp2an 426 |
. . . . . . . . . . 11
⊢ {0, 1}
∈ V |
43 | 42 | rabex 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 ∨ 𝜑)})) |
46 | 45 | exbidv 1825 |
. . . . . . . . . . . 12
⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑤 𝑤 ∈ 𝑢 ↔ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)})) |
47 | | raleq 2672 |
. . . . . . . . . . . . 13
⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥)) |
48 | 47 | rexbidv 2478 |
. . . . . . . . . . . 12
⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑢 𝑦 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥)) |
49 | 44, 46, 48 | 3anbi123d 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 ∨ 𝜑)}𝑦 < 𝑧)) |
52 | 51 | imbi2d 230 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧) ↔ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))) |
53 | 52 | ralbidv 2477 |
. . . . . . . . . . . . 13
⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))) |
54 | 50, 53 | anbi12d 473 |
. . . . . . . . . . . 12
⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → ((∀𝑦 ∈ 𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧)) ↔ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))) |
55 | 54 | rexbidv 2478 |
. . . . . . . . . . 11
⊢ (𝑢 = {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} → (∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑢 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝑢 𝑦 < 𝑧)) ↔ ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)))) |
56 | 49, 55 | imbi12d 234 |
. . . . . . . . . 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 2791 |
. . . . . . . . 9
⊢ (({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ⊆ ℝ ∧ ∃𝑤 𝑤 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 ≤ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))) |
59 | 15, 26, 40, 58 | mp3an 1337 |
. . . . . . . 8
⊢
∃𝑥 ∈
ℝ (∀𝑦 ∈
{𝑗 ∈ {0, 1} ∣
(𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧)) |
60 | 59 | a1i 9 |
. . . . . . 7
⊢ (⊤
→ ∃𝑥 ∈
ℝ (∀𝑦 ∈
{𝑗 ∈ {0, 1} ∣
(𝑗 = 0 ∨ 𝜑)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}𝑦 < 𝑧))) |
61 | 5, 60 | supclti 6991 |
. . . . . 6
⊢ (⊤
→ sup({𝑗 ∈ {0, 1}
∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∈
ℝ) |
62 | 61 | mptru 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))) |
64 | 2, 3, 62, 63 | mp3an 1337 |
. . . 4
⊢ (0 < 1
→ (0 < sup({𝑗
∈ {0, 1} ∣ (𝑗 =
0 ∨ 𝜑)}, ℝ, < )
∨ sup({𝑗 ∈ {0, 1}
∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) <
1)) |
65 | 1, 64 | ax-mp 5 |
. . 3
⊢ (0 <
sup({𝑗 ∈ {0, 1}
∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨
sup({𝑗 ∈ {0, 1}
∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) <
1) |
66 | 5, 60 | suplubti 6993 |
. . . . . . . 8
⊢ (⊤
→ ((0 ∈ ℝ ∧ 0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < )) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧)) |
67 | 66 | mptru 1362 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ 0 < sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < )) → ∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧) |
68 | 2, 67 | mpan 424 |
. . . . . 6
⊢ (0 <
sup({𝑗 ∈ {0, 1}
∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) →
∃𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}0 < 𝑧) |
69 | | df-rex 2461 |
. . . . . 6
⊢
(∃𝑧 ∈
{𝑗 ∈ {0, 1} ∣
(𝑗 = 0 ∨ 𝜑)}0 < 𝑧 ↔ ∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧)) |
70 | 68, 69 | sylib 122 |
. . . . 5
⊢ (0 <
sup({𝑗 ∈ {0, 1}
∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) →
∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧)) |
71 | | eqeq1 2184 |
. . . . . . . . 9
⊢ (𝑗 = 𝑧 → (𝑗 = 0 ↔ 𝑧 = 0)) |
72 | 71 | orbi1d 791 |
. . . . . . . 8
⊢ (𝑗 = 𝑧 → ((𝑗 = 0 ∨ 𝜑) ↔ (𝑧 = 0 ∨ 𝜑))) |
73 | 72 | elrab 2893 |
. . . . . . 7
⊢ (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑))) |
74 | | simpr 110 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 0 < 𝑧) |
75 | 74 | gt0ne0d 8459 |
. . . . . . . . 9
⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝑧 ≠ 0) |
76 | 75 | neneqd 2368 |
. . . . . . . 8
⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → ¬ 𝑧 = 0) |
77 | | simplr 528 |
. . . . . . . 8
⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → (𝑧 = 0 ∨ 𝜑)) |
78 | | orel1 725 |
. . . . . . . 8
⊢ (¬
𝑧 = 0 → ((𝑧 = 0 ∨ 𝜑) → 𝜑)) |
79 | 76, 77, 78 | sylc 62 |
. . . . . . 7
⊢ (((𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)) ∧ 0 < 𝑧) → 𝜑) |
80 | 73, 79 | sylanb 284 |
. . . . . 6
⊢ ((𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑) |
81 | 80 | exlimiv 1598 |
. . . . 5
⊢
(∃𝑧(𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ∧ 0 < 𝑧) → 𝜑) |
82 | 70, 81 | syl 14 |
. . . 4
⊢ (0 <
sup({𝑗 ∈ {0, 1}
∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) → 𝜑) |
83 | 3 | ltnri 8040 |
. . . . . 6
⊢ ¬ 1
< 1 |
84 | | iba 300 |
. . . . . . . . . . . 12
⊢ ((𝑧 = 0 ∨ 𝜑) → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)))) |
85 | 84 | olcs 736 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ {0, 1} ↔ (𝑧 ∈ {0, 1} ∧ (𝑧 = 0 ∨ 𝜑)))) |
86 | 73, 85 | bitr4id 199 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑧 ∈ {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} ↔ 𝑧 ∈ {0, 1})) |
87 | 86 | eqrdv 2175 |
. . . . . . . . 9
⊢ (𝜑 → {𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)} = {0, 1}) |
88 | 87 | supeq1d 6980 |
. . . . . . . 8
⊢ (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = sup({0, 1}, ℝ,
< )) |
89 | 3 | a1i 9 |
. . . . . . . . . 10
⊢ (⊤
→ 1 ∈ ℝ) |
90 | 3 | elexi 2749 |
. . . . . . . . . . . 12
⊢ 1 ∈
V |
91 | 90 | prid2 3698 |
. . . . . . . . . . 11
⊢ 1 ∈
{0, 1} |
92 | 91 | a1i 9 |
. . . . . . . . . 10
⊢ (⊤
→ 1 ∈ {0, 1}) |
93 | | elpri 3614 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ {0, 1} → (𝑧 = 0 ∨ 𝑧 = 1)) |
94 | 2, 3 | lenlti 8048 |
. . . . . . . . . . . . . . 15
⊢ (0 ≤ 1
↔ ¬ 1 < 0) |
95 | 29, 94 | mpbi 145 |
. . . . . . . . . . . . . 14
⊢ ¬ 1
< 0 |
96 | | breq2 4004 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 0 → (1 < 𝑧 ↔ 1 <
0)) |
97 | 95, 96 | mtbiri 675 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 0 → ¬ 1 < 𝑧) |
98 | | breq2 4004 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 1 → (1 < 𝑧 ↔ 1 <
1)) |
99 | 83, 98 | mtbiri 675 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 1 → ¬ 1 < 𝑧) |
100 | 97, 99 | jaoi 716 |
. . . . . . . . . . . 12
⊢ ((𝑧 = 0 ∨ 𝑧 = 1) → ¬ 1 < 𝑧) |
101 | 93, 100 | syl 14 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ {0, 1} → ¬ 1
< 𝑧) |
102 | 101 | adantl 277 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑧
∈ {0, 1}) → ¬ 1 < 𝑧) |
103 | 5, 89, 92, 102 | supmaxti 6997 |
. . . . . . . . 9
⊢ (⊤
→ sup({0, 1}, ℝ, < ) = 1) |
104 | 103 | mptru 1362 |
. . . . . . . 8
⊢ sup({0,
1}, ℝ, < ) = 1 |
105 | 88, 104 | eqtrdi 2226 |
. . . . . . 7
⊢ (𝜑 → sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) = 1) |
106 | 105 | breq1d 4010 |
. . . . . 6
⊢ (𝜑 → (sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1 ↔ 1 <
1)) |
107 | 83, 106 | mtbiri 675 |
. . . . 5
⊢ (𝜑 → ¬ sup({𝑗 ∈ {0, 1} ∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1) |
108 | 107 | con2i 627 |
. . . 4
⊢
(sup({𝑗 ∈ {0,
1} ∣ (𝑗 = 0 ∨
𝜑)}, ℝ, < ) < 1
→ ¬ 𝜑) |
109 | 82, 108 | orim12i 759 |
. . 3
⊢ ((0 <
sup({𝑗 ∈ {0, 1}
∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) ∨
sup({𝑗 ∈ {0, 1}
∣ (𝑗 = 0 ∨ 𝜑)}, ℝ, < ) < 1) →
(𝜑 ∨ ¬ 𝜑)) |
110 | 65, 109 | ax-mp 5 |
. 2
⊢ (𝜑 ∨ ¬ 𝜑) |
111 | | df-dc 835 |
. 2
⊢
(DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) |
112 | 110, 111 | mpbir 146 |
1
⊢
DECID 𝜑 |