Theorem topfneec2

Description: A topology is precisely identified with its equivalence class. (Contributed by Jeff Hankins, 12-Oct-2009)

	Ref	Expression
Hypothesis	topfneec2.1	$$⊢\underset{\dot{}}{\sim }=\mathrm{Fne}\cap {\mathrm{Fne}}^{-1}$$
Assertion	topfneec2	$$⊢\left(J\in \mathrm{Top}\wedge K\in \mathrm{Top}\right)\to \left(\left[J\right]\underset{\dot{}}{\sim }=\left[K\right]\underset{\dot{}}{\sim }\leftrightarrow J=K\right)$$

Proof

Step	Hyp	Ref	Expression
1		topfneec2.1	$$⊢\underset{\dot{}}{\sim }=\mathrm{Fne}\cap {\mathrm{Fne}}^{-1}$$
2	1	fneval	$$⊢\left(J\in \mathrm{Top}\wedge K\in \mathrm{Top}\right)\to \left(J\underset{\dot{}}{\sim }K\leftrightarrow \mathrm{topGen}\left(J\right)=\mathrm{topGen}\left(K\right)\right)$$
3	1	fneer	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}\mathrm{V}$$
4	3	a1i	$$⊢\left(J\in \mathrm{Top}\wedge K\in \mathrm{Top}\right)\to \underset{\dot{}}{\sim }\mathrm{Er}\mathrm{V}$$
5		elex	$$⊢J\in \mathrm{Top}\to J\in \mathrm{V}$$
6	5	adantr	$$⊢\left(J\in \mathrm{Top}\wedge K\in \mathrm{Top}\right)\to J\in \mathrm{V}$$
7	4 6	erth	$$⊢\left(J\in \mathrm{Top}\wedge K\in \mathrm{Top}\right)\to \left(J\underset{\dot{}}{\sim }K\leftrightarrow \left[J\right]\underset{\dot{}}{\sim }=\left[K\right]\underset{\dot{}}{\sim }\right)$$
8		tgtop	$$⊢J\in \mathrm{Top}\to \mathrm{topGen}\left(J\right)=J$$
9		tgtop	$$⊢K\in \mathrm{Top}\to \mathrm{topGen}\left(K\right)=K$$
10	8 9	eqeqan12d	$$⊢\left(J\in \mathrm{Top}\wedge K\in \mathrm{Top}\right)\to \left(\mathrm{topGen}\left(J\right)=\mathrm{topGen}\left(K\right)\leftrightarrow J=K\right)$$
11	2 7 10	3bitr3d	$$⊢\left(J\in \mathrm{Top}\wedge K\in \mathrm{Top}\right)\to \left(\left[J\right]\underset{\dot{}}{\sim }=\left[K\right]\underset{\dot{}}{\sim }\leftrightarrow J=K\right)$$