Step | Hyp | Ref
| Expression |
1 | | df-exmid 4156 |
. 2
⊢
(EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} →
DECID ∅ ∈ 𝑥)) |
2 | | df-dc 821 |
. . . . 5
⊢
(DECID ∅ ∈ 𝑥 ↔ (∅ ∈ 𝑥 ∨ ¬ ∅ ∈ 𝑥)) |
3 | | orcom 718 |
. . . . . 6
⊢ ((∅
∈ 𝑥 ∨ ¬ ∅
∈ 𝑥) ↔ (¬
∅ ∈ 𝑥 ∨
∅ ∈ 𝑥)) |
4 | | simpll 519 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → 𝑥 ⊆ {∅}) |
5 | | simpr 109 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
6 | 4, 5 | sseldd 3129 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → 𝑦 ∈ {∅}) |
7 | | velsn 3577 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ {∅} ↔ 𝑦 = ∅) |
8 | 6, 7 | sylib 121 |
. . . . . . . . . . . 12
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → 𝑦 = ∅) |
9 | 8, 5 | eqeltrrd 2235 |
. . . . . . . . . . 11
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → ∅ ∈ 𝑥) |
10 | | simplr 520 |
. . . . . . . . . . 11
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → ¬ ∅ ∈ 𝑥) |
11 | 9, 10 | pm2.65da 651 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) →
¬ 𝑦 ∈ 𝑥) |
12 | 11 | eq0rdv 3438 |
. . . . . . . . 9
⊢ ((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) →
𝑥 =
∅) |
13 | 12 | ex 114 |
. . . . . . . 8
⊢ (𝑥 ⊆ {∅} → (¬
∅ ∈ 𝑥 →
𝑥 =
∅)) |
14 | | noel 3398 |
. . . . . . . . 9
⊢ ¬
∅ ∈ ∅ |
15 | | eleq2 2221 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (∅
∈ 𝑥 ↔ ∅
∈ ∅)) |
16 | 14, 15 | mtbiri 665 |
. . . . . . . 8
⊢ (𝑥 = ∅ → ¬ ∅
∈ 𝑥) |
17 | 13, 16 | impbid1 141 |
. . . . . . 7
⊢ (𝑥 ⊆ {∅} → (¬
∅ ∈ 𝑥 ↔
𝑥 =
∅)) |
18 | | ss1o0el1 4158 |
. . . . . . 7
⊢ (𝑥 ⊆ {∅} →
(∅ ∈ 𝑥 ↔
𝑥 =
{∅})) |
19 | 17, 18 | orbi12d 783 |
. . . . . 6
⊢ (𝑥 ⊆ {∅} →
((¬ ∅ ∈ 𝑥
∨ ∅ ∈ 𝑥)
↔ (𝑥 = ∅ ∨
𝑥 =
{∅}))) |
20 | 3, 19 | syl5bb 191 |
. . . . 5
⊢ (𝑥 ⊆ {∅} →
((∅ ∈ 𝑥 ∨
¬ ∅ ∈ 𝑥)
↔ (𝑥 = ∅ ∨
𝑥 =
{∅}))) |
21 | 2, 20 | syl5bb 191 |
. . . 4
⊢ (𝑥 ⊆ {∅} →
(DECID ∅ ∈ 𝑥 ↔ (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
22 | 21 | pm5.74i 179 |
. . 3
⊢ ((𝑥 ⊆ {∅} →
DECID ∅ ∈ 𝑥) ↔ (𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
23 | 22 | albii 1450 |
. 2
⊢
(∀𝑥(𝑥 ⊆ {∅} →
DECID ∅ ∈ 𝑥) ↔ ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
24 | 1, 23 | bitri 183 |
1
⊢
(EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |