This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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