Proof of Theorem kmlem11
Step | Hyp | Ref
| Expression |
1 | | kmlem9.1 |
. . . . . 6
⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))} |
2 | 1 | unieqi 4381 |
. . . . 5
⊢ ∪ 𝐴 =
∪ {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))} |
3 | | vex 3176 |
. . . . . . 7
⊢ 𝑡 ∈ V |
4 | | difexg 4735 |
. . . . . . 7
⊢ (𝑡 ∈ V → (𝑡 ∖ ∪ (𝑥
∖ {𝑡})) ∈
V) |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
⊢ (𝑡 ∖ ∪ (𝑥
∖ {𝑡})) ∈
V |
6 | 5 | dfiun2 4490 |
. . . . 5
⊢ ∪ 𝑡 ∈ 𝑥 (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = ∪ {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))} |
7 | 2, 6 | eqtr4i 2635 |
. . . 4
⊢ ∪ 𝐴 =
∪ 𝑡 ∈ 𝑥 (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) |
8 | 7 | ineq2i 3773 |
. . 3
⊢ (𝑧 ∩ ∪ 𝐴) =
(𝑧 ∩ ∪ 𝑡 ∈ 𝑥 (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) |
9 | | iunin2 4520 |
. . 3
⊢ ∪ 𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (𝑧 ∩ ∪
𝑡 ∈ 𝑥 (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) |
10 | 8, 9 | eqtr4i 2635 |
. 2
⊢ (𝑧 ∩ ∪ 𝐴) =
∪ 𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) |
11 | | undif2 3996 |
. . . . . 6
⊢ ({𝑧} ∪ (𝑥 ∖ {𝑧})) = ({𝑧} ∪ 𝑥) |
12 | | snssi 4280 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑥 → {𝑧} ⊆ 𝑥) |
13 | | ssequn1 3745 |
. . . . . . 7
⊢ ({𝑧} ⊆ 𝑥 ↔ ({𝑧} ∪ 𝑥) = 𝑥) |
14 | 12, 13 | sylib 207 |
. . . . . 6
⊢ (𝑧 ∈ 𝑥 → ({𝑧} ∪ 𝑥) = 𝑥) |
15 | 11, 14 | syl5req 2657 |
. . . . 5
⊢ (𝑧 ∈ 𝑥 → 𝑥 = ({𝑧} ∪ (𝑥 ∖ {𝑧}))) |
16 | 15 | iuneq1d 4481 |
. . . 4
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∪
𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) |
17 | | iunxun 4541 |
. . . . . 6
⊢ ∪ 𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (∪
𝑡 ∈ {𝑧} (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) |
18 | | vex 3176 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
19 | | difeq1 3683 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑧 → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑡}))) |
20 | | sneq 4135 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑧 → {𝑡} = {𝑧}) |
21 | 20 | difeq2d 3690 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑧 → (𝑥 ∖ {𝑡}) = (𝑥 ∖ {𝑧})) |
22 | 21 | unieqd 4382 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑧 → ∪ (𝑥 ∖ {𝑡}) = ∪ (𝑥 ∖ {𝑧})) |
23 | 22 | difeq2d 3690 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑧 → (𝑧 ∖ ∪ (𝑥 ∖ {𝑡})) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) |
24 | 19, 23 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝑡 = 𝑧 → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) |
25 | 24 | ineq2d 3776 |
. . . . . . . 8
⊢ (𝑡 = 𝑧 → (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})))) |
26 | 18, 25 | iunxsn 4539 |
. . . . . . 7
⊢ ∪ 𝑡 ∈ {𝑧} (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) |
27 | 26 | uneq1i 3725 |
. . . . . 6
⊢ (∪ 𝑡 ∈ {𝑧} (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) |
28 | 17, 27 | eqtri 2632 |
. . . . 5
⊢ ∪ 𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) |
29 | | eldifsni 4261 |
. . . . . . . . . 10
⊢ (𝑡 ∈ (𝑥 ∖ {𝑧}) → 𝑡 ≠ 𝑧) |
30 | | incom 3767 |
. . . . . . . . . . . 12
⊢ (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ 𝑧) |
31 | | kmlem4 8858 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑡 ≠ 𝑧) → ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ 𝑧) = ∅) |
32 | 30, 31 | syl5eq 2656 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑡 ≠ 𝑧) → (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅) |
33 | 32 | ex 449 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑥 → (𝑡 ≠ 𝑧 → (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅)) |
34 | 29, 33 | syl5 33 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑥 → (𝑡 ∈ (𝑥 ∖ {𝑧}) → (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅)) |
35 | 34 | ralrimiv 2948 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑥 → ∀𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅) |
36 | | iuneq2 4473 |
. . . . . . . 8
⊢
(∀𝑡 ∈
(𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅ → ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∪
𝑡 ∈ (𝑥 ∖ {𝑧})∅) |
37 | 35, 36 | syl 17 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∪
𝑡 ∈ (𝑥 ∖ {𝑧})∅) |
38 | | iun0 4512 |
. . . . . . 7
⊢ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})∅ = ∅ |
39 | 37, 38 | syl6eq 2660 |
. . . . . 6
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅) |
40 | 39 | uneq2d 3729 |
. . . . 5
⊢ (𝑧 ∈ 𝑥 → ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅)) |
41 | 28, 40 | syl5eq 2656 |
. . . 4
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅)) |
42 | 16, 41 | eqtrd 2644 |
. . 3
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅)) |
43 | | un0 3919 |
. . . 4
⊢ ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅) = (𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) |
44 | | indif 3828 |
. . . 4
⊢ (𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) |
45 | 43, 44 | eqtri 2632 |
. . 3
⊢ ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) |
46 | 42, 45 | syl6eq 2660 |
. 2
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) |
47 | 10, 46 | syl5eq 2656 |
1
⊢ (𝑧 ∈ 𝑥 → (𝑧 ∩ ∪ 𝐴) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) |