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	|- .~ = ( Fne i^i `' Fne )
Assertion	fneer	|- .~ Er _V

Proof

Step	Hyp	Ref	Expression
1		fneval.1	|- .~ = ( Fne i^i `' Fne )
2		fveq2	|- ( x = y -> ( topGen ` x ) = ( topGen ` y ) )
3		inss1	|- ( Fne i^i `' Fne ) C_ Fne
4	1 3	eqsstri	|- .~ C_ Fne
5		fnerel	|- Rel Fne
6		relss	|- ( .~ C_ Fne -> ( Rel Fne -> Rel .~ ) )
7	4 5 6	mp2	|- Rel .~
8		dfrel4v	|- ( Rel .~ <-> .~ = { <. x , y >. | x .~ y } )
9	7 8	mpbi	|- .~ = { <. x , y >. | x .~ y }
10	1	fneval	|- ( ( x e. _V /\ y e. _V ) -> ( x .~ y <-> ( topGen ` x ) = ( topGen ` y ) ) )
11	10	el2v	|- ( x .~ y <-> ( topGen ` x ) = ( topGen ` y ) )
12	11	opabbii	|- { <. x , y >. | x .~ y } = { <. x , y >. | ( topGen ` x ) = ( topGen ` y ) }
13	9 12	eqtri	|- .~ = { <. x , y >. | ( topGen ` x ) = ( topGen ` y ) }
14	2 13	eqer	|- .~ Er _V