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