Step | Hyp | Ref
| Expression |
1 | | eldif 3550 |
. . . . 5
⊢ (𝑦 ∈ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ↔ (𝑦 ∈ 𝑧 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∖ {𝑧}))) |
2 | | simpr 476 |
. . . . . 6
⊢ ((𝑦 ∈ 𝑧 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∖ {𝑧})) → ¬ 𝑦 ∈ ∪ (𝑥 ∖ {𝑧})) |
3 | | eluni 4375 |
. . . . . . . 8
⊢ (𝑦 ∈ ∪ (𝑥
∖ {𝑧}) ↔
∃𝑣(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ (𝑥 ∖ {𝑧}))) |
4 | 3 | notbii 309 |
. . . . . . 7
⊢ (¬
𝑦 ∈ ∪ (𝑥
∖ {𝑧}) ↔ ¬
∃𝑣(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ (𝑥 ∖ {𝑧}))) |
5 | | alnex 1697 |
. . . . . . 7
⊢
(∀𝑣 ¬
(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ (𝑥 ∖ {𝑧})) ↔ ¬ ∃𝑣(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ (𝑥 ∖ {𝑧}))) |
6 | | con2b 348 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑣 → ¬ 𝑣 ∈ (𝑥 ∖ {𝑧})) ↔ (𝑣 ∈ (𝑥 ∖ {𝑧}) → ¬ 𝑦 ∈ 𝑣)) |
7 | | imnan 437 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑣 → ¬ 𝑣 ∈ (𝑥 ∖ {𝑧})) ↔ ¬ (𝑦 ∈ 𝑣 ∧ 𝑣 ∈ (𝑥 ∖ {𝑧}))) |
8 | | eldifsn 4260 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑣 ∈ 𝑥 ∧ 𝑣 ≠ 𝑧)) |
9 | | necom 2835 |
. . . . . . . . . . . 12
⊢ (𝑣 ≠ 𝑧 ↔ 𝑧 ≠ 𝑣) |
10 | 9 | anbi2i 726 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ 𝑥 ∧ 𝑣 ≠ 𝑧) ↔ (𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣)) |
11 | 8, 10 | bitri 263 |
. . . . . . . . . 10
⊢ (𝑣 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣)) |
12 | 11 | imbi1i 338 |
. . . . . . . . 9
⊢ ((𝑣 ∈ (𝑥 ∖ {𝑧}) → ¬ 𝑦 ∈ 𝑣) ↔ ((𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣) → ¬ 𝑦 ∈ 𝑣)) |
13 | 6, 7, 12 | 3bitr3i 289 |
. . . . . . . 8
⊢ (¬
(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣) → ¬ 𝑦 ∈ 𝑣)) |
14 | 13 | albii 1737 |
. . . . . . 7
⊢
(∀𝑣 ¬
(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ (𝑥 ∖ {𝑧})) ↔ ∀𝑣((𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣) → ¬ 𝑦 ∈ 𝑣)) |
15 | 4, 5, 14 | 3bitr2i 287 |
. . . . . 6
⊢ (¬
𝑦 ∈ ∪ (𝑥
∖ {𝑧}) ↔
∀𝑣((𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣) → ¬ 𝑦 ∈ 𝑣)) |
16 | 2, 15 | sylib 207 |
. . . . 5
⊢ ((𝑦 ∈ 𝑧 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∖ {𝑧})) → ∀𝑣((𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣) → ¬ 𝑦 ∈ 𝑣)) |
17 | 1, 16 | sylbi 206 |
. . . 4
⊢ (𝑦 ∈ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) → ∀𝑣((𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣) → ¬ 𝑦 ∈ 𝑣)) |
18 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑣 = 𝑤 → (𝑣 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥)) |
19 | | neeq2 2845 |
. . . . . . . 8
⊢ (𝑣 = 𝑤 → (𝑧 ≠ 𝑣 ↔ 𝑧 ≠ 𝑤)) |
20 | 18, 19 | anbi12d 743 |
. . . . . . 7
⊢ (𝑣 = 𝑤 → ((𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤))) |
21 | | eleq2 2677 |
. . . . . . . 8
⊢ (𝑣 = 𝑤 → (𝑦 ∈ 𝑣 ↔ 𝑦 ∈ 𝑤)) |
22 | 21 | notbid 307 |
. . . . . . 7
⊢ (𝑣 = 𝑤 → (¬ 𝑦 ∈ 𝑣 ↔ ¬ 𝑦 ∈ 𝑤)) |
23 | 20, 22 | imbi12d 333 |
. . . . . 6
⊢ (𝑣 = 𝑤 → (((𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣) → ¬ 𝑦 ∈ 𝑣) ↔ ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) → ¬ 𝑦 ∈ 𝑤))) |
24 | 23 | spv 2248 |
. . . . 5
⊢
(∀𝑣((𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣) → ¬ 𝑦 ∈ 𝑣) → ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) → ¬ 𝑦 ∈ 𝑤)) |
25 | 24 | com12 32 |
. . . 4
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) → (∀𝑣((𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣) → ¬ 𝑦 ∈ 𝑣) → ¬ 𝑦 ∈ 𝑤)) |
26 | 17, 25 | syl5 33 |
. . 3
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) → (𝑦 ∈ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) → ¬ 𝑦 ∈ 𝑤)) |
27 | 26 | ralrimiv 2948 |
. 2
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) → ∀𝑦 ∈ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ¬ 𝑦 ∈ 𝑤) |
28 | | disj 3969 |
. 2
⊢ (((𝑧 ∖ ∪ (𝑥
∖ {𝑧})) ∩ 𝑤) = ∅ ↔ ∀𝑦 ∈ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ¬ 𝑦 ∈ 𝑤) |
29 | 27, 28 | sylibr 223 |
1
⊢ ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) → ((𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ∩ 𝑤) = ∅) |