eliuniincex

Description: Counterexample to show that the additional conditions in eliuniin and eliuniin2 are actually needed. Notice that the definition of A is not even needed (it can be any class). (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	eliuniincex.1	\|- B = { (/) }
	eliuniincex.2	\|- C = (/)
	eliuniincex.3	\|- D = (/)
	eliuniincex.4	\|- Z = _V
Assertion	eliuniincex	\|- -. ( Z e. A <-> E. x e. B A. y e. C Z e. D )

Proof

Step	Hyp	Ref	Expression
1		eliuniincex.1	\|- B = { (/) }
2		eliuniincex.2	\|- C = (/)
3		eliuniincex.3	\|- D = (/)
4		eliuniincex.4	\|- Z = _V
5		nvel	\|- -. _V e. A
6	4 5	eqneltri	\|- -. Z e. A
7		0ex	\|- (/) e. _V
8	7	snid	\|- (/) e. { (/) }
9	8 1	eleqtrri	\|- (/) e. B
10		ral0	\|- A. y e. (/) Z e. D
11		nfcv	\|- F/_ x (/)
12		nfcv	\|- F/_ x Z
13	3 11	nfcxfr	\|- F/_ x D
14	12 13	nfel	\|- F/ x Z e. D
15	11 14	nfral	\|- F/ x A. y e. (/) Z e. D
16	2	raleqi	\|- ( A. y e. C Z e. D <-> A. y e. (/) Z e. D )
17	16	a1i	\|- ( x = (/) -> ( A. y e. C Z e. D <-> A. y e. (/) Z e. D ) )
18	15 17	rspce	\|- ( ( (/) e. B /\ A. y e. (/) Z e. D ) -> E. x e. B A. y e. C Z e. D )
19	9 10 18	mp2an	\|- E. x e. B A. y e. C Z e. D
20		pm3.22	\|- ( ( -. Z e. A /\ E. x e. B A. y e. C Z e. D ) -> ( E. x e. B A. y e. C Z e. D /\ -. Z e. A ) )
21	20	olcd	\|- ( ( -. Z e. A /\ E. x e. B A. y e. C Z e. D ) -> ( ( Z e. A /\ -. E. x e. B A. y e. C Z e. D ) \/ ( E. x e. B A. y e. C Z e. D /\ -. Z e. A ) ) )
22		xor	\|- ( -. ( Z e. A <-> E. x e. B A. y e. C Z e. D ) <-> ( ( Z e. A /\ -. E. x e. B A. y e. C Z e. D ) \/ ( E. x e. B A. y e. C Z e. D /\ -. Z e. A ) ) )
23	21 22	sylibr	\|- ( ( -. Z e. A /\ E. x e. B A. y e. C Z e. D ) -> -. ( Z e. A <-> E. x e. B A. y e. C Z e. D ) )
24	6 19 23	mp2an	\|- -. ( Z e. A <-> E. x e. B A. y e. C Z e. D )

Metamath Proof Explorer

Theorem eliuniincex

Proof