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