Proof of Theorem kmlem3
Step | Hyp | Ref
| Expression |
1 | | dfdif2 3850 |
. . . 4
⊢ (𝑧 ∖ ∪ (𝑥
∖ {𝑧})) = {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} |
2 | | dfnul3 4213 |
. . . . . 6
⊢ ∅ =
{𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧} |
3 | 2 | uneq2i 4048 |
. . . . 5
⊢ ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ ∅) = ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧}) |
4 | | un0 4276 |
. . . . 5
⊢ ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ ∅) = {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} |
5 | | unrab 4192 |
. . . . 5
⊢ ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧}) = {𝑣 ∈ 𝑧 ∣ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)} |
6 | 3, 4, 5 | 3eqtr3i 2769 |
. . . 4
⊢ {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} = {𝑣 ∈ 𝑧 ∣ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)} |
7 | | ianor 981 |
. . . . . 6
⊢ (¬
(𝑣 ∈ ∪ (𝑥
∖ {𝑧}) ∧ 𝑣 ∈ 𝑧) ↔ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)) |
8 | | eluni 4796 |
. . . . . . . . 9
⊢ (𝑣 ∈ ∪ (𝑥
∖ {𝑧}) ↔
∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧}))) |
9 | 8 | anbi1i 627 |
. . . . . . . 8
⊢ ((𝑣 ∈ ∪ (𝑥
∖ {𝑧}) ∧ 𝑣 ∈ 𝑧) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧)) |
10 | | df-rex 3059 |
. . . . . . . . 9
⊢
(∃𝑤 ∈
𝑥 ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))) |
11 | | elin 3857 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ (𝑧 ∩ 𝑤) ↔ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)) |
12 | 11 | anbi2i 626 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))) |
13 | | df-an 400 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) |
14 | 12, 13 | bitr3i 280 |
. . . . . . . . . . . 12
⊢ ((𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)) ↔ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) |
15 | 14 | anbi2i 626 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))) ↔ (𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))) |
16 | | eldifsn 4672 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤 ∈ 𝑥 ∧ 𝑤 ≠ 𝑧)) |
17 | | necom 2987 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ≠ 𝑧 ↔ 𝑧 ≠ 𝑤) |
18 | 17 | anbi2i 626 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑤 ≠ 𝑧) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤)) |
19 | 16, 18 | bitri 278 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤)) |
20 | 19 | anbi2i 626 |
. . . . . . . . . . . . 13
⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤))) |
21 | | ancom 464 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ↔ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)) |
22 | 21 | anbi2ci 628 |
. . . . . . . . . . . . 13
⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤)) ↔ ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))) |
23 | | anass 472 |
. . . . . . . . . . . . 13
⊢ (((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)) ↔ (𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)))) |
24 | 20, 22, 23 | 3bitri 300 |
. . . . . . . . . . . 12
⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ (𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)))) |
25 | | an32 646 |
. . . . . . . . . . . 12
⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧)) |
26 | 24, 25 | bitr3i 280 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧)) |
27 | 15, 26 | bitr3i 280 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧)) |
28 | 27 | exbii 1854 |
. . . . . . . . 9
⊢
(∃𝑤(𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) ↔ ∃𝑤((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧)) |
29 | | 19.41v 1956 |
. . . . . . . . 9
⊢
(∃𝑤((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧)) |
30 | 10, 28, 29 | 3bitri 300 |
. . . . . . . 8
⊢
(∃𝑤 ∈
𝑥 ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧)) |
31 | | rexnal 3150 |
. . . . . . . 8
⊢
(∃𝑤 ∈
𝑥 ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ¬ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) |
32 | 9, 30, 31 | 3bitr2ri 303 |
. . . . . . 7
⊢ (¬
∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∧ 𝑣 ∈ 𝑧)) |
33 | 32 | con1bii 360 |
. . . . . 6
⊢ (¬
(𝑣 ∈ ∪ (𝑥
∖ {𝑧}) ∧ 𝑣 ∈ 𝑧) ↔ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) |
34 | 7, 33 | bitr3i 280 |
. . . . 5
⊢ ((¬
𝑣 ∈ ∪ (𝑥
∖ {𝑧}) ∨ ¬
𝑣 ∈ 𝑧) ↔ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) |
35 | 34 | rabbii 3373 |
. . . 4
⊢ {𝑣 ∈ 𝑧 ∣ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)} = {𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))} |
36 | 1, 6, 35 | 3eqtri 2765 |
. . 3
⊢ (𝑧 ∖ ∪ (𝑥
∖ {𝑧})) = {𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))} |
37 | 36 | neeq1i 2998 |
. 2
⊢ ((𝑧 ∖ ∪ (𝑥
∖ {𝑧})) ≠ ∅
↔ {𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))} ≠ ∅) |
38 | | rabn0 4271 |
. 2
⊢ ({𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))} ≠ ∅ ↔ ∃𝑣 ∈ 𝑧 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) |
39 | 37, 38 | bitri 278 |
1
⊢ ((𝑧 ∖ ∪ (𝑥
∖ {𝑧})) ≠ ∅
↔ ∃𝑣 ∈
𝑧 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) |