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	⊢ 𝐵 = { ∅ }
	eliuniincex.2	⊢ 𝐶 = ∅
	eliuniincex.3	⊢ 𝐷 = ∅
	eliuniincex.4	⊢ 𝑍 = V
Assertion	eliuniincex	⊢ ¬ ( 𝑍 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		eliuniincex.1	⊢ 𝐵 = { ∅ }
2		eliuniincex.2	⊢ 𝐶 = ∅
3		eliuniincex.3	⊢ 𝐷 = ∅
4		eliuniincex.4	⊢ 𝑍 = V
5		nvel	⊢ ¬ V ∈ 𝐴
6	4 5	eqneltri	⊢ ¬ 𝑍 ∈ 𝐴
7		0ex	⊢ ∅ ∈ V
8	7	snid	⊢ ∅ ∈ { ∅ }
9	8 1	eleqtrri	⊢ ∅ ∈ 𝐵
10		ral0	⊢ ∀ 𝑦 ∈ ∅ 𝑍 ∈ 𝐷
11		nfcv	⊢ Ⅎ 𝑥 ∅
12		nfcv	⊢ Ⅎ 𝑥 𝑍
13	3 11	nfcxfr	⊢ Ⅎ 𝑥 𝐷
14	12 13	nfel	⊢ Ⅎ 𝑥 𝑍 ∈ 𝐷
15	11 14	nfral	⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ ∅ 𝑍 ∈ 𝐷
16	2	raleqi	⊢ ( ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ↔ ∀ 𝑦 ∈ ∅ 𝑍 ∈ 𝐷 )
17	16	a1i	⊢ ( 𝑥 = ∅ → ( ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ↔ ∀ 𝑦 ∈ ∅ 𝑍 ∈ 𝐷 ) )
18	15 17	rspce	⊢ ( ( ∅ ∈ 𝐵 ∧ ∀ 𝑦 ∈ ∅ 𝑍 ∈ 𝐷 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 )
19	9 10 18	mp2an	⊢ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷
20		pm3.22	⊢ ( ( ¬ 𝑍 ∈ 𝐴 ∧ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) → ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ∧ ¬ 𝑍 ∈ 𝐴 ) )
21	20	olcd	⊢ ( ( ¬ 𝑍 ∈ 𝐴 ∧ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) → ( ( 𝑍 ∈ 𝐴 ∧ ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) ∨ ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ∧ ¬ 𝑍 ∈ 𝐴 ) ) )
22		xor	⊢ ( ¬ ( 𝑍 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) ↔ ( ( 𝑍 ∈ 𝐴 ∧ ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) ∨ ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ∧ ¬ 𝑍 ∈ 𝐴 ) ) )
23	21 22	sylibr	⊢ ( ( ¬ 𝑍 ∈ 𝐴 ∧ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) → ¬ ( 𝑍 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 ) )
24	6 19 23	mp2an	⊢ ¬ ( 𝑍 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 )