Metamath Proof Explorer

Theorem zfregs2

Description: Alternate strong form of the Axiom of Regularity. Not every element of a nonempty class contains some element of that class. (Contributed by Alan Sare, 24-Oct-2011) (Proof shortened by Wolf Lammen, 27-Sep-2013)

		Ref	Expression
	Assertion	zfregs2	$⊢ A \neq \emptyset \to \neg \forall x \in A \exists y (y \in A \land y \in x)$

Proof

Step	Hyp	Ref	Expression
1		zfregs	$⊢ A \neq \emptyset \to \exists x \in A x \cap A = \emptyset$
2		incom	$⊢ x \cap A = A \cap x$
3	2	eqeq1i	$⊢ x \cap A = \emptyset \leftrightarrow A \cap x = \emptyset$
4	3	rexbii	$⊢ \exists x \in A x \cap A = \emptyset \leftrightarrow \exists x \in A A \cap x = \emptyset$
5	1 4	sylib	$⊢ A \neq \emptyset \to \exists x \in A A \cap x = \emptyset$
6		disj1	$⊢ A \cap x = \emptyset \leftrightarrow \forall y (y \in A \to \neg y \in x)$
7	6	rexbii	$⊢ \exists x \in A A \cap x = \emptyset \leftrightarrow \exists x \in A \forall y (y \in A \to \neg y \in x)$
8	5 7	sylib	$⊢ A \neq \emptyset \to \exists x \in A \forall y (y \in A \to \neg y \in x)$
9		alinexa	$⊢ \forall y (y \in A \to \neg y \in x) \leftrightarrow \neg \exists y (y \in A \land y \in x)$
10	9	rexbii	$⊢ \exists x \in A \forall y (y \in A \to \neg y \in x) \leftrightarrow \exists x \in A \neg \exists y (y \in A \land y \in x)$
11	8 10	sylib	$⊢ A \neq \emptyset \to \exists x \in A \neg \exists y (y \in A \land y \in x)$
12		dfrex2	$⊢ \exists x \in A \neg \exists y (y \in A \land y \in x) \leftrightarrow \neg \forall x \in A \neg \neg \exists y (y \in A \land y \in x)$
13	11 12	sylib	$⊢ A \neq \emptyset \to \neg \forall x \in A \neg \neg \exists y (y \in A \land y \in x)$
14		notnotb	$⊢ \exists y (y \in A \land y \in x) \leftrightarrow \neg \neg \exists y (y \in A \land y \in x)$
15	14	ralbii	$⊢ \forall x \in A \exists y (y \in A \land y \in x) \leftrightarrow \forall x \in A \neg \neg \exists y (y \in A \land y \in x)$
16	13 15	sylnibr	$⊢ A \neq \emptyset \to \neg \forall x \in A \exists y (y \in A \land y \in x)$