Step | Hyp | Ref
| Expression |
1 | | df-exmid 4051 |
. 2
⊢
(EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} →
DECID ∅ ∈ 𝑥)) |
2 | | df-dc 784 |
. . . . 5
⊢
(DECID ∅ ∈ 𝑥 ↔ (∅ ∈ 𝑥 ∨ ¬ ∅ ∈ 𝑥)) |
3 | | orcom 685 |
. . . . . 6
⊢ ((∅
∈ 𝑥 ∨ ¬ ∅
∈ 𝑥) ↔ (¬
∅ ∈ 𝑥 ∨
∅ ∈ 𝑥)) |
4 | | simpll 497 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → 𝑥 ⊆ {∅}) |
5 | | simpr 109 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
6 | 4, 5 | sseldd 3040 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → 𝑦 ∈ {∅}) |
7 | | velsn 3483 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ {∅} ↔ 𝑦 = ∅) |
8 | 6, 7 | sylib 121 |
. . . . . . . . . . . 12
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → 𝑦 = ∅) |
9 | 8, 5 | eqeltrrd 2172 |
. . . . . . . . . . 11
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → ∅ ∈ 𝑥) |
10 | | simplr 498 |
. . . . . . . . . . 11
⊢ (((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) ∧
𝑦 ∈ 𝑥) → ¬ ∅ ∈ 𝑥) |
11 | 9, 10 | pm2.65da 625 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) →
¬ 𝑦 ∈ 𝑥) |
12 | 11 | eq0rdv 3346 |
. . . . . . . . 9
⊢ ((𝑥 ⊆ {∅} ∧ ¬
∅ ∈ 𝑥) →
𝑥 =
∅) |
13 | 12 | ex 114 |
. . . . . . . 8
⊢ (𝑥 ⊆ {∅} → (¬
∅ ∈ 𝑥 →
𝑥 =
∅)) |
14 | | noel 3306 |
. . . . . . . . 9
⊢ ¬
∅ ∈ ∅ |
15 | | eleq2 2158 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (∅
∈ 𝑥 ↔ ∅
∈ ∅)) |
16 | 14, 15 | mtbiri 638 |
. . . . . . . 8
⊢ (𝑥 = ∅ → ¬ ∅
∈ 𝑥) |
17 | 13, 16 | impbid1 141 |
. . . . . . 7
⊢ (𝑥 ⊆ {∅} → (¬
∅ ∈ 𝑥 ↔
𝑥 =
∅)) |
18 | | elex2 2649 |
. . . . . . . . . 10
⊢ (∅
∈ 𝑥 →
∃𝑧 𝑧 ∈ 𝑥) |
19 | | sssnm 3620 |
. . . . . . . . . 10
⊢
(∃𝑧 𝑧 ∈ 𝑥 → (𝑥 ⊆ {∅} ↔ 𝑥 = {∅})) |
20 | 18, 19 | syl 14 |
. . . . . . . . 9
⊢ (∅
∈ 𝑥 → (𝑥 ⊆ {∅} ↔ 𝑥 = {∅})) |
21 | 20 | biimpcd 158 |
. . . . . . . 8
⊢ (𝑥 ⊆ {∅} →
(∅ ∈ 𝑥 →
𝑥 =
{∅})) |
22 | | 0ex 3987 |
. . . . . . . . . 10
⊢ ∅
∈ V |
23 | 22 | snid 3495 |
. . . . . . . . 9
⊢ ∅
∈ {∅} |
24 | | eleq2 2158 |
. . . . . . . . 9
⊢ (𝑥 = {∅} → (∅
∈ 𝑥 ↔ ∅
∈ {∅})) |
25 | 23, 24 | mpbiri 167 |
. . . . . . . 8
⊢ (𝑥 = {∅} → ∅
∈ 𝑥) |
26 | 21, 25 | impbid1 141 |
. . . . . . 7
⊢ (𝑥 ⊆ {∅} →
(∅ ∈ 𝑥 ↔
𝑥 =
{∅})) |
27 | 17, 26 | orbi12d 745 |
. . . . . 6
⊢ (𝑥 ⊆ {∅} →
((¬ ∅ ∈ 𝑥
∨ ∅ ∈ 𝑥)
↔ (𝑥 = ∅ ∨
𝑥 =
{∅}))) |
28 | 3, 27 | syl5bb 191 |
. . . . 5
⊢ (𝑥 ⊆ {∅} →
((∅ ∈ 𝑥 ∨
¬ ∅ ∈ 𝑥)
↔ (𝑥 = ∅ ∨
𝑥 =
{∅}))) |
29 | 2, 28 | syl5bb 191 |
. . . 4
⊢ (𝑥 ⊆ {∅} →
(DECID ∅ ∈ 𝑥 ↔ (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
30 | 29 | pm5.74i 179 |
. . 3
⊢ ((𝑥 ⊆ {∅} →
DECID ∅ ∈ 𝑥) ↔ (𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
31 | 30 | albii 1411 |
. 2
⊢
(∀𝑥(𝑥 ⊆ {∅} →
DECID ∅ ∈ 𝑥) ↔ ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |
32 | 1, 31 | bitri 183 |
1
⊢
(EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅}))) |