# 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 syl6bb
|-  ( 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 ) )