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 ∩ Fne -1
Assertion topfneec ⊢ J ∈ Top → A ∈ J ∼ ˙ ↔ topGen ⁡ A = J

Proof

Step Hyp Ref Expression
1 topfneec.1 ⊢ ∼ ˙ = Fne ∩ Fne -1
2 1 fneer ⊢ ∼ ˙ Er V
3 errel ⊢ ∼ ˙ Er V → Rel ⁡ ∼ ˙
4 2 3 ax-mp ⊢ Rel ⁡ ∼ ˙
5 relelec ⊢ Rel ⁡ ∼ ˙ → A ∈ J ∼ ˙ ↔ J ∼ ˙ A
6 4 5 ax-mp ⊢ A ∈ J ∼ ˙ ↔ J ∼ ˙ A
7 4 brrelex2i ⊢ J ∼ ˙ A → A ∈ V
8 7 a1i ⊢ J ∈ Top → J ∼ ˙ A → A ∈ V
9 eleq1 ⊢ topGen ⁡ A = J → topGen ⁡ A ∈ Top ↔ J ∈ Top
10 9 biimparc ⊢ J ∈ Top ∧ topGen ⁡ A = J → topGen ⁡ A ∈ Top
11 tgclb ⊢ A ∈ TopBases ↔ topGen ⁡ A ∈ Top
12 10 11 sylibr ⊢ J ∈ Top ∧ topGen ⁡ A = J → A ∈ TopBases
13 elex ⊢ A ∈ TopBases → A ∈ V
14 12 13 syl ⊢ J ∈ Top ∧ topGen ⁡ A = J → A ∈ V
15 14 ex ⊢ J ∈ Top → topGen ⁡ A = J → A ∈ V
16 1 fneval ⊢ J ∈ Top ∧ A ∈ V → J ∼ ˙ A ↔ topGen ⁡ J = topGen ⁡ A
17 tgtop ⊢ J ∈ Top → topGen ⁡ J = J
18 17 eqeq1d ⊢ J ∈ Top → topGen ⁡ J = topGen ⁡ A ↔ J = topGen ⁡ A
19 eqcom ⊢ J = topGen ⁡ A ↔ topGen ⁡ A = J
20 18 19 bitrdi ⊢ J ∈ Top → topGen ⁡ J = topGen ⁡ A ↔ topGen ⁡ A = J
21 20 adantr ⊢ J ∈ Top ∧ A ∈ V → topGen ⁡ J = topGen ⁡ A ↔ topGen ⁡ A = J
22 16 21 bitrd ⊢ J ∈ Top ∧ A ∈ V → J ∼ ˙ A ↔ topGen ⁡ A = J
23 22 ex ⊢ J ∈ Top → A ∈ V → J ∼ ˙ A ↔ topGen ⁡ A = J
24 8 15 23 pm5.21ndd ⊢ J ∈ Top → J ∼ ˙ A ↔ topGen ⁡ A = J
25 6 24 bitrid ⊢ J ∈ Top → A ∈ J ∼ ˙ ↔ topGen ⁡ A = J