epnsym

Description: The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022)

		Ref	Expression
	Assertion	epnsym	$⊢ E^{-1} \neq E$

Step	Hyp	Ref	Expression
1		cnvepnep	$⊢ E^{-1} \cap E = \emptyset$
2		disjeq0	$⊢ E^{-1} \cap E = \emptyset \to (E^{-1} = E \leftrightarrow (E^{-1} = \emptyset \land E = \emptyset))$
3		epn0	$⊢ E \neq \emptyset$
4		eqneqall	$⊢ E = \emptyset \to (E \neq \emptyset \to E^{-1} \neq E)$
5	3 4	mpi	$⊢ E = \emptyset \to E^{-1} \neq E$
6	5	adantl	$⊢ (E^{-1} = \emptyset \land E = \emptyset) \to E^{-1} \neq E$
7	6	a1i	$⊢ E^{-1} = E \to ((E^{-1} = \emptyset \land E = \emptyset) \to E^{-1} \neq E)$
8		neqne	$⊢ \neg E^{-1} = E \to E^{-1} \neq E$
9	8	a1d	$⊢ \neg E^{-1} = E \to (\neg (E^{-1} = \emptyset \land E = \emptyset) \to E^{-1} \neq E)$
10	7 9	bija	$⊢ (E^{-1} = E \leftrightarrow (E^{-1} = \emptyset \land E = \emptyset)) \to E^{-1} \neq E$
11	1 2 10	mp2b	$⊢ E^{-1} \neq E$

Metamath Proof Explorer