Theorem fneer

Description: Fineness intersected with its converse is an equivalence relation. (Contributed by Jeff Hankins, 6-Oct-2009) (Revised by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypothesis	fneval.1	$$⊢\underset{\dot{}}{\sim }=\mathrm{Fne}\cap {\mathrm{Fne}}^{-1}$$
Assertion	fneer	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		fneval.1	$$⊢\underset{\dot{}}{\sim }=\mathrm{Fne}\cap {\mathrm{Fne}}^{-1}$$
2		fveq2	$$⊢x=y\to \mathrm{topGen}\left(x\right)=\mathrm{topGen}\left(y\right)$$
3		inss1	$$⊢\mathrm{Fne}\cap {\mathrm{Fne}}^{-1}\subseteq \mathrm{Fne}$$
4	1 3	eqsstri	$$⊢\underset{\dot{}}{\sim }\subseteq \mathrm{Fne}$$
5		fnerel	$$⊢\mathrm{Rel}\mathrm{Fne}$$
6		relss	$$⊢\underset{\dot{}}{\sim }\subseteq \mathrm{Fne}\to \left(\mathrm{Rel}\mathrm{Fne}\to \mathrm{Rel}\underset{\dot{}}{\sim }\right)$$
7	4 5 6	mp2	$$⊢\mathrm{Rel}\underset{\dot{}}{\sim }$$
8		dfrel4v	$$⊢\mathrm{Rel}\underset{\dot{}}{\sim }\leftrightarrow \underset{\dot{}}{\sim }=\left\{⟨x,y⟩|x\underset{\dot{}}{\sim }y\right\}$$
9	7 8	mpbi	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|x\underset{\dot{}}{\sim }y\right\}$$
10	1	fneval	$$⊢\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\to \left(x\underset{\dot{}}{\sim }y\leftrightarrow \mathrm{topGen}\left(x\right)=\mathrm{topGen}\left(y\right)\right)$$
11	10	el2v	$$⊢x\underset{\dot{}}{\sim }y\leftrightarrow \mathrm{topGen}\left(x\right)=\mathrm{topGen}\left(y\right)$$
12	11	opabbii	$$⊢\left\{⟨x,y⟩|x\underset{\dot{}}{\sim }y\right\}=\left\{⟨x,y⟩|\mathrm{topGen}\left(x\right)=\mathrm{topGen}\left(y\right)\right\}$$
13	9 12	eqtri	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\mathrm{topGen}\left(x\right)=\mathrm{topGen}\left(y\right)\right\}$$
14	2 13	eqer	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}\mathrm{V}$$