Proof of Theorem kmlem11
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | kmlem9.1 | . . . . . 6
⊢ 𝐴 = {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))} | 
| 2 | 1 | unieqi 4918 | . . . . 5
⊢ ∪ 𝐴 =
∪ {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))} | 
| 3 |  | vex 3483 | . . . . . . 7
⊢ 𝑡 ∈ V | 
| 4 | 3 | difexi 5329 | . . . . . 6
⊢ (𝑡 ∖ ∪ (𝑥
∖ {𝑡})) ∈
V | 
| 5 | 4 | dfiun2 5032 | . . . . 5
⊢ ∪ 𝑡 ∈ 𝑥 (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = ∪ {𝑢 ∣ ∃𝑡 ∈ 𝑥 𝑢 = (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))} | 
| 6 | 2, 5 | eqtr4i 2767 | . . . 4
⊢ ∪ 𝐴 =
∪ 𝑡 ∈ 𝑥 (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) | 
| 7 | 6 | ineq2i 4216 | . . 3
⊢ (𝑧 ∩ ∪ 𝐴) =
(𝑧 ∩ ∪ 𝑡 ∈ 𝑥 (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) | 
| 8 |  | iunin2 5070 | . . 3
⊢ ∪ 𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (𝑧 ∩ ∪
𝑡 ∈ 𝑥 (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) | 
| 9 | 7, 8 | eqtr4i 2767 | . 2
⊢ (𝑧 ∩ ∪ 𝐴) =
∪ 𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) | 
| 10 |  | undif2 4476 | . . . . . 6
⊢ ({𝑧} ∪ (𝑥 ∖ {𝑧})) = ({𝑧} ∪ 𝑥) | 
| 11 |  | snssi 4807 | . . . . . . 7
⊢ (𝑧 ∈ 𝑥 → {𝑧} ⊆ 𝑥) | 
| 12 |  | ssequn1 4185 | . . . . . . 7
⊢ ({𝑧} ⊆ 𝑥 ↔ ({𝑧} ∪ 𝑥) = 𝑥) | 
| 13 | 11, 12 | sylib 218 | . . . . . 6
⊢ (𝑧 ∈ 𝑥 → ({𝑧} ∪ 𝑥) = 𝑥) | 
| 14 | 10, 13 | eqtr2id 2789 | . . . . 5
⊢ (𝑧 ∈ 𝑥 → 𝑥 = ({𝑧} ∪ (𝑥 ∖ {𝑧}))) | 
| 15 | 14 | iuneq1d 5018 | . . . 4
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∪
𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) | 
| 16 |  | iunxun 5093 | . . . . . 6
⊢ ∪ 𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (∪
𝑡 ∈ {𝑧} (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) | 
| 17 |  | vex 3483 | . . . . . . . 8
⊢ 𝑧 ∈ V | 
| 18 |  | difeq1 4118 | . . . . . . . . . 10
⊢ (𝑡 = 𝑧 → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑡}))) | 
| 19 |  | sneq 4635 | . . . . . . . . . . . . 13
⊢ (𝑡 = 𝑧 → {𝑡} = {𝑧}) | 
| 20 | 19 | difeq2d 4125 | . . . . . . . . . . . 12
⊢ (𝑡 = 𝑧 → (𝑥 ∖ {𝑡}) = (𝑥 ∖ {𝑧})) | 
| 21 | 20 | unieqd 4919 | . . . . . . . . . . 11
⊢ (𝑡 = 𝑧 → ∪ (𝑥 ∖ {𝑡}) = ∪ (𝑥 ∖ {𝑧})) | 
| 22 | 21 | difeq2d 4125 | . . . . . . . . . 10
⊢ (𝑡 = 𝑧 → (𝑧 ∖ ∪ (𝑥 ∖ {𝑡})) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) | 
| 23 | 18, 22 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝑡 = 𝑧 → (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) | 
| 24 | 23 | ineq2d 4219 | . . . . . . . 8
⊢ (𝑡 = 𝑧 → (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})))) | 
| 25 | 17, 24 | iunxsn 5090 | . . . . . . 7
⊢ ∪ 𝑡 ∈ {𝑧} (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) | 
| 26 | 25 | uneq1i 4163 | . . . . . 6
⊢ (∪ 𝑡 ∈ {𝑧} (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) | 
| 27 | 16, 26 | eqtri 2764 | . . . . 5
⊢ ∪ 𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) | 
| 28 |  | eldifsni 4789 | . . . . . . . . . 10
⊢ (𝑡 ∈ (𝑥 ∖ {𝑧}) → 𝑡 ≠ 𝑧) | 
| 29 |  | incom 4208 | . . . . . . . . . . . 12
⊢ (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ 𝑧) | 
| 30 |  | kmlem4 10195 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑡 ≠ 𝑧) → ((𝑡 ∖ ∪ (𝑥 ∖ {𝑡})) ∩ 𝑧) = ∅) | 
| 31 | 29, 30 | eqtrid 2788 | . . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑡 ≠ 𝑧) → (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅) | 
| 32 | 31 | ex 412 | . . . . . . . . . 10
⊢ (𝑧 ∈ 𝑥 → (𝑡 ≠ 𝑧 → (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅)) | 
| 33 | 28, 32 | syl5 34 | . . . . . . . . 9
⊢ (𝑧 ∈ 𝑥 → (𝑡 ∈ (𝑥 ∖ {𝑧}) → (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅)) | 
| 34 | 33 | ralrimiv 3144 | . . . . . . . 8
⊢ (𝑧 ∈ 𝑥 → ∀𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅) | 
| 35 |  | iuneq2 5010 | . . . . . . . 8
⊢
(∀𝑡 ∈
(𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅ → ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∪
𝑡 ∈ (𝑥 ∖ {𝑧})∅) | 
| 36 | 34, 35 | syl 17 | . . . . . . 7
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∪
𝑡 ∈ (𝑥 ∖ {𝑧})∅) | 
| 37 |  | iun0 5061 | . . . . . . 7
⊢ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})∅ = ∅ | 
| 38 | 36, 37 | eqtrdi 2792 | . . . . . 6
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ∅) | 
| 39 | 38 | uneq2d 4167 | . . . . 5
⊢ (𝑧 ∈ 𝑥 → ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∪ 𝑡 ∈ (𝑥 ∖ {𝑧})(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡})))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅)) | 
| 40 | 27, 39 | eqtrid 2788 | . . . 4
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ ({𝑧} ∪ (𝑥 ∖ {𝑧}))(𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅)) | 
| 41 | 15, 40 | eqtrd 2776 | . . 3
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅)) | 
| 42 |  | un0 4393 | . . . 4
⊢ ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅) = (𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) | 
| 43 |  | indif 4279 | . . . 4
⊢ (𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) | 
| 44 | 42, 43 | eqtri 2764 | . . 3
⊢ ((𝑧 ∩ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) ∪ ∅) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) | 
| 45 | 41, 44 | eqtrdi 2792 | . 2
⊢ (𝑧 ∈ 𝑥 → ∪
𝑡 ∈ 𝑥 (𝑧 ∩ (𝑡 ∖ ∪ (𝑥 ∖ {𝑡}))) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) | 
| 46 | 9, 45 | eqtrid 2788 | 1
⊢ (𝑧 ∈ 𝑥 → (𝑧 ∩ ∪ 𝐴) = (𝑧 ∖ ∪ (𝑥 ∖ {𝑧}))) |