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	$$⊢\underset{\dot{}}{\sim }=\mathrm{Fne}\cap {\mathrm{Fne}}^{-1}$$
Assertion	topfneec	$$⊢J\in \mathrm{Top}\to \left(A\in \left[J\right]\underset{\dot{}}{\sim }\leftrightarrow \mathrm{topGen}\left(A\right)=J\right)$$

Proof

Step	Hyp	Ref	Expression
1		topfneec.1	$$⊢\underset{\dot{}}{\sim }=\mathrm{Fne}\cap {\mathrm{Fne}}^{-1}$$
2	1	fneer	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}\mathrm{V}$$
3		errel	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}\mathrm{V}\to \mathrm{Rel}\underset{\dot{}}{\sim }$$
4	2 3	ax-mp	$$⊢\mathrm{Rel}\underset{\dot{}}{\sim }$$
5		relelec	$$⊢\mathrm{Rel}\underset{\dot{}}{\sim }\to \left(A\in \left[J\right]\underset{\dot{}}{\sim }\leftrightarrow J\underset{\dot{}}{\sim }A\right)$$
6	4 5	ax-mp	$$⊢A\in \left[J\right]\underset{\dot{}}{\sim }\leftrightarrow J\underset{\dot{}}{\sim }A$$
7	4	brrelex2i	$$⊢J\underset{\dot{}}{\sim }A\to A\in \mathrm{V}$$
8	7	a1i	$$⊢J\in \mathrm{Top}\to \left(J\underset{\dot{}}{\sim }A\to A\in \mathrm{V}\right)$$
9		eleq1	$$⊢\mathrm{topGen}\left(A\right)=J\to \left(\mathrm{topGen}\left(A\right)\in \mathrm{Top}\leftrightarrow 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}\leftrightarrow \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	$$⊢\left(J\in \mathrm{Top}\wedge A\in \mathrm{V}\right)\to \left(J\underset{\dot{}}{\sim }A\leftrightarrow \mathrm{topGen}\left(J\right)=\mathrm{topGen}\left(A\right)\right)$$
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)\leftrightarrow J=\mathrm{topGen}\left(A\right)\right)$$
19		eqcom	$$⊢J=\mathrm{topGen}\left(A\right)\leftrightarrow \mathrm{topGen}\left(A\right)=J$$
20	18 19	bitrdi	$$⊢J\in \mathrm{Top}\to \left(\mathrm{topGen}\left(J\right)=\mathrm{topGen}\left(A\right)\leftrightarrow \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)\leftrightarrow \mathrm{topGen}\left(A\right)=J\right)$$
22	16 21	bitrd	$$⊢\left(J\in \mathrm{Top}\wedge A\in \mathrm{V}\right)\to \left(J\underset{\dot{}}{\sim }A\leftrightarrow \mathrm{topGen}\left(A\right)=J\right)$$
23	22	ex	$$⊢J\in \mathrm{Top}\to \left(A\in \mathrm{V}\to \left(J\underset{\dot{}}{\sim }A\leftrightarrow \mathrm{topGen}\left(A\right)=J\right)\right)$$
24	8 15 23	pm5.21ndd	$$⊢J\in \mathrm{Top}\to \left(J\underset{\dot{}}{\sim }A\leftrightarrow \mathrm{topGen}\left(A\right)=J\right)$$
25	6 24	bitrid	$$⊢J\in \mathrm{Top}\to \left(A\in \left[J\right]\underset{\dot{}}{\sim }\leftrightarrow \mathrm{topGen}\left(A\right)=J\right)$$