This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 = 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 ⊢ ¬ ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 )