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

Metamath Proof Explorer

Theorem cnvepnep

Description: The membership (epsilon) relation and its converse are disjoint, i.e., _E is an asymmetric relation. Variable-free version of en2lp . (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 19-Jun-2022)

		Ref	Expression
	Assertion	cnvepnep	$⊢ E^{-1} \cap E = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		df-eprel	$⊢ E = \{⟨y, x⟩ \| y \in x\}$
2	1	cnveqi	$⊢ E^{-1} = {\{⟨y, x⟩ \| y \in x\}}^{-1}$
3		cnvopab	$⊢ {\{⟨y, x⟩ \| y \in x\}}^{-1} = \{⟨x, y⟩ \| y \in x\}$
4	2 3	eqtri	$⊢ E^{-1} = \{⟨x, y⟩ \| y \in x\}$
5		df-eprel	$⊢ E = \{⟨x, y⟩ \| x \in y\}$
6	4 5	ineq12i	$⊢ E^{-1} \cap E = \{⟨x, y⟩ \| y \in x\} \cap \{⟨x, y⟩ \| x \in y\}$
7		inopab	$⊢ \{⟨x, y⟩ \| y \in x\} \cap \{⟨x, y⟩ \| x \in y\} = \{⟨x, y⟩ \| (y \in x \land x \in y)\}$
8	6 7	eqtri	$⊢ E^{-1} \cap E = \{⟨x, y⟩ \| (y \in x \land x \in y)\}$
9		en2lp	$⊢ \neg (y \in x \land x \in y)$
10	9	gen2	$⊢ \forall x \forall y \neg (y \in x \land x \in y)$
11		opab0	$⊢ \{⟨x, y⟩ \| (y \in x \land x \in y)\} = \emptyset \leftrightarrow \forall x \forall y \neg (y \in x \land x \in y)$
12	10 11	mpbir	$⊢ \{⟨x, y⟩ \| (y \in x \land x \in y)\} = \emptyset$
13	8 12	eqtri	$⊢ E^{-1} \cap E = \emptyset$