Theorem ndisj2

Description: A non-disjointness condition. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	ndisj2.1	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
Assertion	ndisj2	⊢ ( ¬ Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 ∧ ( 𝐵 ∩ 𝐶 ) ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		ndisj2.1	⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
2	1	disjor	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) )
3	2	notbii	⊢ ( ¬ Disj 𝑥 ∈ 𝐴 𝐵 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) )
4		rexnal	⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) )
5		rexnal	⊢ ( ∃ 𝑦 ∈ 𝐴 ¬ ( 𝑥 = 𝑦 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) ↔ ¬ ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) )
6		ioran	⊢ ( ¬ ( 𝑥 = 𝑦 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) ↔ ( ¬ 𝑥 = 𝑦 ∧ ¬ ( 𝐵 ∩ 𝐶 ) = ∅ ) )
7		df-ne	⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦 )
8		df-ne	⊢ ( ( 𝐵 ∩ 𝐶 ) ≠ ∅ ↔ ¬ ( 𝐵 ∩ 𝐶 ) = ∅ )
9	7 8	anbi12i	⊢ ( ( 𝑥 ≠ 𝑦 ∧ ( 𝐵 ∩ 𝐶 ) ≠ ∅ ) ↔ ( ¬ 𝑥 = 𝑦 ∧ ¬ ( 𝐵 ∩ 𝐶 ) = ∅ ) )
10	6 9	bitr4i	⊢ ( ¬ ( 𝑥 = 𝑦 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) ↔ ( 𝑥 ≠ 𝑦 ∧ ( 𝐵 ∩ 𝐶 ) ≠ ∅ ) )
11	10	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐴 ¬ ( 𝑥 = 𝑦 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 ∧ ( 𝐵 ∩ 𝐶 ) ≠ ∅ ) )
12	5 11	bitr3i	⊢ ( ¬ ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 ∧ ( 𝐵 ∩ 𝐶 ) ≠ ∅ ) )
13	12	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 ∧ ( 𝐵 ∩ 𝐶 ) ≠ ∅ ) )
14	3 4 13	3bitr2i	⊢ ( ¬ Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 ∧ ( 𝐵 ∩ 𝐶 ) ≠ ∅ ) )