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 ≠ ∅ → ∀ c c ⊆ ⋂ 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 ∈ b c ∩ x ∈ y
36 vex ⊢ c ∈ V
37 36 inex1 ⊢ c ∩ x ∈ V
38 37 elint2 ⊢ c ∩ x ∈ ⋂ b ↔ ∀ y ∈ b c ∩ 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 ∈ ⋂ b c ∩ 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 ↔ ∀ c c ⊆ ⋂ b → ⋃ c ∈ ⋂ b ∧ ∀ c ∈ ⋂ b ∀ x ∈ ⋂ b c ∩ x ∈ ⋂ b
45 43 44 syl ⊢ b ⊆ TopOn ⁡ B ∧ b ≠ ∅ → ⋂ b ∈ Top ↔ ∀ c c ⊆ ⋂ b → ⋃ c ∈ ⋂ b ∧ ∀ c ∈ ⋂ b ∀ x ∈ ⋂ b c ∩ 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 ≠ ∅ ↔ ∃ x x ∈ b
49 48 biimpi ⊢ b ≠ ∅ → ∃ x x ∈ b
50 49 ad2antlr ⊢ b ⊆ TopOn ⁡ B ∧ b ≠ ∅ ∧ c ∈ ⋂ b → ∃ x x ∈ 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 → ∃ x x ∈ b → c ⊆ B
62 50 61 mpd ⊢ b ⊆ TopOn ⁡ B ∧ b ≠ ∅ ∧ c ∈ ⋂ b → c ⊆ B
63 62 ralrimiva ⊢ b ⊆ TopOn ⁡ B ∧ b ≠ ∅ → ∀ c ∈ ⋂ b c ⊆ B
64 unissb ⊢ ⋃ ⋂ b ⊆ B ↔ ∀ c ∈ ⋂ b c ⊆ 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 ∈ b B ∈ c
76 75 3adant1 ⊢ B ∈ V ∧ b ⊆ TopOn ⁡ B ∧ b ≠ ∅ → ∀ c ∈ b B ∈ c
77 elintg ⊢ B ∈ V → B ∈ ⋂ b ↔ ∀ c ∈ b B ∈ c
78 77 3ad2ant1 ⊢ B ∈ V ∧ b ⊆ TopOn ⁡ B ∧ b ≠ ∅ → B ∈ ⋂ b ↔ ∀ c ∈ b B ∈ 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