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 ∩ ◡ 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