This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 ∧ ( 𝐵 ∩ 𝐶 ) ≠ ∅ ) )