Metamath Proof Explorer

Theorem eliincex

Description: Counterexample to show that the additional conditions in eliin and eliin2 are actually needed. (Contributed by Glauco Siliprandi, 26-Jun-2021)

		Ref	Expression
	Hypotheses	eliinct.1	$⊢ A = V$
		eliinct.2	$⊢ B = \emptyset$
	Assertion	eliincex	$⊢ \neg (A \in ⋂_{x \in B} C \leftrightarrow \forall x \in B A \in C)$

Proof

Step	Hyp	Ref	Expression
1		eliinct.1	$⊢ A = V$
2		eliinct.2	$⊢ B = \emptyset$
3		nvel	$⊢ \neg V \in ⋂_{x \in B} C$
4	1 3	eqneltri	$⊢ \neg A \in ⋂_{x \in B} C$
5		ral0	$⊢ \forall x \in \emptyset A \in C$
6	2	raleqi	$⊢ \forall x \in B A \in C \leftrightarrow \forall x \in \emptyset A \in C$
7	5 6	mpbir	$⊢ \forall x \in B A \in C$
8		pm3.22	$⊢ (\neg A \in ⋂_{x \in B} C \land \forall x \in B A \in C) \to (\forall x \in B A \in C \land \neg A \in ⋂_{x \in B} C)$
9	8	olcd	$⊢ (\neg A \in ⋂_{x \in B} C \land \forall x \in B A \in C) \to ((A \in ⋂_{x \in B} C \land \neg \forall x \in B A \in C) \lor (\forall x \in B A \in C \land \neg A \in ⋂_{x \in B} C))$
10		xor	$⊢ \neg (A \in ⋂_{x \in B} C \leftrightarrow \forall x \in B A \in C) \leftrightarrow ((A \in ⋂_{x \in B} C \land \neg \forall x \in B A \in C) \lor (\forall x \in B A \in C \land \neg A \in ⋂_{x \in B} C))$
11	9 10	sylibr	$⊢ (\neg A \in ⋂_{x \in B} C \land \forall x \in B A \in C) \to \neg (A \in ⋂_{x \in B} C \leftrightarrow \forall x \in B A \in C)$
12	4 7 11	mp2an	$⊢ \neg (A \in ⋂_{x \in B} C \leftrightarrow \forall x \in B A \in C)$