This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐾 ∈ ( Clsd “ ( TopOn ‘ 𝐵 ) ) ↔ ( 𝐾 ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) )

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 ∧ 𝐾 ∈ ( Clsd “ ( TopOn ‘ 𝐵 ) ) ) → ∃ 𝑎 ∈ ( TopOn ‘ 𝐵 ) ( Clsd ‘ 𝑎 ) = 𝐾 )
5 3 4 mpan ⊢ ( 𝐾 ∈ ( Clsd “ ( TopOn ‘ 𝐵 ) ) → ∃ 𝑎 ∈ ( TopOn ‘ 𝐵 ) ( Clsd ‘ 𝑎 ) = 𝐾 )
6 cldmreon ⊢ ( 𝑎 ∈ ( TopOn ‘ 𝐵 ) → ( Clsd ‘ 𝑎 ) ∈ ( Moore ‘ 𝐵 ) )
7 topontop ⊢ ( 𝑎 ∈ ( TopOn ‘ 𝐵 ) → 𝑎 ∈ Top )
8 0cld ⊢ ( 𝑎 ∈ Top → ∅ ∈ ( Clsd ‘ 𝑎 ) )
9 7 8 syl ⊢ ( 𝑎 ∈ ( TopOn ‘ 𝐵 ) → ∅ ∈ ( Clsd ‘ 𝑎 ) )
10 uncld ⊢ ( ( 𝑥 ∈ ( Clsd ‘ 𝑎 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝑎 ) ) → ( 𝑥 ∪ 𝑦 ) ∈ ( Clsd ‘ 𝑎 ) )
11 10 adantl ⊢ ( ( 𝑎 ∈ ( TopOn ‘ 𝐵 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝑎 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝑎 ) ) ) → ( 𝑥 ∪ 𝑦 ) ∈ ( Clsd ‘ 𝑎 ) )
12 11 ralrimivva ⊢ ( 𝑎 ∈ ( TopOn ‘ 𝐵 ) → ∀ 𝑥 ∈ ( Clsd ‘ 𝑎 ) ∀ 𝑦 ∈ ( Clsd ‘ 𝑎 ) ( 𝑥 ∪ 𝑦 ) ∈ ( Clsd ‘ 𝑎 ) )
13 6 9 12 3jca ⊢ ( 𝑎 ∈ ( TopOn ‘ 𝐵 ) → ( ( Clsd ‘ 𝑎 ) ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ ( Clsd ‘ 𝑎 ) ∧ ∀ 𝑥 ∈ ( Clsd ‘ 𝑎 ) ∀ 𝑦 ∈ ( Clsd ‘ 𝑎 ) ( 𝑥 ∪ 𝑦 ) ∈ ( Clsd ‘ 𝑎 ) ) )
14 eleq1 ⊢ ( ( Clsd ‘ 𝑎 ) = 𝐾 → ( ( Clsd ‘ 𝑎 ) ∈ ( Moore ‘ 𝐵 ) ↔ 𝐾 ∈ ( Moore ‘ 𝐵 ) ) )
15 eleq2 ⊢ ( ( Clsd ‘ 𝑎 ) = 𝐾 → ( ∅ ∈ ( Clsd ‘ 𝑎 ) ↔ ∅ ∈ 𝐾 ) )
16 eleq2 ⊢ ( ( Clsd ‘ 𝑎 ) = 𝐾 → ( ( 𝑥 ∪ 𝑦 ) ∈ ( Clsd ‘ 𝑎 ) ↔ ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) )
17 16 raleqbi1dv ⊢ ( ( Clsd ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑦 ∈ ( Clsd ‘ 𝑎 ) ( 𝑥 ∪ 𝑦 ) ∈ ( Clsd ‘ 𝑎 ) ↔ ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) )
18 17 raleqbi1dv ⊢ ( ( Clsd ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑥 ∈ ( Clsd ‘ 𝑎 ) ∀ 𝑦 ∈ ( Clsd ‘ 𝑎 ) ( 𝑥 ∪ 𝑦 ) ∈ ( Clsd ‘ 𝑎 ) ↔ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) )
19 14 15 18 3anbi123d ⊢ ( ( Clsd ‘ 𝑎 ) = 𝐾 → ( ( ( Clsd ‘ 𝑎 ) ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ ( Clsd ‘ 𝑎 ) ∧ ∀ 𝑥 ∈ ( Clsd ‘ 𝑎 ) ∀ 𝑦 ∈ ( Clsd ‘ 𝑎 ) ( 𝑥 ∪ 𝑦 ) ∈ ( Clsd ‘ 𝑎 ) ) ↔ ( 𝐾 ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) ) )
20 13 19 syl5ibcom ⊢ ( 𝑎 ∈ ( TopOn ‘ 𝐵 ) → ( ( Clsd ‘ 𝑎 ) = 𝐾 → ( 𝐾 ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) ) )
21 20 rexlimiv ⊢ ( ∃ 𝑎 ∈ ( TopOn ‘ 𝐵 ) ( Clsd ‘ 𝑎 ) = 𝐾 → ( 𝐾 ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) )
22 5 21 syl ⊢ ( 𝐾 ∈ ( Clsd “ ( TopOn ‘ 𝐵 ) ) → ( 𝐾 ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) )
23 simp1 ⊢ ( ( 𝐾 ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) → 𝐾 ∈ ( Moore ‘ 𝐵 ) )
24 simp2 ⊢ ( ( 𝐾 ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) → ∅ ∈ 𝐾 )
25 uneq1 ⊢ ( 𝑥 = 𝑏 → ( 𝑥 ∪ 𝑦 ) = ( 𝑏 ∪ 𝑦 ) )
26 25 eleq1d ⊢ ( 𝑥 = 𝑏 → ( ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ↔ ( 𝑏 ∪ 𝑦 ) ∈ 𝐾 ) )
27 uneq2 ⊢ ( 𝑦 = 𝑐 → ( 𝑏 ∪ 𝑦 ) = ( 𝑏 ∪ 𝑐 ) )
28 27 eleq1d ⊢ ( 𝑦 = 𝑐 → ( ( 𝑏 ∪ 𝑦 ) ∈ 𝐾 ↔ ( 𝑏 ∪ 𝑐 ) ∈ 𝐾 ) )
29 26 28 rspc2v ⊢ ( ( 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝐾 ) → ( ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 → ( 𝑏 ∪ 𝑐 ) ∈ 𝐾 ) )
30 29 com12 ⊢ ( ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 → ( ( 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝐾 ) → ( 𝑏 ∪ 𝑐 ) ∈ 𝐾 ) )
31 30 3ad2ant3 ⊢ ( ( 𝐾 ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) → ( ( 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝐾 ) → ( 𝑏 ∪ 𝑐 ) ∈ 𝐾 ) )
32 31 3impib ⊢ ( ( ( 𝐾 ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) ∧ 𝑏 ∈ 𝐾 ∧ 𝑐 ∈ 𝐾 ) → ( 𝑏 ∪ 𝑐 ) ∈ 𝐾 )
33 eqid ⊢ { 𝑎 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑎 ) ∈ 𝐾 } = { 𝑎 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑎 ) ∈ 𝐾 }
34 23 24 32 33 mretopd ⊢ ( ( 𝐾 ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) → ( { 𝑎 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑎 ) ∈ 𝐾 } ∈ ( TopOn ‘ 𝐵 ) ∧ 𝐾 = ( Clsd ‘ { 𝑎 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑎 ) ∈ 𝐾 } ) ) )
35 34 simprd ⊢ ( ( 𝐾 ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) → 𝐾 = ( Clsd ‘ { 𝑎 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑎 ) ∈ 𝐾 } ) )
36 34 simpld ⊢ ( ( 𝐾 ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) → { 𝑎 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑎 ) ∈ 𝐾 } ∈ ( TopOn ‘ 𝐵 ) )
37 7 ssriv ⊢ ( TopOn ‘ 𝐵 ) ⊆ Top
38 1 fndmi ⊢ dom Clsd = Top
39 37 38 sseqtrri ⊢ ( TopOn ‘ 𝐵 ) ⊆ dom Clsd
40 funfvima2 ⊢ ( ( Fun Clsd ∧ ( TopOn ‘ 𝐵 ) ⊆ dom Clsd ) → ( { 𝑎 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑎 ) ∈ 𝐾 } ∈ ( TopOn ‘ 𝐵 ) → ( Clsd ‘ { 𝑎 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑎 ) ∈ 𝐾 } ) ∈ ( Clsd “ ( TopOn ‘ 𝐵 ) ) ) )
41 3 39 40 mp2an ⊢ ( { 𝑎 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑎 ) ∈ 𝐾 } ∈ ( TopOn ‘ 𝐵 ) → ( Clsd ‘ { 𝑎 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑎 ) ∈ 𝐾 } ) ∈ ( Clsd “ ( TopOn ‘ 𝐵 ) ) )
42 36 41 syl ⊢ ( ( 𝐾 ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) → ( Clsd ‘ { 𝑎 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑎 ) ∈ 𝐾 } ) ∈ ( Clsd “ ( TopOn ‘ 𝐵 ) ) )
43 35 42 eqeltrd ⊢ ( ( 𝐾 ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) → 𝐾 ∈ ( Clsd “ ( TopOn ‘ 𝐵 ) ) )
44 22 43 impbii ⊢ ( 𝐾 ∈ ( Clsd “ ( TopOn ‘ 𝐵 ) ) ↔ ( 𝐾 ∈ ( Moore ‘ 𝐵 ) ∧ ∅ ∈ 𝐾 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝑥 ∪ 𝑦 ) ∈ 𝐾 ) )