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

Metamath Proof Explorer

Theorem disjexc

Description: A variant of disjex , applicable for more generic families. (Contributed by Thierry Arnoux, 4-Oct-2016)

Ref Expression
Hypothesis disjexc.1 ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
Assertion disjexc ( ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝑥 = 𝑦 ) → ( 𝐴 = 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 disjexc.1 ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
2 1 imim2i ⊢ ( ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝑥 = 𝑦 ) → ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝐴 = 𝐵 ) )
3 orcom ⊢ ( ( 𝐴 = 𝐵 ∨ ¬ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ↔ ( ¬ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ∨ 𝐴 = 𝐵 ) )
4 df-in ⊢ ( 𝐴 ∩ 𝐵 ) = { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) }
5 4 neeq1i ⊢ ( ( 𝐴 ∩ 𝐵 ) ≠ ∅ ↔ { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } ≠ ∅ )
6 abn0 ⊢ ( { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } ≠ ∅ ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
7 5 6 bitr2i ⊢ ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ↔ ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
8 7 necon2bbii ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ¬ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
9 8 orbi2i ⊢ ( ( 𝐴 = 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) ↔ ( 𝐴 = 𝐵 ∨ ¬ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) )
10 imor ⊢ ( ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝐴 = 𝐵 ) ↔ ( ¬ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ∨ 𝐴 = 𝐵 ) )
11 3 9 10 3bitr4i ⊢ ( ( 𝐴 = 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) ↔ ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝐴 = 𝐵 ) )
12 2 11 sylibr ⊢ ( ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝑥 = 𝑦 ) → ( 𝐴 = 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) )