Proof of Theorem kmlem11
Step | Hyp | Ref
| Expression |
1 | | kmlem9.1 |
. . . . . 6
⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))} |
2 | 1 | unieqi 4851 |
. . . . 5
⊢ ∪ 𝐴 =
∪ {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))} |
3 | | vex 3497 |
. . . . . . 7
⊢ 𝑡 ∈ V |
4 | 3 | difexi 5232 |
. . . . . 6
⊢ (𝑡 ∖ ∪ (𝑥
∖ {𝑡})) ∈
V |
5 | 4 | dfiun2 4958 |
. . . . 5
⊢ ∪ 𝑡 ∈ 𝑥 (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = ∪ {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))} |
6 | 2, 5 | eqtr4i 2847 |
. . . 4
⊢ ∪ 𝐴 =
∪ 𝑡 ∈ 𝑥 (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) |
7 | 6 | ineq2i 4186 |
. . 3
⊢ (𝑧 ∩ ∪ 𝐴) =
(𝑧 ∩ ∪ 𝑡 ∈ 𝑥 (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) |
8 | | iunin2 4993 |
. . 3
⊢ ∪ 𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (𝑧 ∩ ∪
𝑡 ∈ 𝑥 (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) |
9 | 7, 8 | eqtr4i 2847 |
. 2
⊢ (𝑧 ∩ ∪ 𝐴) =
∪ 𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) |
10 | | undif2 4425 |
. . . . . 6
⊢ ({𝑧} ∪ (𝑥 ∖ {𝑧})) = ({𝑧} ∪ 𝑥) |
11 | | snssi 4741 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑥 → {𝑧} ⊆ 𝑥) |
12 | | ssequn1 4156 |
. . . . . . 7
⊢ ({𝑧} ⊆ 𝑥 ↔ ({𝑧} ∪ 𝑥) = 𝑥) |
13 | 11, 12 | sylib 220 |
. . . . . 6
⊢ (𝑧 ∈ 𝑥 → ({𝑧} ∪ 𝑥) = 𝑥) |
14 | 10, 13 | syl5req 2869 |
. . . . 5
⊢ (𝑧 ∈ 𝑥 → 𝑥 = ({𝑧} ∪ (𝑥 ∖ {𝑧}))) |
15 | 14 | iuneq1d 4946 |
. . . 4
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∪
𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) |
16 | | iunxun 5016 |
. . . . . 6
⊢ ∪ 𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (∪
𝑡 ∈ {𝑧} (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) |
17 | | vex 3497 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
18 | | difeq1 4092 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑧 → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑡}))) |
19 | | sneq 4577 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑧 → {𝑡} = {𝑧}) |
20 | 19 | difeq2d 4099 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑧 → (𝑥 ∖ {𝑡}) = (𝑥 ∖ {𝑧})) |
21 | 20 | unieqd 4852 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑧 → ∪ (𝑥 ∖ {𝑡}) = ∪ (𝑥 ∖ {𝑧})) |
22 | 21 | difeq2d 4099 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑧 → (𝑧 ∖ ∪ (𝑥 ∖ {𝑡})) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) |
23 | 18, 22 | eqtrd 2856 |
. . . . . . . . 9
⊢ (𝑡 = 𝑧 → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) |
24 | 23 | ineq2d 4189 |
. . . . . . . 8
⊢ (𝑡 = 𝑧 → (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})))) |
25 | 17, 24 | iunxsn 5013 |
. . . . . . 7
⊢ ∪ 𝑡 ∈ {𝑧} (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) |
26 | 25 | uneq1i 4135 |
. . . . . 6
⊢ (∪ 𝑡 ∈ {𝑧} (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) |
27 | 16, 26 | eqtri 2844 |
. . . . 5
⊢ ∪ 𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) |
28 | | eldifsni 4722 |
. . . . . . . . . 10
⊢ (𝑡 ∈ (𝑥 ∖ {𝑧}) → 𝑡 ≠ 𝑧) |
29 | | incom 4178 |
. . . . . . . . . . . 12
⊢ (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ 𝑧) |
30 | | kmlem4 9579 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑡 ≠ 𝑧) → ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ 𝑧) = ∅) |
31 | 29, 30 | syl5eq 2868 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑡 ≠ 𝑧) → (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅) |
32 | 31 | ex 415 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑥 → (𝑡 ≠ 𝑧 → (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅)) |
33 | 28, 32 | syl5 34 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑥 → (𝑡 ∈ (𝑥 ∖ {𝑧}) → (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅)) |
34 | 33 | ralrimiv 3181 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑥 → ∀𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅) |
35 | | iuneq2 4938 |
. . . . . . . 8
⊢
(∀𝑡 ∈
(𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅ → ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∪
𝑡 ∈ (𝑥 ∖ {𝑧})∅) |
36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∪
𝑡 ∈ (𝑥 ∖ {𝑧})∅) |
37 | | iun0 4985 |
. . . . . . 7
⊢ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})∅ = ∅ |
38 | 36, 37 | syl6eq 2872 |
. . . . . 6
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅) |
39 | 38 | uneq2d 4139 |
. . . . 5
⊢ (𝑧 ∈ 𝑥 → ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅)) |
40 | 27, 39 | syl5eq 2868 |
. . . 4
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅)) |
41 | 15, 40 | eqtrd 2856 |
. . 3
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅)) |
42 | | un0 4344 |
. . . 4
⊢ ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅) = (𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) |
43 | | indif 4246 |
. . . 4
⊢ (𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) |
44 | 42, 43 | eqtri 2844 |
. . 3
⊢ ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) |
45 | 41, 44 | syl6eq 2872 |
. 2
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) |
46 | 9, 45 | syl5eq 2868 |
1
⊢ (𝑧 ∈ 𝑥 → (𝑧 ∩ ∪ 𝐴) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) |