This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )
Assertion topfneec ( 𝐽 ∈ Top → ( 𝐴 ∈ [ 𝐽 ] ∼ ↔ ( topGen ‘ 𝐴 ) = 𝐽 ) )

Proof

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