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