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 e. V /\ S C_ ( TopOn ` X ) ) -> ( topGen ` ( fi ` ( { X } u. U. S ) ) ) = |^| { k e. ( TopOn ` X ) | A. j e. S j C_ k } )

Proof

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