Proof of Theorem istopclsd
Step | Hyp | Ref
| Expression |
1 | | istopclsd.j |
. . . 4
⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧)} |
2 | | istopclsd.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝒫 𝐵⟶𝒫 𝐵) |
3 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐹:𝒫 𝐵⟶𝒫 𝐵 → 𝐹 Fn 𝒫 𝐵) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn 𝒫 𝐵) |
5 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → 𝐹 Fn 𝒫 𝐵) |
6 | | difss 3699 |
. . . . . . . . 9
⊢ (𝐵 ∖ 𝑧) ⊆ 𝐵 |
7 | | istopclsd.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
8 | | elpw2g 4754 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑉 → ((𝐵 ∖ 𝑧) ∈ 𝒫 𝐵 ↔ (𝐵 ∖ 𝑧) ⊆ 𝐵)) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 ∖ 𝑧) ∈ 𝒫 𝐵 ↔ (𝐵 ∖ 𝑧) ⊆ 𝐵)) |
10 | 6, 9 | mpbiri 247 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∖ 𝑧) ∈ 𝒫 𝐵) |
11 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑧) ∈ 𝒫 𝐵) |
12 | | fnelfp 6346 |
. . . . . . 7
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ (𝐵 ∖ 𝑧) ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧))) |
13 | 5, 11, 12 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → ((𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧))) |
14 | 13 | bicomd 212 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝒫 𝐵) → ((𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧) ↔ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I ))) |
15 | 14 | rabbidva 3163 |
. . . 4
⊢ (𝜑 → {𝑧 ∈ 𝒫 𝐵 ∣ (𝐹‘(𝐵 ∖ 𝑧)) = (𝐵 ∖ 𝑧)} = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )}) |
16 | 1, 15 | syl5eq 2656 |
. . 3
⊢ (𝜑 → 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )}) |
17 | | istopclsd.e |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ (𝐹‘𝑥)) |
18 | | simp1 1054 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → 𝜑) |
19 | | simp2 1055 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → 𝑥 ⊆ 𝐵) |
20 | | simp3 1056 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → 𝑦 ⊆ 𝑥) |
21 | 20, 19 | sstrd 3578 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → 𝑦 ⊆ 𝐵) |
22 | | istopclsd.u |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵) → (𝐹‘(𝑥 ∪ 𝑦)) = ((𝐹‘𝑥) ∪ (𝐹‘𝑦))) |
23 | 18, 19, 21, 22 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘(𝑥 ∪ 𝑦)) = ((𝐹‘𝑥) ∪ (𝐹‘𝑦))) |
24 | | ssequn2 3748 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ 𝑥 ↔ (𝑥 ∪ 𝑦) = 𝑥) |
25 | 24 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ 𝑥 → (𝑥 ∪ 𝑦) = 𝑥) |
26 | 25 | 3ad2ant3 1077 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝑥 ∪ 𝑦) = 𝑥) |
27 | 26 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘(𝑥 ∪ 𝑦)) = (𝐹‘𝑥)) |
28 | 23, 27 | eqtr3d 2646 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → ((𝐹‘𝑥) ∪ (𝐹‘𝑦)) = (𝐹‘𝑥)) |
29 | | ssequn2 3748 |
. . . . . . 7
⊢ ((𝐹‘𝑦) ⊆ (𝐹‘𝑥) ↔ ((𝐹‘𝑥) ∪ (𝐹‘𝑦)) = (𝐹‘𝑥)) |
30 | 28, 29 | sylibr 223 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝑥) → (𝐹‘𝑦) ⊆ (𝐹‘𝑥)) |
31 | | istopclsd.i |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐵) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) |
32 | 7, 2, 17, 30, 31 | ismrcd1 36279 |
. . . . 5
⊢ (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵)) |
33 | | istopclsd.z |
. . . . . 6
⊢ (𝜑 → (𝐹‘∅) = ∅) |
34 | | 0elpw 4760 |
. . . . . . 7
⊢ ∅
∈ 𝒫 𝐵 |
35 | | fnelfp 6346 |
. . . . . . 7
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ ∅ ∈ 𝒫 𝐵) → (∅ ∈ dom
(𝐹 ∩ I ) ↔ (𝐹‘∅) =
∅)) |
36 | 4, 34, 35 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → (∅ ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘∅) =
∅)) |
37 | 33, 36 | mpbird 246 |
. . . . 5
⊢ (𝜑 → ∅ ∈ dom (𝐹 ∩ I )) |
38 | | simp1 1054 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → 𝜑) |
39 | | inss1 3795 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∩ I ) ⊆ 𝐹 |
40 | | dmss 5245 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∩ I ) ⊆ 𝐹 → dom (𝐹 ∩ I ) ⊆ dom 𝐹) |
41 | 39, 40 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ dom
(𝐹 ∩ I ) ⊆ dom
𝐹 |
42 | | fdm 5964 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝒫 𝐵⟶𝒫 𝐵 → dom 𝐹 = 𝒫 𝐵) |
43 | 2, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐹 = 𝒫 𝐵) |
44 | 41, 43 | syl5sseq 3616 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵) |
45 | 44 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵) |
46 | | simp2 1055 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → 𝑥 ∈ dom (𝐹 ∩ I )) |
47 | 45, 46 | sseldd 3569 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → 𝑥 ∈ 𝒫 𝐵) |
48 | 47 | elpwid 4118 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → 𝑥 ⊆ 𝐵) |
49 | | simp3 1056 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → 𝑦 ∈ dom (𝐹 ∩ I )) |
50 | 45, 49 | sseldd 3569 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → 𝑦 ∈ 𝒫 𝐵) |
51 | 50 | elpwid 4118 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → 𝑦 ⊆ 𝐵) |
52 | 38, 48, 51, 22 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝐹‘(𝑥 ∪ 𝑦)) = ((𝐹‘𝑥) ∪ (𝐹‘𝑦))) |
53 | 4 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → 𝐹 Fn 𝒫 𝐵) |
54 | | fnelfp 6346 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ 𝑥 ∈ 𝒫 𝐵) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑥) = 𝑥)) |
55 | 53, 47, 54 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑥) = 𝑥)) |
56 | 46, 55 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝐹‘𝑥) = 𝑥) |
57 | | fnelfp 6346 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ 𝑦 ∈ 𝒫 𝐵) → (𝑦 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑦) = 𝑦)) |
58 | 53, 50, 57 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝑦 ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘𝑦) = 𝑦)) |
59 | 49, 58 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝐹‘𝑦) = 𝑦) |
60 | 56, 59 | uneq12d 3730 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → ((𝐹‘𝑥) ∪ (𝐹‘𝑦)) = (𝑥 ∪ 𝑦)) |
61 | 52, 60 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝐹‘(𝑥 ∪ 𝑦)) = (𝑥 ∪ 𝑦)) |
62 | 48, 51 | unssd 3751 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝑥 ∪ 𝑦) ⊆ 𝐵) |
63 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
64 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
65 | 63, 64 | unex 6854 |
. . . . . . . . 9
⊢ (𝑥 ∪ 𝑦) ∈ V |
66 | 65 | elpw 4114 |
. . . . . . . 8
⊢ ((𝑥 ∪ 𝑦) ∈ 𝒫 𝐵 ↔ (𝑥 ∪ 𝑦) ⊆ 𝐵) |
67 | 62, 66 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝑥 ∪ 𝑦) ∈ 𝒫 𝐵) |
68 | | fnelfp 6346 |
. . . . . . 7
⊢ ((𝐹 Fn 𝒫 𝐵 ∧ (𝑥 ∪ 𝑦) ∈ 𝒫 𝐵) → ((𝑥 ∪ 𝑦) ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘(𝑥 ∪ 𝑦)) = (𝑥 ∪ 𝑦))) |
69 | 53, 67, 68 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → ((𝑥 ∪ 𝑦) ∈ dom (𝐹 ∩ I ) ↔ (𝐹‘(𝑥 ∪ 𝑦)) = (𝑥 ∪ 𝑦))) |
70 | 61, 69 | mpbird 246 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐹 ∩ I ) ∧ 𝑦 ∈ dom (𝐹 ∩ I )) → (𝑥 ∪ 𝑦) ∈ dom (𝐹 ∩ I )) |
71 | | eqid 2610 |
. . . . 5
⊢ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )} = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )} |
72 | 32, 37, 70, 71 | mretopd 20706 |
. . . 4
⊢ (𝜑 → ({𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )} ∈ (TopOn‘𝐵) ∧ dom (𝐹 ∩ I ) = (Clsd‘{𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )}))) |
73 | 72 | simpld 474 |
. . 3
⊢ (𝜑 → {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )} ∈ (TopOn‘𝐵)) |
74 | 16, 73 | eqeltrd 2688 |
. 2
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐵)) |
75 | | topontop 20541 |
. . . . . 6
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) |
76 | 74, 75 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ Top) |
77 | | eqid 2610 |
. . . . . 6
⊢
(mrCls‘(Clsd‘𝐽)) = (mrCls‘(Clsd‘𝐽)) |
78 | 77 | mrccls 20693 |
. . . . 5
⊢ (𝐽 ∈ Top →
(cls‘𝐽) =
(mrCls‘(Clsd‘𝐽))) |
79 | 76, 78 | syl 17 |
. . . 4
⊢ (𝜑 → (cls‘𝐽) =
(mrCls‘(Clsd‘𝐽))) |
80 | 72 | simprd 478 |
. . . . . 6
⊢ (𝜑 → dom (𝐹 ∩ I ) = (Clsd‘{𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )})) |
81 | 16 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 → (Clsd‘𝐽) = (Clsd‘{𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ dom (𝐹 ∩ I )})) |
82 | 80, 81 | eqtr4d 2647 |
. . . . 5
⊢ (𝜑 → dom (𝐹 ∩ I ) = (Clsd‘𝐽)) |
83 | 82 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (mrCls‘dom (𝐹 ∩ I )) =
(mrCls‘(Clsd‘𝐽))) |
84 | 79, 83 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → (cls‘𝐽) = (mrCls‘dom (𝐹 ∩ I ))) |
85 | 7, 2, 17, 30, 31 | ismrcd2 36280 |
. . 3
⊢ (𝜑 → 𝐹 = (mrCls‘dom (𝐹 ∩ I ))) |
86 | 84, 85 | eqtr4d 2647 |
. 2
⊢ (𝜑 → (cls‘𝐽) = 𝐹) |
87 | 74, 86 | jca 553 |
1
⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ (cls‘𝐽) = 𝐹)) |