Metamath Proof Explorer

Theorem toponmre

Description: The topologies over a given base set form a Moore collection: the intersection of any family of them is a topology, including the empty (relative) intersection which gives the discrete topology distop . (Contributed by Stefan O'Rear, 31-Jan-2015) (Revised by Mario Carneiro, 5-May-2015)

Ref Expression
Assertion toponmre ⊢B∈V→TopOn⁡B∈Moore⁡𝒫B

Proof

Step Hyp Ref Expression
1 toponsspwpw ⊢TopOn⁡B⊆𝒫𝒫B
2 1 a1i ⊢B∈V→TopOn⁡B⊆𝒫𝒫B
3 distopon ⊢B∈V→𝒫B∈TopOn⁡B
4 simpl ⊢b⊆TopOn⁡B∧b≠∅→b⊆TopOn⁡B
5 4 sselda ⊢b⊆TopOn⁡B∧b≠∅∧x∈b→x∈TopOn⁡B
6 5 adantrl ⊢b⊆TopOn⁡B∧b≠∅∧c⊆⋂b∧x∈b→x∈TopOn⁡B
7 topontop ⊢x∈TopOn⁡B→x∈Top
8 6 7 syl ⊢b⊆TopOn⁡B∧b≠∅∧c⊆⋂b∧x∈b→x∈Top
9 simpl ⊢c⊆⋂b∧x∈b→c⊆⋂b
10 intss1 ⊢x∈b→⋂b⊆x
11 10 adantl ⊢c⊆⋂b∧x∈b→⋂b⊆x
12 9 11 sstrd ⊢c⊆⋂b∧x∈b→c⊆x
13 12 adantl ⊢b⊆TopOn⁡B∧b≠∅∧c⊆⋂b∧x∈b→c⊆x
14 uniopn ⊢x∈Top∧c⊆x→⋃c∈x
15 8 13 14 syl2anc ⊢b⊆TopOn⁡B∧b≠∅∧c⊆⋂b∧x∈b→⋃c∈x
16 15 expr ⊢b⊆TopOn⁡B∧b≠∅∧c⊆⋂b→x∈b→⋃c∈x
17 16 ralrimiv ⊢b⊆TopOn⁡B∧b≠∅∧c⊆⋂b→∀x∈b⋃c∈x
18 vuniex ⊢⋃c∈V
19 18 elint2 ⊢⋃c∈⋂b↔∀x∈b⋃c∈x
20 17 19 sylibr ⊢b⊆TopOn⁡B∧b≠∅∧c⊆⋂b→⋃c∈⋂b
21 20 ex ⊢b⊆TopOn⁡B∧b≠∅→c⊆⋂b→⋃c∈⋂b
22 21 alrimiv ⊢b⊆TopOn⁡B∧b≠∅→∀cc⊆⋂b→⋃c∈⋂b
23 simpll ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b∧x∈⋂b→b⊆TopOn⁡B
24 23 sselda ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b∧x∈⋂b∧y∈b→y∈TopOn⁡B
25 topontop ⊢y∈TopOn⁡B→y∈Top
26 24 25 syl ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b∧x∈⋂b∧y∈b→y∈Top
27 intss1 ⊢y∈b→⋂b⊆y
28 27 adantl ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b∧x∈⋂b∧y∈b→⋂b⊆y
29 simplrl ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b∧x∈⋂b∧y∈b→c∈⋂b
30 28 29 sseldd ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b∧x∈⋂b∧y∈b→c∈y
31 simplrr ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b∧x∈⋂b∧y∈b→x∈⋂b
32 28 31 sseldd ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b∧x∈⋂b∧y∈b→x∈y
33 inopn ⊢y∈Top∧c∈y∧x∈y→c∩x∈y
34 26 30 32 33 syl3anc ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b∧x∈⋂b∧y∈b→c∩x∈y
35 34 ralrimiva ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b∧x∈⋂b→∀y∈bc∩x∈y
36 vex ⊢c∈V
37 36 inex1 ⊢c∩x∈V
38 37 elint2 ⊢c∩x∈⋂b↔∀y∈bc∩x∈y
39 35 38 sylibr ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b∧x∈⋂b→c∩x∈⋂b
40 39 ralrimivva ⊢b⊆TopOn⁡B∧b≠∅→∀c∈⋂b∀x∈⋂bc∩x∈⋂b
41 intex ⊢b≠∅↔⋂b∈V
42 41 biimpi ⊢b≠∅→⋂b∈V
43 42 adantl ⊢b⊆TopOn⁡B∧b≠∅→⋂b∈V
44 istopg ⊢⋂b∈V→⋂b∈Top↔∀cc⊆⋂b→⋃c∈⋂b∧∀c∈⋂b∀x∈⋂bc∩x∈⋂b
45 43 44 syl ⊢b⊆TopOn⁡B∧b≠∅→⋂b∈Top↔∀cc⊆⋂b→⋃c∈⋂b∧∀c∈⋂b∀x∈⋂bc∩x∈⋂b
46 22 40 45 mpbir2and ⊢b⊆TopOn⁡B∧b≠∅→⋂b∈Top
47 46 3adant1 ⊢B∈V∧b⊆TopOn⁡B∧b≠∅→⋂b∈Top
48 n0 ⊢b≠∅↔∃xx∈b
49 48 biimpi ⊢b≠∅→∃xx∈b
50 49 ad2antlr ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b→∃xx∈b
51 10 sselda ⊢x∈b∧c∈⋂b→c∈x
52 51 ancoms ⊢c∈⋂b∧x∈b→c∈x
53 elssuni ⊢c∈x→c⊆⋃x
54 52 53 syl ⊢c∈⋂b∧x∈b→c⊆⋃x
55 54 adantl ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b∧x∈b→c⊆⋃x
56 5 adantrl ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b∧x∈b→x∈TopOn⁡B
57 toponuni ⊢x∈TopOn⁡B→B=⋃x
58 56 57 syl ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b∧x∈b→B=⋃x
59 55 58 sseqtrrd ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b∧x∈b→c⊆B
60 59 expr ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b→x∈b→c⊆B
61 60 exlimdv ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b→∃xx∈b→c⊆B
62 50 61 mpd ⊢b⊆TopOn⁡B∧b≠∅∧c∈⋂b→c⊆B
63 62 ralrimiva ⊢b⊆TopOn⁡B∧b≠∅→∀c∈⋂bc⊆B
64 unissb ⊢⋃⋂b⊆B↔∀c∈⋂bc⊆B
65 63 64 sylibr ⊢b⊆TopOn⁡B∧b≠∅→⋃⋂b⊆B
66 65 3adant1 ⊢B∈V∧b⊆TopOn⁡B∧b≠∅→⋃⋂b⊆B
67 4 sselda ⊢b⊆TopOn⁡B∧b≠∅∧c∈b→c∈TopOn⁡B
68 toponuni ⊢c∈TopOn⁡B→B=⋃c
69 67 68 syl ⊢b⊆TopOn⁡B∧b≠∅∧c∈b→B=⋃c
70 topontop ⊢c∈TopOn⁡B→c∈Top
71 eqid ⊢⋃c=⋃c
72 71 topopn ⊢c∈Top→⋃c∈c
73 67 70 72 3syl ⊢b⊆TopOn⁡B∧b≠∅∧c∈b→⋃c∈c
74 69 73 eqeltrd ⊢b⊆TopOn⁡B∧b≠∅∧c∈b→B∈c
75 74 ralrimiva ⊢b⊆TopOn⁡B∧b≠∅→∀c∈bB∈c
76 75 3adant1 ⊢B∈V∧b⊆TopOn⁡B∧b≠∅→∀c∈bB∈c
77 elintg ⊢B∈V→B∈⋂b↔∀c∈bB∈c
78 77 3ad2ant1 ⊢B∈V∧b⊆TopOn⁡B∧b≠∅→B∈⋂b↔∀c∈bB∈c
79 76 78 mpbird ⊢B∈V∧b⊆TopOn⁡B∧b≠∅→B∈⋂b
80 unissel ⊢⋃⋂b⊆B∧B∈⋂b→⋃⋂b=B
81 66 79 80 syl2anc ⊢B∈V∧b⊆TopOn⁡B∧b≠∅→⋃⋂b=B
82 81 eqcomd ⊢B∈V∧b⊆TopOn⁡B∧b≠∅→B=⋃⋂b
83 istopon ⊢⋂b∈TopOn⁡B↔⋂b∈Top∧B=⋃⋂b
84 47 82 83 sylanbrc ⊢B∈V∧b⊆TopOn⁡B∧b≠∅→⋂b∈TopOn⁡B
85 2 3 84 ismred ⊢B∈V→TopOn⁡B∈Moore⁡𝒫B