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