Theorem zfregs2VD

Description: Virtual deduction proof of zfregs2 . (Contributed by Alan Sare, 24-Oct-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	zfregs2VD	$$⊢A\ne \varnothing \to \neg \forall x\in A\exists y\left(y\in A\wedge y\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		idn1	$$⊢\left(A\ne \varnothing \to A\ne \varnothing \right)$$
2		zfregs	$$⊢A\ne \varnothing \to \exists x\in Ax\cap A=\varnothing$$
3	1 2	e1a	$$⊢\left(A\ne \varnothing \to \exists x\in Ax\cap A=\varnothing \right)$$
4		incom	$$⊢x\cap A=A\cap x$$
5	4	eqeq1i	$$⊢x\cap A=\varnothing \leftrightarrow A\cap x=\varnothing$$
6	5	rexbii	$$⊢\exists x\in Ax\cap A=\varnothing \leftrightarrow \exists x\in AA\cap x=\varnothing$$
7	3 6	e1bi	$$⊢\left(A\ne \varnothing \to \exists x\in AA\cap x=\varnothing \right)$$
8		disj1	$$⊢A\cap x=\varnothing \leftrightarrow \forall y\left(y\in A\to \neg y\in x\right)$$
9	8	rexbii	$$⊢\exists x\in AA\cap x=\varnothing \leftrightarrow \exists x\in A\forall y\left(y\in A\to \neg y\in x\right)$$
10	7 9	e1bi	$$⊢\left(A\ne \varnothing \to \exists x\in A\forall y\left(y\in A\to \neg y\in x\right)\right)$$
11		alinexa	$$⊢\forall y\left(y\in A\to \neg y\in x\right)\leftrightarrow \neg \exists y\left(y\in A\wedge y\in x\right)$$
12	11	rexbii	$$⊢\exists x\in A\forall y\left(y\in A\to \neg y\in x\right)\leftrightarrow \exists x\in A\neg \exists y\left(y\in A\wedge y\in x\right)$$
13	10 12	e1bi	$$⊢\left(A\ne \varnothing \to \exists x\in A\neg \exists y\left(y\in A\wedge y\in x\right)\right)$$
14		dfrex2	$$⊢\exists x\in A\neg \exists y\left(y\in A\wedge y\in x\right)\leftrightarrow \neg \forall x\in A\neg \neg \exists y\left(y\in A\wedge y\in x\right)$$
15	13 14	e1bi	$$⊢\left(A\ne \varnothing \to \neg \forall x\in A\neg \neg \exists y\left(y\in A\wedge y\in x\right)\right)$$
16		notnotr	$$⊢\neg \neg \exists y\left(y\in A\wedge y\in x\right)\to \exists y\left(y\in A\wedge y\in x\right)$$
17		notnot	$$⊢\exists y\left(y\in A\wedge y\in x\right)\to \neg \neg \exists y\left(y\in A\wedge y\in x\right)$$
18	16 17	impbii	$$⊢\neg \neg \exists y\left(y\in A\wedge y\in x\right)\leftrightarrow \exists y\left(y\in A\wedge y\in x\right)$$
19	18	ralbii	$$⊢\forall x\in A\neg \neg \exists y\left(y\in A\wedge y\in x\right)\leftrightarrow \forall x\in A\exists y\left(y\in A\wedge y\in x\right)$$
20	19	notbii	$$⊢\neg \forall x\in A\neg \neg \exists y\left(y\in A\wedge y\in x\right)\leftrightarrow \neg \forall x\in A\exists y\left(y\in A\wedge y\in x\right)$$
21	15 20	e1bi	$$⊢\left(A\ne \varnothing \to \neg \forall x\in A\exists y\left(y\in A\wedge y\in x\right)\right)$$
22	21	in1	$$⊢A\ne \varnothing \to \neg \forall x\in A\exists y\left(y\in A\wedge y\in x\right)$$