| Step | Hyp | Ref
| Expression |
| 1 | | fncld 23030 |
. . . . 5
⊢ Clsd Fn
Top |
| 2 | | fnfun 6668 |
. . . . 5
⊢ (Clsd Fn
Top → Fun Clsd) |
| 3 | 1, 2 | ax-mp 5 |
. . . 4
⊢ Fun
Clsd |
| 4 | | fvelima 6974 |
. . . 4
⊢ ((Fun
Clsd ∧ 𝐾 ∈ (Clsd
“ (TopOn‘𝐵)))
→ ∃𝑎 ∈
(TopOn‘𝐵)(Clsd‘𝑎) = 𝐾) |
| 5 | 3, 4 | mpan 690 |
. . 3
⊢ (𝐾 ∈ (Clsd “
(TopOn‘𝐵)) →
∃𝑎 ∈
(TopOn‘𝐵)(Clsd‘𝑎) = 𝐾) |
| 6 | | cldmreon 23102 |
. . . . . 6
⊢ (𝑎 ∈ (TopOn‘𝐵) → (Clsd‘𝑎) ∈ (Moore‘𝐵)) |
| 7 | | topontop 22919 |
. . . . . . 7
⊢ (𝑎 ∈ (TopOn‘𝐵) → 𝑎 ∈ Top) |
| 8 | | 0cld 23046 |
. . . . . . 7
⊢ (𝑎 ∈ Top → ∅
∈ (Clsd‘𝑎)) |
| 9 | 7, 8 | syl 17 |
. . . . . 6
⊢ (𝑎 ∈ (TopOn‘𝐵) → ∅ ∈
(Clsd‘𝑎)) |
| 10 | | uncld 23049 |
. . . . . . . 8
⊢ ((𝑥 ∈ (Clsd‘𝑎) ∧ 𝑦 ∈ (Clsd‘𝑎)) → (𝑥 ∪ 𝑦) ∈ (Clsd‘𝑎)) |
| 11 | 10 | adantl 481 |
. . . . . . 7
⊢ ((𝑎 ∈ (TopOn‘𝐵) ∧ (𝑥 ∈ (Clsd‘𝑎) ∧ 𝑦 ∈ (Clsd‘𝑎))) → (𝑥 ∪ 𝑦) ∈ (Clsd‘𝑎)) |
| 12 | 11 | ralrimivva 3202 |
. . . . . 6
⊢ (𝑎 ∈ (TopOn‘𝐵) → ∀𝑥 ∈ (Clsd‘𝑎)∀𝑦 ∈ (Clsd‘𝑎)(𝑥 ∪ 𝑦) ∈ (Clsd‘𝑎)) |
| 13 | 6, 9, 12 | 3jca 1129 |
. . . . 5
⊢ (𝑎 ∈ (TopOn‘𝐵) → ((Clsd‘𝑎) ∈ (Moore‘𝐵) ∧ ∅ ∈
(Clsd‘𝑎) ∧
∀𝑥 ∈
(Clsd‘𝑎)∀𝑦 ∈ (Clsd‘𝑎)(𝑥 ∪ 𝑦) ∈ (Clsd‘𝑎))) |
| 14 | | eleq1 2829 |
. . . . . 6
⊢
((Clsd‘𝑎) =
𝐾 → ((Clsd‘𝑎) ∈ (Moore‘𝐵) ↔ 𝐾 ∈ (Moore‘𝐵))) |
| 15 | | eleq2 2830 |
. . . . . 6
⊢
((Clsd‘𝑎) =
𝐾 → (∅ ∈
(Clsd‘𝑎) ↔
∅ ∈ 𝐾)) |
| 16 | | eleq2 2830 |
. . . . . . . 8
⊢
((Clsd‘𝑎) =
𝐾 → ((𝑥 ∪ 𝑦) ∈ (Clsd‘𝑎) ↔ (𝑥 ∪ 𝑦) ∈ 𝐾)) |
| 17 | 16 | raleqbi1dv 3338 |
. . . . . . 7
⊢
((Clsd‘𝑎) =
𝐾 → (∀𝑦 ∈ (Clsd‘𝑎)(𝑥 ∪ 𝑦) ∈ (Clsd‘𝑎) ↔ ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾)) |
| 18 | 17 | raleqbi1dv 3338 |
. . . . . 6
⊢
((Clsd‘𝑎) =
𝐾 → (∀𝑥 ∈ (Clsd‘𝑎)∀𝑦 ∈ (Clsd‘𝑎)(𝑥 ∪ 𝑦) ∈ (Clsd‘𝑎) ↔ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾)) |
| 19 | 14, 15, 18 | 3anbi123d 1438 |
. . . . 5
⊢
((Clsd‘𝑎) =
𝐾 →
(((Clsd‘𝑎) ∈
(Moore‘𝐵) ∧
∅ ∈ (Clsd‘𝑎) ∧ ∀𝑥 ∈ (Clsd‘𝑎)∀𝑦 ∈ (Clsd‘𝑎)(𝑥 ∪ 𝑦) ∈ (Clsd‘𝑎)) ↔ (𝐾 ∈ (Moore‘𝐵) ∧ ∅ ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾))) |
| 20 | 13, 19 | syl5ibcom 245 |
. . . 4
⊢ (𝑎 ∈ (TopOn‘𝐵) → ((Clsd‘𝑎) = 𝐾 → (𝐾 ∈ (Moore‘𝐵) ∧ ∅ ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾))) |
| 21 | 20 | rexlimiv 3148 |
. . 3
⊢
(∃𝑎 ∈
(TopOn‘𝐵)(Clsd‘𝑎) = 𝐾 → (𝐾 ∈ (Moore‘𝐵) ∧ ∅ ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾)) |
| 22 | 5, 21 | syl 17 |
. 2
⊢ (𝐾 ∈ (Clsd “
(TopOn‘𝐵)) →
(𝐾 ∈
(Moore‘𝐵) ∧
∅ ∈ 𝐾 ∧
∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾)) |
| 23 | | simp1 1137 |
. . . . 5
⊢ ((𝐾 ∈ (Moore‘𝐵) ∧ ∅ ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾) → 𝐾 ∈ (Moore‘𝐵)) |
| 24 | | simp2 1138 |
. . . . 5
⊢ ((𝐾 ∈ (Moore‘𝐵) ∧ ∅ ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾) → ∅ ∈ 𝐾) |
| 25 | | uneq1 4161 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑏 → (𝑥 ∪ 𝑦) = (𝑏 ∪ 𝑦)) |
| 26 | 25 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑥 = 𝑏 → ((𝑥 ∪ 𝑦) ∈ 𝐾 ↔ (𝑏 ∪ 𝑦) ∈ 𝐾)) |
| 27 | | uneq2 4162 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑐 → (𝑏 ∪ 𝑦) = (𝑏 ∪ 𝑐)) |
| 28 | 27 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑦 = 𝑐 → ((𝑏 ∪ 𝑦) ∈ 𝐾 ↔ (𝑏 ∪ 𝑐) ∈ 𝐾)) |
| 29 | 26, 28 | rspc2v 3633 |
. . . . . . . 8
⊢ ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝐾) → (∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾 → (𝑏 ∪ 𝑐) ∈ 𝐾)) |
| 30 | 29 | com12 32 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾 → ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝐾) → (𝑏 ∪ 𝑐) ∈ 𝐾)) |
| 31 | 30 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝐾 ∈ (Moore‘𝐵) ∧ ∅ ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾) → ((𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝐾) → (𝑏 ∪ 𝑐) ∈ 𝐾)) |
| 32 | 31 | 3impib 1117 |
. . . . 5
⊢ (((𝐾 ∈ (Moore‘𝐵) ∧ ∅ ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾) ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝐾) → (𝑏 ∪ 𝑐) ∈ 𝐾) |
| 33 | | eqid 2737 |
. . . . 5
⊢ {𝑎 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑎) ∈ 𝐾} = {𝑎 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑎) ∈ 𝐾} |
| 34 | 23, 24, 32, 33 | mretopd 23100 |
. . . 4
⊢ ((𝐾 ∈ (Moore‘𝐵) ∧ ∅ ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾) → ({𝑎 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑎) ∈ 𝐾} ∈ (TopOn‘𝐵) ∧ 𝐾 = (Clsd‘{𝑎 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑎) ∈ 𝐾}))) |
| 35 | 34 | simprd 495 |
. . 3
⊢ ((𝐾 ∈ (Moore‘𝐵) ∧ ∅ ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾) → 𝐾 = (Clsd‘{𝑎 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑎) ∈ 𝐾})) |
| 36 | 34 | simpld 494 |
. . . 4
⊢ ((𝐾 ∈ (Moore‘𝐵) ∧ ∅ ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾) → {𝑎 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑎) ∈ 𝐾} ∈ (TopOn‘𝐵)) |
| 37 | 7 | ssriv 3987 |
. . . . . 6
⊢
(TopOn‘𝐵)
⊆ Top |
| 38 | 1 | fndmi 6672 |
. . . . . 6
⊢ dom Clsd
= Top |
| 39 | 37, 38 | sseqtrri 4033 |
. . . . 5
⊢
(TopOn‘𝐵)
⊆ dom Clsd |
| 40 | | funfvima2 7251 |
. . . . 5
⊢ ((Fun
Clsd ∧ (TopOn‘𝐵)
⊆ dom Clsd) → ({𝑎 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑎) ∈ 𝐾} ∈ (TopOn‘𝐵) → (Clsd‘{𝑎 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑎) ∈ 𝐾}) ∈ (Clsd “ (TopOn‘𝐵)))) |
| 41 | 3, 39, 40 | mp2an 692 |
. . . 4
⊢ ({𝑎 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑎) ∈ 𝐾} ∈ (TopOn‘𝐵) → (Clsd‘{𝑎 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑎) ∈ 𝐾}) ∈ (Clsd “ (TopOn‘𝐵))) |
| 42 | 36, 41 | syl 17 |
. . 3
⊢ ((𝐾 ∈ (Moore‘𝐵) ∧ ∅ ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾) → (Clsd‘{𝑎 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑎) ∈ 𝐾}) ∈ (Clsd “ (TopOn‘𝐵))) |
| 43 | 35, 42 | eqeltrd 2841 |
. 2
⊢ ((𝐾 ∈ (Moore‘𝐵) ∧ ∅ ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾) → 𝐾 ∈ (Clsd “ (TopOn‘𝐵))) |
| 44 | 22, 43 | impbii 209 |
1
⊢ (𝐾 ∈ (Clsd “
(TopOn‘𝐵)) ↔
(𝐾 ∈
(Moore‘𝐵) ∧
∅ ∈ 𝐾 ∧
∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾)) |