# 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
Assertion topfneec

### Proof

Step Hyp Ref Expression
1 topfneec.1
2 1 fneer
3 errel
4 2 3 ax-mp
5 relelec
6 4 5 ax-mp
7 4 brrelex2i
8 7 a1i
9 eleq1 ${⊢}\mathrm{topGen}\left({A}\right)={J}\to \left(\mathrm{topGen}\left({A}\right)\in \mathrm{Top}↔{J}\in \mathrm{Top}\right)$
10 9 biimparc ${⊢}\left({J}\in \mathrm{Top}\wedge \mathrm{topGen}\left({A}\right)={J}\right)\to \mathrm{topGen}\left({A}\right)\in \mathrm{Top}$
11 tgclb ${⊢}{A}\in \mathrm{TopBases}↔\mathrm{topGen}\left({A}\right)\in \mathrm{Top}$
12 10 11 sylibr ${⊢}\left({J}\in \mathrm{Top}\wedge \mathrm{topGen}\left({A}\right)={J}\right)\to {A}\in \mathrm{TopBases}$
13 elex ${⊢}{A}\in \mathrm{TopBases}\to {A}\in \mathrm{V}$
14 12 13 syl ${⊢}\left({J}\in \mathrm{Top}\wedge \mathrm{topGen}\left({A}\right)={J}\right)\to {A}\in \mathrm{V}$
15 14 ex ${⊢}{J}\in \mathrm{Top}\to \left(\mathrm{topGen}\left({A}\right)={J}\to {A}\in \mathrm{V}\right)$
16 1 fneval
17 tgtop ${⊢}{J}\in \mathrm{Top}\to \mathrm{topGen}\left({J}\right)={J}$
18 17 eqeq1d ${⊢}{J}\in \mathrm{Top}\to \left(\mathrm{topGen}\left({J}\right)=\mathrm{topGen}\left({A}\right)↔{J}=\mathrm{topGen}\left({A}\right)\right)$
19 eqcom ${⊢}{J}=\mathrm{topGen}\left({A}\right)↔\mathrm{topGen}\left({A}\right)={J}$
20 18 19 syl6bb ${⊢}{J}\in \mathrm{Top}\to \left(\mathrm{topGen}\left({J}\right)=\mathrm{topGen}\left({A}\right)↔\mathrm{topGen}\left({A}\right)={J}\right)$
21 20 adantr ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\in \mathrm{V}\right)\to \left(\mathrm{topGen}\left({J}\right)=\mathrm{topGen}\left({A}\right)↔\mathrm{topGen}\left({A}\right)={J}\right)$
22 16 21 bitrd
23 22 ex
24 8 15 23 pm5.21ndd
25 6 24 syl5bb