Metamath Proof Explorer

Theorem iscldtop

Description: A family is the closed sets of a topology iff it is a Moore collection and closed under finite union. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Assertion iscldtop ⊢K∈ClsdTopOn⁡B↔K∈Moore⁡B∧∅∈K∧∀x∈K∀y∈Kx∪y∈K

Proof

Step Hyp Ref Expression
1 fncld ⊢ClsdFnTop
2 fnfun ⊢ClsdFnTop→Fun⁡Clsd
3 1 2 ax-mp ⊢Fun⁡Clsd
4 fvelima ⊢Fun⁡Clsd∧K∈ClsdTopOn⁡B→∃a∈TopOn⁡BClsd⁡a=K
5 3 4 mpan ⊢K∈ClsdTopOn⁡B→∃a∈TopOn⁡BClsd⁡a=K
6 cldmreon ⊢a∈TopOn⁡B→Clsd⁡a∈Moore⁡B
7 topontop ⊢a∈TopOn⁡B→a∈Top
8 0cld ⊢a∈Top→∅∈Clsd⁡a
9 7 8 syl ⊢a∈TopOn⁡B→∅∈Clsd⁡a
10 uncld ⊢x∈Clsd⁡a∧y∈Clsd⁡a→x∪y∈Clsd⁡a
11 10 adantl ⊢a∈TopOn⁡B∧x∈Clsd⁡a∧y∈Clsd⁡a→x∪y∈Clsd⁡a
12 11 ralrimivva ⊢a∈TopOn⁡B→∀x∈Clsd⁡a∀y∈Clsd⁡ax∪y∈Clsd⁡a
13 6 9 12 3jca ⊢a∈TopOn⁡B→Clsd⁡a∈Moore⁡B∧∅∈Clsd⁡a∧∀x∈Clsd⁡a∀y∈Clsd⁡ax∪y∈Clsd⁡a
14 eleq1 ⊢Clsd⁡a=K→Clsd⁡a∈Moore⁡B↔K∈Moore⁡B
15 eleq2 ⊢Clsd⁡a=K→∅∈Clsd⁡a↔∅∈K
16 eleq2 ⊢Clsd⁡a=K→x∪y∈Clsd⁡a↔x∪y∈K
17 16 raleqbi1dv ⊢Clsd⁡a=K→∀y∈Clsd⁡ax∪y∈Clsd⁡a↔∀y∈Kx∪y∈K
18 17 raleqbi1dv ⊢Clsd⁡a=K→∀x∈Clsd⁡a∀y∈Clsd⁡ax∪y∈Clsd⁡a↔∀x∈K∀y∈Kx∪y∈K
19 14 15 18 3anbi123d ⊢Clsd⁡a=K→Clsd⁡a∈Moore⁡B∧∅∈Clsd⁡a∧∀x∈Clsd⁡a∀y∈Clsd⁡ax∪y∈Clsd⁡a↔K∈Moore⁡B∧∅∈K∧∀x∈K∀y∈Kx∪y∈K
20 13 19 syl5ibcom ⊢a∈TopOn⁡B→Clsd⁡a=K→K∈Moore⁡B∧∅∈K∧∀x∈K∀y∈Kx∪y∈K
21 20 rexlimiv ⊢∃a∈TopOn⁡BClsd⁡a=K→K∈Moore⁡B∧∅∈K∧∀x∈K∀y∈Kx∪y∈K
22 5 21 syl ⊢K∈ClsdTopOn⁡B→K∈Moore⁡B∧∅∈K∧∀x∈K∀y∈Kx∪y∈K
23 simp1 ⊢K∈Moore⁡B∧∅∈K∧∀x∈K∀y∈Kx∪y∈K→K∈Moore⁡B
24 simp2 ⊢K∈Moore⁡B∧∅∈K∧∀x∈K∀y∈Kx∪y∈K→∅∈K
25 uneq1 ⊢x=b→x∪y=b∪y
26 25 eleq1d ⊢x=b→x∪y∈K↔b∪y∈K
27 uneq2 ⊢y=c→b∪y=b∪c
28 27 eleq1d ⊢y=c→b∪y∈K↔b∪c∈K
29 26 28 rspc2v ⊢b∈K∧c∈K→∀x∈K∀y∈Kx∪y∈K→b∪c∈K
30 29 com12 ⊢∀x∈K∀y∈Kx∪y∈K→b∈K∧c∈K→b∪c∈K
31 30 3ad2ant3 ⊢K∈Moore⁡B∧∅∈K∧∀x∈K∀y∈Kx∪y∈K→b∈K∧c∈K→b∪c∈K
32 31 3impib ⊢K∈Moore⁡B∧∅∈K∧∀x∈K∀y∈Kx∪y∈K∧b∈K∧c∈K→b∪c∈K
33 eqid ⊢a∈𝒫B|B∖a∈K=a∈𝒫B|B∖a∈K
34 23 24 32 33 mretopd ⊢K∈Moore⁡B∧∅∈K∧∀x∈K∀y∈Kx∪y∈K→a∈𝒫B|B∖a∈K∈TopOn⁡B∧K=Clsd⁡a∈𝒫B|B∖a∈K
35 34 simprd ⊢K∈Moore⁡B∧∅∈K∧∀x∈K∀y∈Kx∪y∈K→K=Clsd⁡a∈𝒫B|B∖a∈K
36 34 simpld ⊢K∈Moore⁡B∧∅∈K∧∀x∈K∀y∈Kx∪y∈K→a∈𝒫B|B∖a∈K∈TopOn⁡B
37 7 ssriv ⊢TopOn⁡B⊆Top
38 1 fndmi ⊢dom⁡Clsd=Top
39 37 38 sseqtrri ⊢TopOn⁡B⊆dom⁡Clsd
40 funfvima2 ⊢Fun⁡Clsd∧TopOn⁡B⊆dom⁡Clsd→a∈𝒫B|B∖a∈K∈TopOn⁡B→Clsd⁡a∈𝒫B|B∖a∈K∈ClsdTopOn⁡B
41 3 39 40 mp2an ⊢a∈𝒫B|B∖a∈K∈TopOn⁡B→Clsd⁡a∈𝒫B|B∖a∈K∈ClsdTopOn⁡B
42 36 41 syl ⊢K∈Moore⁡B∧∅∈K∧∀x∈K∀y∈Kx∪y∈K→Clsd⁡a∈𝒫B|B∖a∈K∈ClsdTopOn⁡B
43 35 42 eqeltrd ⊢K∈Moore⁡B∧∅∈K∧∀x∈K∀y∈Kx∪y∈K→K∈ClsdTopOn⁡B
44 22 43 impbii ⊢K∈ClsdTopOn⁡B↔K∈Moore⁡B∧∅∈K∧∀x∈K∀y∈Kx∪y∈K