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	$⊢ \underset{˙}{\sim} = Fne \cap {Fne}^{-1}$
	Assertion	fneer	$⊢ \underset{˙}{\sim} Er V$

Proof

Step	Hyp	Ref	Expression
1		fneval.1	$⊢ \underset{˙}{\sim} = Fne \cap {Fne}^{-1}$
2		fveq2	$⊢ x = y \to topGen (x) = topGen (y)$
3		inss1	$⊢ Fne \cap {Fne}^{-1} \subseteq Fne$
4	1 3	eqsstri	$⊢ \underset{˙}{\sim} \subseteq Fne$
5		fnerel	$⊢ Rel Fne$
6		relss	$⊢ \underset{˙}{\sim} \subseteq Fne \to (Rel Fne \to Rel \underset{˙}{\sim})$
7	4 5 6	mp2	$⊢ Rel \underset{˙}{\sim}$
8		dfrel4v	$⊢ Rel \underset{˙}{\sim} \leftrightarrow \underset{˙}{\sim} = \{⟨x, y⟩ \| x \underset{˙}{\sim} y\}$
9	7 8	mpbi	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| x \underset{˙}{\sim} y\}$
10	1	fneval	$⊢ (x \in V \land y \in V) \to (x \underset{˙}{\sim} y \leftrightarrow topGen (x) = topGen (y))$
11	10	el2v	$⊢ x \underset{˙}{\sim} y \leftrightarrow topGen (x) = topGen (y)$
12	11	opabbii	$⊢ \{⟨x, y⟩ \| x \underset{˙}{\sim} y\} = \{⟨x, y⟩ \| topGen (x) = topGen (y)\}$
13	9 12	eqtri	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| topGen (x) = topGen (y)\}$
14	2 13	eqer	$⊢ \underset{˙}{\sim} Er V$