notsep

Description: In the Separation Scheme sepgi , we require that y not occur in ph (which can be generalized to "not be free in"). That requirement is necessary: notsep , which requires only ax-ext and ax-nul on top of first-order logic, derives *non*-existence of a "separating set" for specific values of the containing set A and of the separating condition ph . Therefore, from the axioms required by notsep and an overly strong axiom of separation without the requirement that y not occur in ph , we could derive F. , a contradiction. (Contributed by NM, 8-Feb-2006) (Proof shortened by BJ, 18-Nov-2023)

	Ref	Expression
Hypotheses	notsep.1	$⊢ A = \{\emptyset\}$
	notsep.2	$⊢ φ \leftrightarrow \neg x \in y$
Assertion	notsep	$⊢ \neg \exists y \forall x (x \in y \leftrightarrow (x \in A \land φ))$

Proof

Step	Hyp	Ref	Expression
1		notsep.1	$⊢ A = \{\emptyset\}$
2		notsep.2	$⊢ φ \leftrightarrow \neg x \in y$
3		0ex	$⊢ \emptyset \in V$
4	3	snnz	$⊢ \{\emptyset\} \neq \emptyset$
5	1 4	eqnetri	$⊢ A \neq \emptyset$
6		n0	$⊢ A \neq \emptyset \leftrightarrow \exists x x \in A$
7	5 6	mpbi	$⊢ \exists x x \in A$
8		pm5.19	$⊢ \neg (x \in y \leftrightarrow \neg x \in y)$
9		ibar	$⊢ x \in A \to (φ \leftrightarrow (x \in A \land φ))$
10	9 2	bitr3di	$⊢ x \in A \to ((x \in A \land φ) \leftrightarrow \neg x \in y)$
11	10	bibi2d	$⊢ x \in A \to ((x \in y \leftrightarrow (x \in A \land φ)) \leftrightarrow (x \in y \leftrightarrow \neg x \in y))$
12	8 11	mtbiri	$⊢ x \in A \to \neg (x \in y \leftrightarrow (x \in A \land φ))$
13	7 12	eximii	$⊢ \exists x \neg (x \in y \leftrightarrow (x \in A \land φ))$
14		exnal	$⊢ \exists x \neg (x \in y \leftrightarrow (x \in A \land φ)) \leftrightarrow \neg \forall x (x \in y \leftrightarrow (x \in A \land φ))$
15	13 14	mpbi	$⊢ \neg \forall x (x \in y \leftrightarrow (x \in A \land φ))$
16	15	nex	$⊢ \neg \exists y \forall x (x \in y \leftrightarrow (x \in A \land φ))$

Metamath Proof Explorer

Theorem notsep

Proof