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 ( 𝐵 ∈ 𝑉 → ( TopOn ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) )

Proof

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