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