Metamath Proof Explorer

Theorem topfneec

Description: A cover is equivalent to a topology iff it is a base for that topology. (Contributed by Jeff Hankins, 8-Oct-2009) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypothesis topfneec.1 
|- .~ = ( Fne i^i `' Fne )
Assertion topfneec 
|- ( J e. Top -> ( A e. [ J ] .~ <-> ( topGen ` A ) = J ) )

Proof

Step Hyp Ref Expression
1 topfneec.1 
 |-  .~ = ( Fne i^i `' Fne )
2 1 fneer 
 |-  .~ Er _V
3 errel 
 |-  ( .~ Er _V -> Rel .~ )
4 2 3 ax-mp 
 |-  Rel .~
5 relelec 
 |-  ( Rel .~ -> ( A e. [ J ] .~ <-> J .~ A ) )
6 4 5 ax-mp 
 |-  ( A e. [ J ] .~ <-> J .~ A )
7 4 brrelex2i 
 |-  ( J .~ A -> A e. _V )
8 7 a1i 
 |-  ( J e. Top -> ( J .~ A -> A e. _V ) )
9 eleq1 
 |-  ( ( topGen ` A ) = J -> ( ( topGen ` A ) e. Top <-> J e. Top ) )
10 9 biimparc 
 |-  ( ( J e. Top /\ ( topGen ` A ) = J ) -> ( topGen ` A ) e. Top )
11 tgclb 
 |-  ( A e. TopBases <-> ( topGen ` A ) e. Top )
12 10 11 sylibr 
 |-  ( ( J e. Top /\ ( topGen ` A ) = J ) -> A e. TopBases )
13 elex 
 |-  ( A e. TopBases -> A e. _V )
14 12 13 syl 
 |-  ( ( J e. Top /\ ( topGen ` A ) = J ) -> A e. _V )
15 14 ex 
 |-  ( J e. Top -> ( ( topGen ` A ) = J -> A e. _V ) )
16 1 fneval 
 |-  ( ( J e. Top /\ A e. _V ) -> ( J .~ A <-> ( topGen ` J ) = ( topGen ` A ) ) )
17 tgtop 
 |-  ( J e. Top -> ( topGen ` J ) = J )
18 17 eqeq1d 
 |-  ( J e. Top -> ( ( topGen ` J ) = ( topGen ` A ) <-> J = ( topGen ` A ) ) )
19 eqcom 
 |-  ( J = ( topGen ` A ) <-> ( topGen ` A ) = J )
20 18 19 bitrdi 
 |-  ( J e. Top -> ( ( topGen ` J ) = ( topGen ` A ) <-> ( topGen ` A ) = J ) )
21 20 adantr 
 |-  ( ( J e. Top /\ A e. _V ) -> ( ( topGen ` J ) = ( topGen ` A ) <-> ( topGen ` A ) = J ) )
22 16 21 bitrd 
 |-  ( ( J e. Top /\ A e. _V ) -> ( J .~ A <-> ( topGen ` A ) = J ) )
23 22 ex 
 |-  ( J e. Top -> ( A e. _V -> ( J .~ A <-> ( topGen ` A ) = J ) ) )
24 8 15 23 pm5.21ndd 
 |-  ( J e. Top -> ( J .~ A <-> ( topGen ` A ) = J ) )
25 6 24 bitrid 
 |-  ( J e. Top -> ( A e. [ J ] .~ <-> ( topGen ` A ) = J ) )