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 ) )