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∈Sj⊆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∈Sj⊆k→k∈Top
3 toponmax ⊢k∈TopOn⁡X→X∈k
4 3 ad2antrl ⊢X∈V∧S⊆TopOn⁡X∧k∈TopOn⁡X∧∀j∈Sj⊆k→X∈k
5 4 snssd ⊢X∈V∧S⊆TopOn⁡X∧k∈TopOn⁡X∧∀j∈Sj⊆k→X⊆k
6 simprr ⊢X∈V∧S⊆TopOn⁡X∧k∈TopOn⁡X∧∀j∈Sj⊆k→∀j∈Sj⊆k
7 unissb ⊢⋃S⊆k↔∀j∈Sj⊆k
8 6 7 sylibr ⊢X∈V∧S⊆TopOn⁡X∧k∈TopOn⁡X∧∀j∈Sj⊆k→⋃S⊆k
9 5 8 unssd ⊢X∈V∧S⊆TopOn⁡X∧k∈TopOn⁡X∧∀j∈Sj⊆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∈Sj⊆k→topGen⁡fi⁡X∪⋃S⊆k
12 11 expr ⊢X∈V∧S⊆TopOn⁡X∧k∈TopOn⁡X→∀j∈Sj⊆k→topGen⁡fi⁡X∪⋃S⊆k
13 12 ralrimiva ⊢X∈V∧S⊆TopOn⁡X→∀k∈TopOn⁡X∀j∈Sj⊆k→topGen⁡fi⁡X∪⋃S⊆k
14 ssintrab ⊢topGen⁡fi⁡X∪⋃S⊆⋂k∈TopOn⁡X|∀j∈Sj⊆k↔∀k∈TopOn⁡X∀j∈Sj⊆k→topGen⁡fi⁡X∪⋃S⊆k
15 13 14 sylibr ⊢X∈V∧S⊆TopOn⁡X→topGen⁡fi⁡X∪⋃S⊆⋂k∈TopOn⁡X|∀j∈Sj⊆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∈Sj⊆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∈Sj⊆k↔∀j∈Sj⊆topGen⁡fi⁡X∪⋃S
64 63 elrab ⊢topGen⁡fi⁡X∪⋃S∈k∈TopOn⁡X|∀j∈Sj⊆k↔topGen⁡fi⁡X∪⋃S∈TopOn⁡X∧∀j∈Sj⊆topGen⁡fi⁡X∪⋃S
65 51 61 64 sylanbrc ⊢X∈V∧S⊆TopOn⁡X→topGen⁡fi⁡X∪⋃S∈k∈TopOn⁡X|∀j∈Sj⊆k
66 intss1 ⊢topGen⁡fi⁡X∪⋃S∈k∈TopOn⁡X|∀j∈Sj⊆k→⋂k∈TopOn⁡X|∀j∈Sj⊆k⊆topGen⁡fi⁡X∪⋃S
67 65 66 syl ⊢X∈V∧S⊆TopOn⁡X→⋂k∈TopOn⁡X|∀j∈Sj⊆k⊆topGen⁡fi⁡X∪⋃S
68 15 67 eqssd ⊢X∈V∧S⊆TopOn⁡X→topGen⁡fi⁡X∪⋃S=⋂k∈TopOn⁡X|∀j∈Sj⊆k