Step | Hyp | Ref
| Expression |
1 | | df-exmid 4181 |
. 2
⊢
(EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} →
DECID ∅ ∈ 𝑥)) |
2 | | df-dc 830 |
. . . . 5
⊢
(DECID ∅ ∈ 𝑥 ↔ (∅ ∈ 𝑥 ∨ ¬ ∅ ∈ 𝑥)) |
3 | | orcom 723 |
. . . . . 6
⊢ ((∅
∈ 𝑥 ∨ ¬ ∅
∈ 𝑥) ↔ (¬
∅ ∈ 𝑥 ∨
∅ ∈ 𝑥)) |
4 | | simpll 524 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → 𝑥 ⊆ {∅}) |
5 | | simpr 109 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
6 | 4, 5 | sseldd 3148 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → 𝑦 ∈ {∅}) |
7 | | velsn 3600 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ {∅} ↔ 𝑦 = ∅) |
8 | 6, 7 | sylib 121 |
. . . . . . . . . . . 12
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → 𝑦 = ∅) |
9 | 8, 5 | eqeltrrd 2248 |
. . . . . . . . . . 11
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → ∅ ∈ 𝑥) |
10 | | simplr 525 |
. . . . . . . . . . 11
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → ¬ ∅ ∈ 𝑥) |
11 | 9, 10 | pm2.65da 656 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) →
¬ 𝑦 ∈ 𝑥) |
12 | 11 | eq0rdv 3459 |
. . . . . . . . 9
⊢ ((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) →
𝑥 =
∅) |
13 | 12 | ex 114 |
. . . . . . . 8
⊢ (𝑥 ⊆ {∅} → (¬
∅ ∈ 𝑥 →
𝑥 =
∅)) |
14 | | noel 3418 |
. . . . . . . . 9
⊢ ¬
∅ ∈ ∅ |
15 | | eleq2 2234 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (∅
∈ 𝑥 ↔ ∅
∈ ∅)) |
16 | 14, 15 | mtbiri 670 |
. . . . . . . 8
⊢ (𝑥 = ∅ → ¬ ∅
∈ 𝑥) |
17 | 13, 16 | impbid1 141 |
. . . . . . 7
⊢ (𝑥 ⊆ {∅} → (¬
∅ ∈ 𝑥 ↔
𝑥 =
∅)) |
18 | | ss1o0el1 4183 |
. . . . . . 7
⊢ (𝑥 ⊆ {∅} →
(∅ ∈ 𝑥 ↔
𝑥 =
{∅})) |
19 | 17, 18 | orbi12d 788 |
. . . . . 6
⊢ (𝑥 ⊆ {∅} →
((¬ ∅ ∈ 𝑥
∨ ∅ ∈ 𝑥)
↔ (𝑥 = ∅ ∨
𝑥 =
{∅}))) |
20 | 3, 19 | syl5bb 191 |
. . . . 5
⊢ (𝑥 ⊆ {∅} →
((∅ ∈ 𝑥 ∨
¬ ∅ ∈ 𝑥)
↔ (𝑥 = ∅ ∨
𝑥 =
{∅}))) |
21 | 2, 20 | syl5bb 191 |
. . . 4
⊢ (𝑥 ⊆ {∅} →
(DECID ∅ ∈ 𝑥 ↔ (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
22 | 21 | pm5.74i 179 |
. . 3
⊢ ((𝑥 ⊆ {∅} →
DECID ∅ ∈ 𝑥) ↔ (𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
23 | 22 | albii 1463 |
. 2
⊢
(∀𝑥(𝑥 ⊆ {∅} →
DECID ∅ ∈ 𝑥) ↔ ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
24 | 1, 23 | bitri 183 |
1
⊢
(EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |