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

Metamath Proof Explorer

Theorem disjiunel

Description: A set of elements B of a disjoint set A is disjoint with another element of that set. (Contributed by Thierry Arnoux, 24-May-2020)

Ref Expression
Hypotheses disjiunel.1 ⊢ φ → Disj x ∈ A B
disjiunel.2 ⊢ x = Y → B = D
disjiunel.3 ⊢ φ → E ⊆ A
disjiunel.4 ⊢ φ → Y ∈ A ∖ E
Assertion disjiunel ⊢ φ → ⋃ x ∈ E B ∩ D = ∅

Proof

Step Hyp Ref Expression
1 disjiunel.1 ⊢ φ → Disj x ∈ A B
2 disjiunel.2 ⊢ x = Y → B = D
3 disjiunel.3 ⊢ φ → E ⊆ A
4 disjiunel.4 ⊢ φ → Y ∈ A ∖ E
5 4 eldifad ⊢ φ → Y ∈ A
6 5 snssd ⊢ φ → Y ⊆ A
7 3 6 unssd ⊢ φ → E ∪ Y ⊆ A
8 disjss1 ⊢ E ∪ Y ⊆ A → Disj x ∈ A B → Disj x ∈ E ∪ Y B
9 7 1 8 sylc ⊢ φ → Disj x ∈ E ∪ Y B
10 4 eldifbd ⊢ φ → ¬ Y ∈ E
11 2 disjunsn ⊢ Y ∈ A ∧ ¬ Y ∈ E → Disj x ∈ E ∪ Y B ↔ Disj x ∈ E B ∧ ⋃ x ∈ E B ∩ D = ∅
12 5 10 11 syl2anc ⊢ φ → Disj x ∈ E ∪ Y B ↔ Disj x ∈ E B ∧ ⋃ x ∈ E B ∩ D = ∅
13 9 12 mpbid ⊢ φ → Disj x ∈ E B ∧ ⋃ x ∈ E B ∩ D = ∅
14 13 simprd ⊢ φ → ⋃ x ∈ E B ∩ D = ∅