| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fal 1553 | . . . . . . 7
⊢  ¬
⊥ | 
| 2 |  | pm5.501 366 | . . . . . . . 8
⊢ (⊤
→ (⊥ ↔ (⊤ ↔ ⊥))) | 
| 3 | 2 | mptru 1546 | . . . . . . 7
⊢ (⊥
↔ (⊤ ↔ ⊥)) | 
| 4 | 1, 3 | mtbi 322 | . . . . . 6
⊢  ¬
(⊤ ↔ ⊥) | 
| 5 | 4 | exgen 1973 | . . . . 5
⊢
∃𝑦 ¬
(⊤ ↔ ⊥) | 
| 6 |  | exnal 1826 | . . . . 5
⊢
(∃𝑦 ¬
(⊤ ↔ ⊥) ↔ ¬ ∀𝑦(⊤ ↔ ⊥)) | 
| 7 | 5, 6 | mpbi 230 | . . . 4
⊢  ¬
∀𝑦(⊤ ↔
⊥) | 
| 8 |  | df-clab 2714 | . . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∣ ⊤} ↔ [𝑦 / 𝑥]⊤) | 
| 9 |  | sbv 2087 | . . . . . . 7
⊢ ([𝑦 / 𝑥]⊤ ↔ ⊤) | 
| 10 | 8, 9 | bitr2i 276 | . . . . . 6
⊢ (⊤
↔ 𝑦 ∈ {𝑥 ∣
⊤}) | 
| 11 |  | df-clab 2714 | . . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∣ ⊥} ↔ [𝑦 / 𝑥]⊥) | 
| 12 |  | sbv 2087 | . . . . . . 7
⊢ ([𝑦 / 𝑥]⊥ ↔ ⊥) | 
| 13 | 11, 12 | bitr2i 276 | . . . . . 6
⊢ (⊥
↔ 𝑦 ∈ {𝑥 ∣
⊥}) | 
| 14 | 10, 13 | bibi12i 339 | . . . . 5
⊢
((⊤ ↔ ⊥) ↔ (𝑦 ∈ {𝑥 ∣ ⊤} ↔ 𝑦 ∈ {𝑥 ∣ ⊥})) | 
| 15 | 14 | albii 1818 | . . . 4
⊢
(∀𝑦(⊤
↔ ⊥) ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ ⊤} ↔ 𝑦 ∈ {𝑥 ∣ ⊥})) | 
| 16 | 7, 15 | mtbi 322 | . . 3
⊢  ¬
∀𝑦(𝑦 ∈ {𝑥 ∣ ⊤} ↔ 𝑦 ∈ {𝑥 ∣ ⊥}) | 
| 17 |  | dfcleq 2729 | . . . 4
⊢ ({𝑥 ∣ ⊤} = {𝑥 ∣ ⊥} ↔
∀𝑦(𝑦 ∈ {𝑥 ∣ ⊤} ↔ 𝑦 ∈ {𝑥 ∣ ⊥})) | 
| 18 |  | dfv2 3482 | . . . . . 6
⊢ V =
{𝑥 ∣
⊤} | 
| 19 | 18 | eqcomi 2745 | . . . . 5
⊢ {𝑥 ∣ ⊤} =
V | 
| 20 |  | dfnul4 4334 | . . . . . 6
⊢ ∅ =
{𝑥 ∣
⊥} | 
| 21 | 20 | eqcomi 2745 | . . . . 5
⊢ {𝑥 ∣ ⊥} =
∅ | 
| 22 | 19, 21 | eqeq12i 2754 | . . . 4
⊢ ({𝑥 ∣ ⊤} = {𝑥 ∣ ⊥} ↔ V =
∅) | 
| 23 | 17, 22 | bitr3i 277 | . . 3
⊢
(∀𝑦(𝑦 ∈ {𝑥 ∣ ⊤} ↔ 𝑦 ∈ {𝑥 ∣ ⊥}) ↔ V =
∅) | 
| 24 | 16, 23 | mtbi 322 | . 2
⊢  ¬ V
= ∅ | 
| 25 | 24 | neir 2942 | 1
⊢ V ≠
∅ |