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 ( ( 𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ ( TopOn ‘ 𝑋 ) ) → ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ∪ 𝑆 ) ) ) = ∩ { 𝑘 ∈ ( TopOn ‘ 𝑋 ) ∣ ∀ 𝑗 ∈ 𝑆 𝑗 ⊆ 𝑘 } )

Proof

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