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	⊢ 𝐴 = V
	eliinct.2	⊢ 𝐵 = ∅
Assertion	eliincex	⊢ ¬ ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		eliinct.1	⊢ 𝐴 = V
2		eliinct.2	⊢ 𝐵 = ∅
3		nvel	⊢ ¬ V ∈ ∩ 𝑥 ∈ 𝐵 𝐶
4	1 3	eqneltri	⊢ ¬ 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶
5		ral0	⊢ ∀ 𝑥 ∈ ∅ 𝐴 ∈ 𝐶
6	2	raleqi	⊢ ( ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ↔ ∀ 𝑥 ∈ ∅ 𝐴 ∈ 𝐶 )
7	5 6	mpbir	⊢ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶
8		pm3.22	⊢ ( ( ¬ 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) → ( ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ∧ ¬ 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ) )
9	8	olcd	⊢ ( ( ¬ 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) → ( ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ ¬ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) ∨ ( ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ∧ ¬ 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ) ) )
10		xor	⊢ ( ¬ ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) ↔ ( ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ ¬ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) ∨ ( ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ∧ ¬ 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ) ) )
11	9 10	sylibr	⊢ ( ( ¬ 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) → ¬ ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) )
12	4 7 11	mp2an	⊢ ¬ ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 )