Metamath Proof Explorer

Theorem topmeet

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

Ref Expression
Assertion topmeet 
|- ( ( X e. V /\ S C_ ( TopOn ` X ) ) -> ( ~P X i^i |^| S ) = U. { k e. ( TopOn ` X ) | A. j e. S k C_ j } )

Proof

Step Hyp Ref Expression
1 topmtcl 
 |-  ( ( X e. V /\ S C_ ( TopOn ` X ) ) -> ( ~P X i^i |^| S ) e. ( TopOn ` X ) )
2 inss2 
 |-  ( ~P X i^i |^| S ) C_ |^| S
3 intss1 
 |-  ( j e. S -> |^| S C_ j )
4 2 3 sstrid 
 |-  ( j e. S -> ( ~P X i^i |^| S ) C_ j )
5 4 rgen 
 |-  A. j e. S ( ~P X i^i |^| S ) C_ j
6 sseq1 
 |-  ( k = ( ~P X i^i |^| S ) -> ( k C_ j <-> ( ~P X i^i |^| S ) C_ j ) )
7 6 ralbidv 
 |-  ( k = ( ~P X i^i |^| S ) -> ( A. j e. S k C_ j <-> A. j e. S ( ~P X i^i |^| S ) C_ j ) )
8 7 elrab 
 |-  ( ( ~P X i^i |^| S ) e. { k e. ( TopOn ` X ) | A. j e. S k C_ j } <-> ( ( ~P X i^i |^| S ) e. ( TopOn ` X ) /\ A. j e. S ( ~P X i^i |^| S ) C_ j ) )
9 5 8 mpbiran2 
 |-  ( ( ~P X i^i |^| S ) e. { k e. ( TopOn ` X ) | A. j e. S k C_ j } <-> ( ~P X i^i |^| S ) e. ( TopOn ` X ) )
10 1 9 sylibr 
 |-  ( ( X e. V /\ S C_ ( TopOn ` X ) ) -> ( ~P X i^i |^| S ) e. { k e. ( TopOn ` X ) | A. j e. S k C_ j } )
11 elssuni 
 |-  ( ( ~P X i^i |^| S ) e. { k e. ( TopOn ` X ) | A. j e. S k C_ j } -> ( ~P X i^i |^| S ) C_ U. { k e. ( TopOn ` X ) | A. j e. S k C_ j } )
12 10 11 syl 
 |-  ( ( X e. V /\ S C_ ( TopOn ` X ) ) -> ( ~P X i^i |^| S ) C_ U. { k e. ( TopOn ` X ) | A. j e. S k C_ j } )
13 toponuni 
 |-  ( k e. ( TopOn ` X ) -> X = U. k )
14 eqimss2 
 |-  ( X = U. k -> U. k C_ X )
15 13 14 syl 
 |-  ( k e. ( TopOn ` X ) -> U. k C_ X )
16 sspwuni 
 |-  ( k C_ ~P X <-> U. k C_ X )
17 15 16 sylibr 
 |-  ( k e. ( TopOn ` X ) -> k C_ ~P X )
18 17 3ad2ant2 
 |-  ( ( ( X e. V /\ S C_ ( TopOn ` X ) ) /\ k e. ( TopOn ` X ) /\ A. j e. S k C_ j ) -> k C_ ~P X )
19 simp3 
 |-  ( ( ( X e. V /\ S C_ ( TopOn ` X ) ) /\ k e. ( TopOn ` X ) /\ A. j e. S k C_ j ) -> A. j e. S k C_ j )
20 ssint 
 |-  ( k C_ |^| S <-> A. j e. S k C_ j )
21 19 20 sylibr 
 |-  ( ( ( X e. V /\ S C_ ( TopOn ` X ) ) /\ k e. ( TopOn ` X ) /\ A. j e. S k C_ j ) -> k C_ |^| S )
22 18 21 ssind 
 |-  ( ( ( X e. V /\ S C_ ( TopOn ` X ) ) /\ k e. ( TopOn ` X ) /\ A. j e. S k C_ j ) -> k C_ ( ~P X i^i |^| S ) )
23 velpw 
 |-  ( k e. ~P ( ~P X i^i |^| S ) <-> k C_ ( ~P X i^i |^| S ) )
24 22 23 sylibr 
 |-  ( ( ( X e. V /\ S C_ ( TopOn ` X ) ) /\ k e. ( TopOn ` X ) /\ A. j e. S k C_ j ) -> k e. ~P ( ~P X i^i |^| S ) )
25 24 rabssdv 
 |-  ( ( X e. V /\ S C_ ( TopOn ` X ) ) -> { k e. ( TopOn ` X ) | A. j e. S k C_ j } C_ ~P ( ~P X i^i |^| S ) )
26 sspwuni 
 |-  ( { k e. ( TopOn ` X ) | A. j e. S k C_ j } C_ ~P ( ~P X i^i |^| S ) <-> U. { k e. ( TopOn ` X ) | A. j e. S k C_ j } C_ ( ~P X i^i |^| S ) )
27 25 26 sylib 
 |-  ( ( X e. V /\ S C_ ( TopOn ` X ) ) -> U. { k e. ( TopOn ` X ) | A. j e. S k C_ j } C_ ( ~P X i^i |^| S ) )
28 12 27 eqssd 
 |-  ( ( X e. V /\ S C_ ( TopOn ` X ) ) -> ( ~P X i^i |^| S ) = U. { k e. ( TopOn ` X ) | A. j e. S k C_ j } )