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 = ∅
Assertion eliincex ⊢ ¬ A ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B A ∈ C

Proof

Step Hyp Ref Expression
1 eliinct.1 ⊢ A = V
2 eliinct.2 ⊢ B = ∅
3 nvel ⊢ ¬ V ∈ ⋂ x ∈ B C
4 1 3 eqneltri ⊢ ¬ A ∈ ⋂ x ∈ B C
5 ral0 ⊢ ∀ x ∈ ∅ A ∈ C
6 2 raleqi ⊢ ∀ x ∈ B A ∈ C ↔ ∀ x ∈ ∅ A ∈ C
7 5 6 mpbir ⊢ ∀ x ∈ B A ∈ C
8 pm3.22 ⊢ ¬ A ∈ ⋂ x ∈ B C ∧ ∀ x ∈ B A ∈ C → ∀ x ∈ B A ∈ C ∧ ¬ A ∈ ⋂ x ∈ B C
9 8 olcd ⊢ ¬ A ∈ ⋂ x ∈ B C ∧ ∀ x ∈ B A ∈ C → A ∈ ⋂ x ∈ B C ∧ ¬ ∀ x ∈ B A ∈ C ∨ ∀ x ∈ B A ∈ C ∧ ¬ A ∈ ⋂ x ∈ B C
10 xor ⊢ ¬ A ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B A ∈ C ↔ A ∈ ⋂ x ∈ B C ∧ ¬ ∀ x ∈ B A ∈ C ∨ ∀ x ∈ B A ∈ C ∧ ¬ A ∈ ⋂ x ∈ B C
11 9 10 sylibr ⊢ ¬ A ∈ ⋂ x ∈ B C ∧ ∀ x ∈ B A ∈ C → ¬ A ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B A ∈ C
12 4 7 11 mp2an ⊢ ¬ A ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B A ∈ C