Metamath Proof Explorer

Theorem eliuniincex

Description: Counterexample to show that the additional conditions in eliuniin and eliuniin2 are actually needed. Notice that the definition of A is not even needed (it can be any class). (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses eliuniincex.1 ⊢ B = ∅
eliuniincex.2 ⊢ C = ∅
eliuniincex.3 ⊢ D = ∅
eliuniincex.4 ⊢ Z = V
Assertion eliuniincex ⊢ ¬ Z ∈ A ↔ ∃ x ∈ B ∀ y ∈ C Z ∈ D

Proof

Step Hyp Ref Expression
1 eliuniincex.1 ⊢ B = ∅
2 eliuniincex.2 ⊢ C = ∅
3 eliuniincex.3 ⊢ D = ∅
4 eliuniincex.4 ⊢ Z = V
5 nvel ⊢ ¬ V ∈ A
6 4 5 eqneltri ⊢ ¬ Z ∈ A
7 0ex ⊢ ∅ ∈ V
8 7 snid ⊢ ∅ ∈ ∅
9 8 1 eleqtrri ⊢ ∅ ∈ B
10 ral0 ⊢ ∀ y ∈ ∅ Z ∈ D
11 nfcv ⊢ Ⅎ _ x ∅
12 nfcv ⊢ Ⅎ _ x Z
13 3 11 nfcxfr ⊢ Ⅎ _ x D
14 12 13 nfel ⊢ Ⅎ x Z ∈ D
15 11 14 nfral ⊢ Ⅎ x ∀ y ∈ ∅ Z ∈ D
16 2 raleqi ⊢ ∀ y ∈ C Z ∈ D ↔ ∀ y ∈ ∅ Z ∈ D
17 16 a1i ⊢ x = ∅ → ∀ y ∈ C Z ∈ D ↔ ∀ y ∈ ∅ Z ∈ D
18 15 17 rspce ⊢ ∅ ∈ B ∧ ∀ y ∈ ∅ Z ∈ D → ∃ x ∈ B ∀ y ∈ C Z ∈ D
19 9 10 18 mp2an ⊢ ∃ x ∈ B ∀ y ∈ C Z ∈ D
20 pm3.22 ⊢ ¬ Z ∈ A ∧ ∃ x ∈ B ∀ y ∈ C Z ∈ D → ∃ x ∈ B ∀ y ∈ C Z ∈ D ∧ ¬ Z ∈ A
21 20 olcd ⊢ ¬ Z ∈ A ∧ ∃ x ∈ B ∀ y ∈ C Z ∈ D → Z ∈ A ∧ ¬ ∃ x ∈ B ∀ y ∈ C Z ∈ D ∨ ∃ x ∈ B ∀ y ∈ C Z ∈ D ∧ ¬ Z ∈ A
22 xor ⊢ ¬ Z ∈ A ↔ ∃ x ∈ B ∀ y ∈ C Z ∈ D ↔ Z ∈ A ∧ ¬ ∃ x ∈ B ∀ y ∈ C Z ∈ D ∨ ∃ x ∈ B ∀ y ∈ C Z ∈ D ∧ ¬ Z ∈ A
23 21 22 sylibr ⊢ ¬ Z ∈ A ∧ ∃ x ∈ B ∀ y ∈ C Z ∈ D → ¬ Z ∈ A ↔ ∃ x ∈ B ∀ y ∈ C Z ∈ D
24 6 19 23 mp2an ⊢ ¬ Z ∈ A ↔ ∃ x ∈ B ∀ y ∈ C Z ∈ D