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 e. A <-> E. x e. B A. y e. C Z e. 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 e. A
6 4 5 eqneltri 
 |-  -. Z e. A
7 0ex 
 |-  (/) e. _V
8 7 snid 
 |-  (/) e. { (/) }
9 8 1 eleqtrri 
 |-  (/) e. B
10 ral0 
 |-  A. y e. (/) Z e. D
11 nfcv 
 |-  F/_ x (/)
12 nfcv 
 |-  F/_ x Z
13 3 11 nfcxfr 
 |-  F/_ x D
14 12 13 nfel 
 |-  F/ x Z e. D
15 11 14 nfral 
 |-  F/ x A. y e. (/) Z e. D
16 2 raleqi 
 |-  ( A. y e. C Z e. D <-> A. y e. (/) Z e. D )
17 16 a1i 
 |-  ( x = (/) -> ( A. y e. C Z e. D <-> A. y e. (/) Z e. D ) )
18 15 17 rspce 
 |-  ( ( (/) e. B /\ A. y e. (/) Z e. D ) -> E. x e. B A. y e. C Z e. D )
19 9 10 18 mp2an 
 |-  E. x e. B A. y e. C Z e. D
20 pm3.22 
 |-  ( ( -. Z e. A /\ E. x e. B A. y e. C Z e. D ) -> ( E. x e. B A. y e. C Z e. D /\ -. Z e. A ) )
21 20 olcd 
 |-  ( ( -. Z e. A /\ E. x e. B A. y e. C Z e. D ) -> ( ( Z e. A /\ -. E. x e. B A. y e. C Z e. D ) \/ ( E. x e. B A. y e. C Z e. D /\ -. Z e. A ) ) )
22 xor 
 |-  ( -. ( Z e. A <-> E. x e. B A. y e. C Z e. D ) <-> ( ( Z e. A /\ -. E. x e. B A. y e. C Z e. D ) \/ ( E. x e. B A. y e. C Z e. D /\ -. Z e. A ) ) )
23 21 22 sylibr 
 |-  ( ( -. Z e. A /\ E. x e. B A. y e. C Z e. D ) -> -. ( Z e. A <-> E. x e. B A. y e. C Z e. D ) )
24 6 19 23 mp2an 
 |-  -. ( Z e. A <-> E. x e. B A. y e. C Z e. D )