Metamath Proof Explorer

Theorem topjoin

Description: Two equivalent formulations of the join of a collection of topologies. (Contributed by Jeff Hankins, 6-Oct-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion topjoin ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → topGen ⁡ fi ⁡ X ∪ ⋃ S = ⋂ k ∈ TopOn ⁡ X | ∀ j ∈ S j ⊆ k

Proof

Step Hyp Ref Expression
1 topontop ⊢ k ∈ TopOn ⁡ X → k ∈ Top
2 1 ad2antrl ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X ∧ k ∈ TopOn ⁡ X ∧ ∀ j ∈ S j ⊆ k → k ∈ Top
3 toponmax ⊢ k ∈ TopOn ⁡ X → X ∈ k
4 3 ad2antrl ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X ∧ k ∈ TopOn ⁡ X ∧ ∀ j ∈ S j ⊆ k → X ∈ k
5 4 snssd ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X ∧ k ∈ TopOn ⁡ X ∧ ∀ j ∈ S j ⊆ k → X ⊆ k
6 simprr ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X ∧ k ∈ TopOn ⁡ X ∧ ∀ j ∈ S j ⊆ k → ∀ j ∈ S j ⊆ k
7 unissb ⊢ ⋃ S ⊆ k ↔ ∀ j ∈ S j ⊆ k
8 6 7 sylibr ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X ∧ k ∈ TopOn ⁡ X ∧ ∀ j ∈ S j ⊆ k → ⋃ S ⊆ k
9 5 8 unssd ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X ∧ k ∈ TopOn ⁡ X ∧ ∀ j ∈ S j ⊆ k → X ∪ ⋃ S ⊆ k
10 tgfiss ⊢ k ∈ Top ∧ X ∪ ⋃ S ⊆ k → topGen ⁡ fi ⁡ X ∪ ⋃ S ⊆ k
11 2 9 10 syl2anc ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X ∧ k ∈ TopOn ⁡ X ∧ ∀ j ∈ S j ⊆ k → topGen ⁡ fi ⁡ X ∪ ⋃ S ⊆ k
12 11 expr ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X ∧ k ∈ TopOn ⁡ X → ∀ j ∈ S j ⊆ k → topGen ⁡ fi ⁡ X ∪ ⋃ S ⊆ k
13 12 ralrimiva ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → ∀ k ∈ TopOn ⁡ X ∀ j ∈ S j ⊆ k → topGen ⁡ fi ⁡ X ∪ ⋃ S ⊆ k
14 ssintrab ⊢ topGen ⁡ fi ⁡ X ∪ ⋃ S ⊆ ⋂ k ∈ TopOn ⁡ X | ∀ j ∈ S j ⊆ k ↔ ∀ k ∈ TopOn ⁡ X ∀ j ∈ S j ⊆ k → topGen ⁡ fi ⁡ X ∪ ⋃ S ⊆ k
15 13 14 sylibr ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → topGen ⁡ fi ⁡ X ∪ ⋃ S ⊆ ⋂ k ∈ TopOn ⁡ X | ∀ j ∈ S j ⊆ k
16 fibas ⊢ fi ⁡ X ∪ ⋃ S ∈ TopBases
17 tgtopon ⊢ fi ⁡ X ∪ ⋃ S ∈ TopBases → topGen ⁡ fi ⁡ X ∪ ⋃ S ∈ TopOn ⁡ ⋃ fi ⁡ X ∪ ⋃ S
18 16 17 ax-mp ⊢ topGen ⁡ fi ⁡ X ∪ ⋃ S ∈ TopOn ⁡ ⋃ fi ⁡ X ∪ ⋃ S
19 uniun ⊢ ⋃ X ∪ ⋃ S = ⋃ X ∪ ⋃ ⋃ S
20 unisng ⊢ X ∈ V → ⋃ X = X
21 20 adantr ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → ⋃ X = X
22 21 uneq1d ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → ⋃ X ∪ ⋃ ⋃ S = X ∪ ⋃ ⋃ S
23 19 22 eqtr2id ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → X ∪ ⋃ ⋃ S = ⋃ X ∪ ⋃ S
24 simpr ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → S ⊆ TopOn ⁡ X
25 toponuni ⊢ k ∈ TopOn ⁡ X → X = ⋃ k
26 eqimss2 ⊢ X = ⋃ k → ⋃ k ⊆ X
27 25 26 syl ⊢ k ∈ TopOn ⁡ X → ⋃ k ⊆ X
28 sspwuni ⊢ k ⊆ 𝒫 X ↔ ⋃ k ⊆ X
29 27 28 sylibr ⊢ k ∈ TopOn ⁡ X → k ⊆ 𝒫 X
30 velpw ⊢ k ∈ 𝒫 𝒫 X ↔ k ⊆ 𝒫 X
31 29 30 sylibr ⊢ k ∈ TopOn ⁡ X → k ∈ 𝒫 𝒫 X
32 31 ssriv ⊢ TopOn ⁡ X ⊆ 𝒫 𝒫 X
33 24 32 sstrdi ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → S ⊆ 𝒫 𝒫 X
34 sspwuni ⊢ S ⊆ 𝒫 𝒫 X ↔ ⋃ S ⊆ 𝒫 X
35 33 34 sylib ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → ⋃ S ⊆ 𝒫 X
36 sspwuni ⊢ ⋃ S ⊆ 𝒫 X ↔ ⋃ ⋃ S ⊆ X
37 35 36 sylib ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → ⋃ ⋃ S ⊆ X
38 ssequn2 ⊢ ⋃ ⋃ S ⊆ X ↔ X ∪ ⋃ ⋃ S = X
39 37 38 sylib ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → X ∪ ⋃ ⋃ S = X
40 snex ⊢ X ∈ V
41 fvex ⊢ TopOn ⁡ X ∈ V
42 41 ssex ⊢ S ⊆ TopOn ⁡ X → S ∈ V
43 42 adantl ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → S ∈ V
44 43 uniexd ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → ⋃ S ∈ V
45 unexg ⊢ X ∈ V ∧ ⋃ S ∈ V → X ∪ ⋃ S ∈ V
46 40 44 45 sylancr ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → X ∪ ⋃ S ∈ V
47 fiuni ⊢ X ∪ ⋃ S ∈ V → ⋃ X ∪ ⋃ S = ⋃ fi ⁡ X ∪ ⋃ S
48 46 47 syl ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → ⋃ X ∪ ⋃ S = ⋃ fi ⁡ X ∪ ⋃ S
49 23 39 48 3eqtr3d ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → X = ⋃ fi ⁡ X ∪ ⋃ S
50 49 fveq2d ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → TopOn ⁡ X = TopOn ⁡ ⋃ fi ⁡ X ∪ ⋃ S
51 18 50 eleqtrrid ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → topGen ⁡ fi ⁡ X ∪ ⋃ S ∈ TopOn ⁡ X
52 elssuni ⊢ j ∈ S → j ⊆ ⋃ S
53 ssun2 ⊢ ⋃ S ⊆ X ∪ ⋃ S
54 52 53 sstrdi ⊢ j ∈ S → j ⊆ X ∪ ⋃ S
55 ssfii ⊢ X ∪ ⋃ S ∈ V → X ∪ ⋃ S ⊆ fi ⁡ X ∪ ⋃ S
56 46 55 syl ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → X ∪ ⋃ S ⊆ fi ⁡ X ∪ ⋃ S
57 54 56 sylan9ssr ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X ∧ j ∈ S → j ⊆ fi ⁡ X ∪ ⋃ S
58 bastg ⊢ fi ⁡ X ∪ ⋃ S ∈ TopBases → fi ⁡ X ∪ ⋃ S ⊆ topGen ⁡ fi ⁡ X ∪ ⋃ S
59 16 58 ax-mp ⊢ fi ⁡ X ∪ ⋃ S ⊆ topGen ⁡ fi ⁡ X ∪ ⋃ S
60 57 59 sstrdi ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X ∧ j ∈ S → j ⊆ topGen ⁡ fi ⁡ X ∪ ⋃ S
61 60 ralrimiva ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → ∀ j ∈ S j ⊆ topGen ⁡ fi ⁡ X ∪ ⋃ S
62 sseq2 ⊢ k = topGen ⁡ fi ⁡ X ∪ ⋃ S → j ⊆ k ↔ j ⊆ topGen ⁡ fi ⁡ X ∪ ⋃ S
63 62 ralbidv ⊢ k = topGen ⁡ fi ⁡ X ∪ ⋃ S → ∀ j ∈ S j ⊆ k ↔ ∀ j ∈ S j ⊆ topGen ⁡ fi ⁡ X ∪ ⋃ S
64 63 elrab ⊢ topGen ⁡ fi ⁡ X ∪ ⋃ S ∈ k ∈ TopOn ⁡ X | ∀ j ∈ S j ⊆ k ↔ topGen ⁡ fi ⁡ X ∪ ⋃ S ∈ TopOn ⁡ X ∧ ∀ j ∈ S j ⊆ topGen ⁡ fi ⁡ X ∪ ⋃ S
65 51 61 64 sylanbrc ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → topGen ⁡ fi ⁡ X ∪ ⋃ S ∈ k ∈ TopOn ⁡ X | ∀ j ∈ S j ⊆ k
66 intss1 ⊢ topGen ⁡ fi ⁡ X ∪ ⋃ S ∈ k ∈ TopOn ⁡ X | ∀ j ∈ S j ⊆ k → ⋂ k ∈ TopOn ⁡ X | ∀ j ∈ S j ⊆ k ⊆ topGen ⁡ fi ⁡ X ∪ ⋃ S
67 65 66 syl ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → ⋂ k ∈ TopOn ⁡ X | ∀ j ∈ S j ⊆ k ⊆ topGen ⁡ fi ⁡ X ∪ ⋃ S
68 15 67 eqssd ⊢ X ∈ V ∧ S ⊆ TopOn ⁡ X → topGen ⁡ fi ⁡ X ∪ ⋃ S = ⋂ k ∈ TopOn ⁡ X | ∀ j ∈ S j ⊆ k