Proof of Theorem istopclsd
| Step | Hyp | Ref
| Expression |
| 1 | | istopclsd.j |
. . . 4
⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧)} |
| 2 | | istopclsd.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵) |
| 3 | 2 | ffnd 6737 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn 𝒫 𝐵) |
| 4 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → 𝐹 Fn 𝒫 𝐵) |
| 5 | | difss 4136 |
. . . . . . . . 9
⊢ (𝐵 ∖ 𝑧) ⊆ 𝐵 |
| 6 | | istopclsd.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
| 7 | | elpw2g 5333 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑉 → ((𝐵 ∖ 𝑧) ∈ 𝒫 𝐵 ↔ (𝐵 ∖ 𝑧) ⊆ 𝐵)) |
| 8 | 6, 7 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 ∖ 𝑧) ∈ 𝒫 𝐵 ↔ (𝐵 ∖ 𝑧) ⊆ 𝐵)) |
| 9 | 5, 8 | mpbiri 258 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∖ 𝑧) ∈ 𝒫 𝐵) |
| 10 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑧) ∈ 𝒫 𝐵) |
| 11 | | fnelfp 7195 |
. . . . . . 7
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ (𝐵 ∖ 𝑧) ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧))) |
| 12 | 4, 10, 11 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧))) |
| 13 | 12 | bicomd 223 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → ((𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧) ↔ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I ))) |
| 14 | 13 | rabbidva 3443 |
. . . 4
⊢ (𝜑 → {𝑧 ∈ 𝒫 𝐵 ∣ (𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧)} = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )}) |
| 15 | 1, 14 | eqtrid 2789 |
. . 3
⊢ (𝜑 → 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )}) |
| 16 | | istopclsd.e |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) |
| 17 | | simp1 1137 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → 𝜑) |
| 18 | | simp2 1138 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → 𝑥 ⊆ 𝐵) |
| 19 | | simp3 1139 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → 𝑦 ⊆ 𝑥) |
| 20 | 19, 18 | sstrd 3994 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → 𝑦 ⊆ 𝐵) |
| 21 | | istopclsd.u |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵) → (𝐹‘(𝑥 ∪ 𝑦)) = ((𝐹‘𝑥) ∪ (𝐹‘𝑦))) |
| 22 | 17, 18, 20, 21 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘(𝑥 ∪ 𝑦)) = ((𝐹‘𝑥) ∪ (𝐹‘𝑦))) |
| 23 | | ssequn2 4189 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ 𝑥 ↔ (𝑥 ∪ 𝑦) = 𝑥) |
| 24 | 23 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ 𝑥 → (𝑥 ∪ 𝑦) = 𝑥) |
| 25 | 24 | 3ad2ant3 1136 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝑥 ∪ 𝑦) = 𝑥) |
| 26 | 25 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘(𝑥 ∪ 𝑦)) = (𝐹‘𝑥)) |
| 27 | 22, 26 | eqtr3d 2779 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → ((𝐹‘𝑥) ∪ (𝐹‘𝑦)) = (𝐹‘𝑥)) |
| 28 | | ssequn2 4189 |
. . . . . . 7
⊢ ((𝐹‘𝑦) ⊆ (𝐹‘𝑥) ↔ ((𝐹‘𝑥) ∪ (𝐹‘𝑦)) = (𝐹‘𝑥)) |
| 29 | 27, 28 | sylibr 234 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) |
| 30 | | istopclsd.i |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) |
| 31 | 6, 2, 16, 29, 30 | ismrcd1 42709 |
. . . . 5
⊢ (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵)) |
| 32 | | istopclsd.z |
. . . . . 6
⊢ (𝜑 → (𝐹‘∅) = ∅) |
| 33 | | 0elpw 5356 |
. . . . . . 7
⊢ ∅
∈ 𝒫 𝐵 |
| 34 | | fnelfp 7195 |
. . . . . . 7
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ ∅ ∈ 𝒫 𝐵) → (∅ ∈ dom
(𝐹 ∩ I ) ↔ (𝐹‘∅) =
∅)) |
| 35 | 3, 33, 34 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → (∅ ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘∅) =
∅)) |
| 36 | 32, 35 | mpbird 257 |
. . . . 5
⊢ (𝜑 → ∅ ∈ dom (𝐹 ∩ I )) |
| 37 | | simp1 1137 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → 𝜑) |
| 38 | | inss1 4237 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∩ I ) ⊆ 𝐹 |
| 39 | | dmss 5913 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∩ I ) ⊆ 𝐹 → dom (𝐹 ∩ I ) ⊆ dom 𝐹) |
| 40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ dom
(𝐹 ∩ I ) ⊆ dom
𝐹 |
| 41 | 40, 2 | fssdm 6755 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵) |
| 42 | 41 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵) |
| 43 | | simp2 1138 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → 𝑥 ∈ dom (𝐹 ∩ I )) |
| 44 | 42, 43 | sseldd 3984 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → 𝑥 ∈ 𝒫 𝐵) |
| 45 | 44 | elpwid 4609 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → 𝑥 ⊆ 𝐵) |
| 46 | | simp3 1139 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → 𝑦 ∈ dom (𝐹 ∩ I )) |
| 47 | 42, 46 | sseldd 3984 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → 𝑦 ∈ 𝒫 𝐵) |
| 48 | 47 | elpwid 4609 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → 𝑦 ⊆ 𝐵) |
| 49 | 37, 45, 48, 21 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝐹‘(𝑥 ∪ 𝑦)) = ((𝐹‘𝑥) ∪ (𝐹‘𝑦))) |
| 50 | 3 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → 𝐹 Fn 𝒫 𝐵) |
| 51 | | fnelfp 7195 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ 𝑥 ∈ 𝒫 𝐵) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑥) = 𝑥)) |
| 52 | 50, 44, 51 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑥) = 𝑥)) |
| 53 | 43, 52 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝐹‘𝑥) = 𝑥) |
| 54 | | fnelfp 7195 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ 𝑦 ∈ 𝒫 𝐵) → (𝑦 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑦) = 𝑦)) |
| 55 | 50, 47, 54 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝑦 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑦) = 𝑦)) |
| 56 | 46, 55 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝐹‘𝑦) = 𝑦) |
| 57 | 53, 56 | uneq12d 4169 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → ((𝐹‘𝑥) ∪ (𝐹‘𝑦)) = (𝑥 ∪ 𝑦)) |
| 58 | 49, 57 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝐹‘(𝑥 ∪ 𝑦)) = (𝑥 ∪ 𝑦)) |
| 59 | 45, 48 | unssd 4192 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝑥 ∪ 𝑦) ⊆ 𝐵) |
| 60 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 61 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
| 62 | 60, 61 | unex 7764 |
. . . . . . . . 9
⊢ (𝑥 ∪ 𝑦) ∈ V |
| 63 | 62 | elpw 4604 |
. . . . . . . 8
⊢ ((𝑥 ∪ 𝑦) ∈ 𝒫 𝐵 ↔ (𝑥 ∪ 𝑦) ⊆ 𝐵) |
| 64 | 59, 63 | sylibr 234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝑥 ∪ 𝑦) ∈ 𝒫 𝐵) |
| 65 | | fnelfp 7195 |
. . . . . . 7
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ (𝑥 ∪ 𝑦) ∈ 𝒫 𝐵) → ((𝑥 ∪ 𝑦) ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘(𝑥 ∪ 𝑦)) = (𝑥 ∪ 𝑦))) |
| 66 | 50, 64, 65 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → ((𝑥 ∪ 𝑦) ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘(𝑥 ∪ 𝑦)) = (𝑥 ∪ 𝑦))) |
| 67 | 58, 66 | mpbird 257 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝑥 ∪ 𝑦) ∈ dom (𝐹 ∩ I )) |
| 68 | | eqid 2737 |
. . . . 5
⊢ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )} = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )} |
| 69 | 31, 36, 67, 68 | mretopd 23100 |
. . . 4
⊢ (𝜑 → ({𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )} ∈ (TopOn‘𝐵) ∧ dom (𝐹 ∩ I ) = (Clsd‘{𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )}))) |
| 70 | 69 | simpld 494 |
. . 3
⊢ (𝜑 → {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )} ∈ (TopOn‘𝐵)) |
| 71 | 15, 70 | eqeltrd 2841 |
. 2
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐵)) |
| 72 | | topontop 22919 |
. . . . . 6
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) |
| 73 | 71, 72 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ Top) |
| 74 | | eqid 2737 |
. . . . . 6
⊢
(mrCls‘(Clsd‘𝐽)) = (mrCls‘(Clsd‘𝐽)) |
| 75 | 74 | mrccls 23087 |
. . . . 5
⊢ (𝐽 ∈ Top →
(cls‘𝐽) =
(mrCls‘(Clsd‘𝐽))) |
| 76 | 73, 75 | syl 17 |
. . . 4
⊢ (𝜑 → (cls‘𝐽) =
(mrCls‘(Clsd‘𝐽))) |
| 77 | 69 | simprd 495 |
. . . . . 6
⊢ (𝜑 → dom (𝐹 ∩ I ) = (Clsd‘{𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )})) |
| 78 | 15 | fveq2d 6910 |
. . . . . 6
⊢ (𝜑 → (Clsd‘𝐽) = (Clsd‘{𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )})) |
| 79 | 77, 78 | eqtr4d 2780 |
. . . . 5
⊢ (𝜑 → dom (𝐹 ∩ I ) = (Clsd‘𝐽)) |
| 80 | 79 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (mrCls‘dom (𝐹 ∩ I )) =
(mrCls‘(Clsd‘𝐽))) |
| 81 | 76, 80 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → (cls‘𝐽) = (mrCls‘dom (𝐹 ∩ I ))) |
| 82 | 6, 2, 16, 29, 30 | ismrcd2 42710 |
. . 3
⊢ (𝜑 → 𝐹 = (mrCls‘dom (𝐹 ∩ I ))) |
| 83 | 81, 82 | eqtr4d 2780 |
. 2
⊢ (𝜑 → (cls‘𝐽) = 𝐹) |
| 84 | 71, 83 | jca 511 |
1
⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ (cls‘𝐽) = 𝐹)) |