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∈CZ∈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 ⊢Ⅎ_xZ
13 3 11 nfcxfr ⊢Ⅎ_xD
14 12 13 nfel ⊢ℲxZ∈D
15 11 14 nfral ⊢Ⅎx∀y∈∅Z∈D
16 2 raleqi ⊢∀y∈CZ∈D↔∀y∈∅Z∈D
17 16 a1i ⊢x=∅→∀y∈CZ∈D↔∀y∈∅Z∈D
18 15 17 rspce ⊢∅∈B∧∀y∈∅Z∈D→∃x∈B∀y∈CZ∈D
19 9 10 18 mp2an ⊢∃x∈B∀y∈CZ∈D
20 pm3.22 ⊢¬Z∈A∧∃x∈B∀y∈CZ∈D→∃x∈B∀y∈CZ∈D∧¬Z∈A
21 20 olcd ⊢¬Z∈A∧∃x∈B∀y∈CZ∈D→Z∈A∧¬∃x∈B∀y∈CZ∈D∨∃x∈B∀y∈CZ∈D∧¬Z∈A
22 xor ⊢¬Z∈A↔∃x∈B∀y∈CZ∈D↔Z∈A∧¬∃x∈B∀y∈CZ∈D∨∃x∈B∀y∈CZ∈D∧¬Z∈A
23 21 22 sylibr ⊢¬Z∈A∧∃x∈B∀y∈CZ∈D→¬Z∈A↔∃x∈B∀y∈CZ∈D
24 6 19 23 mp2an ⊢¬Z∈A↔∃x∈B∀y∈CZ∈D