Proof of Theorem kmlem3
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dfdif2 3960 | . . . 4
⊢ (𝑧 ∖ ∪ (𝑥
∖ {𝑧})) = {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} | 
| 2 |  | dfnul3 4337 | . . . . . 6
⊢ ∅ =
{𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧} | 
| 3 | 2 | uneq2i 4165 | . . . . 5
⊢ ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ ∅) = ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧}) | 
| 4 |  | un0 4394 | . . . . 5
⊢ ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ ∅) = {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} | 
| 5 |  | unrab 4315 | . . . . 5
⊢ ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧}) = {𝑣 ∈ 𝑧 ∣ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)} | 
| 6 | 3, 4, 5 | 3eqtr3i 2773 | . . . 4
⊢ {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} = {𝑣 ∈ 𝑧 ∣ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)} | 
| 7 |  | ianor 984 | . . . . . 6
⊢ (¬
(𝑣 ∈ ∪ (𝑥
∖ {𝑧}) ∧ 𝑣 ∈ 𝑧) ↔ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)) | 
| 8 |  | eluni 4910 | . . . . . . . . 9
⊢ (𝑣 ∈ ∪ (𝑥
∖ {𝑧}) ↔
∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧}))) | 
| 9 | 8 | anbi1i 624 | . . . . . . . 8
⊢ ((𝑣 ∈ ∪ (𝑥
∖ {𝑧}) ∧ 𝑣 ∈ 𝑧) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧)) | 
| 10 |  | df-rex 3071 | . . . . . . . . 9
⊢
(∃𝑤 ∈
𝑥 ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))) | 
| 11 |  | elin 3967 | . . . . . . . . . . . . . 14
⊢ (𝑣 ∈ (𝑧 ∩ 𝑤) ↔ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)) | 
| 12 | 11 | anbi2i 623 | . . . . . . . . . . . . 13
⊢ ((𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))) | 
| 13 |  | df-an 396 | . . . . . . . . . . . . 13
⊢ ((𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) | 
| 14 | 12, 13 | bitr3i 277 | . . . . . . . . . . . 12
⊢ ((𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)) ↔ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) | 
| 15 | 14 | anbi2i 623 | . . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))) ↔ (𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))) | 
| 16 |  | eldifsn 4786 | . . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤 ∈ 𝑥 ∧ 𝑤 ≠ 𝑧)) | 
| 17 |  | necom 2994 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 ≠ 𝑧 ↔ 𝑧 ≠ 𝑤) | 
| 18 | 17 | anbi2i 623 | . . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑤 ≠ 𝑧) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤)) | 
| 19 | 16, 18 | bitri 275 | . . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤)) | 
| 20 | 19 | anbi2i 623 | . . . . . . . . . . . . 13
⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤))) | 
| 21 |  | ancom 460 | . . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ↔ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)) | 
| 22 | 21 | anbi2ci 625 | . . . . . . . . . . . . 13
⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤)) ↔ ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))) | 
| 23 |  | anass 468 | . . . . . . . . . . . . 13
⊢ (((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)) ↔ (𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)))) | 
| 24 | 20, 22, 23 | 3bitri 297 | . . . . . . . . . . . 12
⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ (𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)))) | 
| 25 |  | an32 646 | . . . . . . . . . . . 12
⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧)) | 
| 26 | 24, 25 | bitr3i 277 | . . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧)) | 
| 27 | 15, 26 | bitr3i 277 | . . . . . . . . . 10
⊢ ((𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧)) | 
| 28 | 27 | exbii 1848 | . . . . . . . . 9
⊢
(∃𝑤(𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) ↔ ∃𝑤((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧)) | 
| 29 |  | 19.41v 1949 | . . . . . . . . 9
⊢
(∃𝑤((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧)) | 
| 30 | 10, 28, 29 | 3bitri 297 | . . . . . . . 8
⊢
(∃𝑤 ∈
𝑥 ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧)) | 
| 31 |  | rexnal 3100 | . . . . . . . 8
⊢
(∃𝑤 ∈
𝑥 ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ¬ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) | 
| 32 | 9, 30, 31 | 3bitr2ri 300 | . . . . . . 7
⊢ (¬
∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∧ 𝑣 ∈ 𝑧)) | 
| 33 | 32 | con1bii 356 | . . . . . 6
⊢ (¬
(𝑣 ∈ ∪ (𝑥
∖ {𝑧}) ∧ 𝑣 ∈ 𝑧) ↔ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) | 
| 34 | 7, 33 | bitr3i 277 | . . . . 5
⊢ ((¬
𝑣 ∈ ∪ (𝑥
∖ {𝑧}) ∨ ¬
𝑣 ∈ 𝑧) ↔ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) | 
| 35 | 34 | rabbii 3442 | . . . 4
⊢ {𝑣 ∈ 𝑧 ∣ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)} = {𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))} | 
| 36 | 1, 6, 35 | 3eqtri 2769 | . . 3
⊢ (𝑧 ∖ ∪ (𝑥
∖ {𝑧})) = {𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))} | 
| 37 | 36 | neeq1i 3005 | . 2
⊢ ((𝑧 ∖ ∪ (𝑥
∖ {𝑧})) ≠ ∅
↔ {𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))} ≠ ∅) | 
| 38 |  | rabn0 4389 | . 2
⊢ ({𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))} ≠ ∅ ↔ ∃𝑣 ∈ 𝑧 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) | 
| 39 | 37, 38 | bitri 275 | 1
⊢ ((𝑧 ∖ ∪ (𝑥
∖ {𝑧})) ≠ ∅
↔ ∃𝑣 ∈
𝑧 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) |