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 ∈ Clsd TopOn ⁡ B ↔ K ∈ Moore ⁡ B ∧ ∅ ∈ K ∧ ∀ x ∈ K ∀ y ∈ K x ∪ y ∈ K

Proof

Step Hyp Ref Expression
1 fncld ⊢ Clsd Fn Top
2 fnfun ⊢ Clsd Fn Top → Fun ⁡ Clsd
3 1 2 ax-mp ⊢ Fun ⁡ Clsd
4 fvelima ⊢ Fun ⁡ Clsd ∧ K ∈ Clsd TopOn ⁡ B → ∃ a ∈ TopOn ⁡ B Clsd ⁡ a = K
5 3 4 mpan ⊢ K ∈ Clsd TopOn ⁡ B → ∃ a ∈ TopOn ⁡ B Clsd ⁡ 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 ⁡ a x ∪ y ∈ Clsd ⁡ a
13 6 9 12 3jca ⊢ a ∈ TopOn ⁡ B → Clsd ⁡ a ∈ Moore ⁡ B ∧ ∅ ∈ Clsd ⁡ a ∧ ∀ x ∈ Clsd ⁡ a ∀ y ∈ Clsd ⁡ a x ∪ 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 ⁡ a x ∪ y ∈ Clsd ⁡ a ↔ ∀ y ∈ K x ∪ y ∈ K
18 17 raleqbi1dv ⊢ Clsd ⁡ a = K → ∀ x ∈ Clsd ⁡ a ∀ y ∈ Clsd ⁡ a x ∪ y ∈ Clsd ⁡ a ↔ ∀ x ∈ K ∀ y ∈ K x ∪ y ∈ K
19 14 15 18 3anbi123d ⊢ Clsd ⁡ a = K → Clsd ⁡ a ∈ Moore ⁡ B ∧ ∅ ∈ Clsd ⁡ a ∧ ∀ x ∈ Clsd ⁡ a ∀ y ∈ Clsd ⁡ a x ∪ y ∈ Clsd ⁡ a ↔ K ∈ Moore ⁡ B ∧ ∅ ∈ K ∧ ∀ x ∈ K ∀ y ∈ K x ∪ y ∈ K
20 13 19 syl5ibcom ⊢ a ∈ TopOn ⁡ B → Clsd ⁡ a = K → K ∈ Moore ⁡ B ∧ ∅ ∈ K ∧ ∀ x ∈ K ∀ y ∈ K x ∪ y ∈ K
21 20 rexlimiv ⊢ ∃ a ∈ TopOn ⁡ B Clsd ⁡ a = K → K ∈ Moore ⁡ B ∧ ∅ ∈ K ∧ ∀ x ∈ K ∀ y ∈ K x ∪ y ∈ K
22 5 21 syl ⊢ K ∈ Clsd TopOn ⁡ B → K ∈ Moore ⁡ B ∧ ∅ ∈ K ∧ ∀ x ∈ K ∀ y ∈ K x ∪ y ∈ K
23 simp1 ⊢ K ∈ Moore ⁡ B ∧ ∅ ∈ K ∧ ∀ x ∈ K ∀ y ∈ K x ∪ y ∈ K → K ∈ Moore ⁡ B
24 simp2 ⊢ K ∈ Moore ⁡ B ∧ ∅ ∈ K ∧ ∀ x ∈ K ∀ y ∈ K x ∪ 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 ∈ K x ∪ y ∈ K → b ∪ c ∈ K
30 29 com12 ⊢ ∀ x ∈ K ∀ y ∈ K x ∪ y ∈ K → b ∈ K ∧ c ∈ K → b ∪ c ∈ K
31 30 3ad2ant3 ⊢ K ∈ Moore ⁡ B ∧ ∅ ∈ K ∧ ∀ x ∈ K ∀ y ∈ K x ∪ y ∈ K → b ∈ K ∧ c ∈ K → b ∪ c ∈ K
32 31 3impib ⊢ K ∈ Moore ⁡ B ∧ ∅ ∈ K ∧ ∀ x ∈ K ∀ y ∈ K x ∪ 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 ∈ K x ∪ 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 ∈ K x ∪ y ∈ K → K = Clsd ⁡ a ∈ 𝒫 B | B ∖ a ∈ K
36 34 simpld ⊢ K ∈ Moore ⁡ B ∧ ∅ ∈ K ∧ ∀ x ∈ K ∀ y ∈ K x ∪ 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 ∈ Clsd TopOn ⁡ B
41 3 39 40 mp2an ⊢ a ∈ 𝒫 B | B ∖ a ∈ K ∈ TopOn ⁡ B → Clsd ⁡ a ∈ 𝒫 B | B ∖ a ∈ K ∈ Clsd TopOn ⁡ B
42 36 41 syl ⊢ K ∈ Moore ⁡ B ∧ ∅ ∈ K ∧ ∀ x ∈ K ∀ y ∈ K x ∪ y ∈ K → Clsd ⁡ a ∈ 𝒫 B | B ∖ a ∈ K ∈ Clsd TopOn ⁡ B
43 35 42 eqeltrd ⊢ K ∈ Moore ⁡ B ∧ ∅ ∈ K ∧ ∀ x ∈ K ∀ y ∈ K x ∪ y ∈ K → K ∈ Clsd TopOn ⁡ B
44 22 43 impbii ⊢ K ∈ Clsd TopOn ⁡ B ↔ K ∈ Moore ⁡ B ∧ ∅ ∈ K ∧ ∀ x ∈ K ∀ y ∈ K x ∪ y ∈ K