Metamath Proof Explorer

Theorem istopon

Description: Property of being a topology with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015) (Revised by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion istopon 
|- ( J e. ( TopOn ` B ) <-> ( J e. Top /\ B = U. J ) )

Proof

Step Hyp Ref Expression
1 elfvex 
 |-  ( J e. ( TopOn ` B ) -> B e. _V )
2 uniexg 
 |-  ( J e. Top -> U. J e. _V )
3 eleq1 
 |-  ( B = U. J -> ( B e. _V <-> U. J e. _V ) )
4 2 3 syl5ibrcom 
 |-  ( J e. Top -> ( B = U. J -> B e. _V ) )
5 4 imp 
 |-  ( ( J e. Top /\ B = U. J ) -> B e. _V )
6 eqeq1 
 |-  ( b = B -> ( b = U. j <-> B = U. j ) )
7 6 rabbidv 
 |-  ( b = B -> { j e. Top | b = U. j } = { j e. Top | B = U. j } )
8 df-topon 
 |-  TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
9 vpwex 
 |-  ~P b e. _V
10 9 pwex 
 |-  ~P ~P b e. _V
11 rabss 
 |-  ( { j e. Top | b = U. j } C_ ~P ~P b <-> A. j e. Top ( b = U. j -> j e. ~P ~P b ) )
12 pwuni 
 |-  j C_ ~P U. j
13 pweq 
 |-  ( b = U. j -> ~P b = ~P U. j )
14 12 13 sseqtrrid 
 |-  ( b = U. j -> j C_ ~P b )
15 velpw 
 |-  ( j e. ~P ~P b <-> j C_ ~P b )
16 14 15 sylibr 
 |-  ( b = U. j -> j e. ~P ~P b )
17 16 a1i 
 |-  ( j e. Top -> ( b = U. j -> j e. ~P ~P b ) )
18 11 17 mprgbir 
 |-  { j e. Top | b = U. j } C_ ~P ~P b
19 10 18 ssexi 
 |-  { j e. Top | b = U. j } e. _V
20 7 8 19 fvmpt3i 
 |-  ( B e. _V -> ( TopOn ` B ) = { j e. Top | B = U. j } )
21 20 eleq2d 
 |-  ( B e. _V -> ( J e. ( TopOn ` B ) <-> J e. { j e. Top | B = U. j } ) )
22 unieq 
 |-  ( j = J -> U. j = U. J )
23 22 eqeq2d 
 |-  ( j = J -> ( B = U. j <-> B = U. J ) )
24 23 elrab 
 |-  ( J e. { j e. Top | B = U. j } <-> ( J e. Top /\ B = U. J ) )
25 21 24 bitrdi 
 |-  ( B e. _V -> ( J e. ( TopOn ` B ) <-> ( J e. Top /\ B = U. J ) ) )
26 1 5 25 pm5.21nii 
 |-  ( J e. ( TopOn ` B ) <-> ( J e. Top /\ B = U. J ) )