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 ∩ Fne )
Assertion fneer Er V

Proof

Step Hyp Ref Expression
1 fneval.1 = ( Fne ∩ Fne )
2 fveq2 ( 𝑥 = 𝑦 → ( topGen ‘ 𝑥 ) = ( topGen ‘ 𝑦 ) )
3 inss1 ( Fne ∩ Fne ) ⊆ Fne
4 1 3 eqsstri ⊆ Fne
5 fnerel Rel Fne
6 relss ( ⊆ Fne → ( Rel Fne → Rel ) )
7 4 5 6 mp2 Rel
8 dfrel4v ( Rel = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑦 } )
9 7 8 mpbi = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑦 }
10 1 fneval ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 𝑦 ↔ ( topGen ‘ 𝑥 ) = ( topGen ‘ 𝑦 ) ) )
11 10 el2v ( 𝑥 𝑦 ↔ ( topGen ‘ 𝑥 ) = ( topGen ‘ 𝑦 ) )
12 11 opabbii { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑦 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( topGen ‘ 𝑥 ) = ( topGen ‘ 𝑦 ) }
13 9 12 eqtri = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( topGen ‘ 𝑥 ) = ( topGen ‘ 𝑦 ) }
14 2 13 eqer Er V