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 𝑥 ∈ 𝐴 𝐵 )
disjiunel.2 ⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐷 )
disjiunel.3 ⊢ ( 𝜑 → 𝐸 ⊆ 𝐴 )
disjiunel.4 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 ∖ 𝐸 ) )
Assertion disjiunel ( 𝜑 → ( ∪ 𝑥 ∈ 𝐸 𝐵 ∩ 𝐷 ) = ∅ )

Proof

Step Hyp Ref Expression
1 disjiunel.1 ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
2 disjiunel.2 ⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐷 )
3 disjiunel.3 ⊢ ( 𝜑 → 𝐸 ⊆ 𝐴 )
4 disjiunel.4 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 ∖ 𝐸 ) )
5 4 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
6 5 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝐴 )
7 3 6 unssd ⊢ ( 𝜑 → ( 𝐸 ∪ { 𝑌 } ) ⊆ 𝐴 )
8 disjss1 ⊢ ( ( 𝐸 ∪ { 𝑌 } ) ⊆ 𝐴 → ( Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑥 ∈ ( 𝐸 ∪ { 𝑌 } ) 𝐵 ) )
9 7 1 8 sylc ⊢ ( 𝜑 → Disj 𝑥 ∈ ( 𝐸 ∪ { 𝑌 } ) 𝐵 )
10 4 eldifbd ⊢ ( 𝜑 → ¬ 𝑌 ∈ 𝐸 )
11 2 disjunsn ⊢ ( ( 𝑌 ∈ 𝐴 ∧ ¬ 𝑌 ∈ 𝐸 ) → ( Disj 𝑥 ∈ ( 𝐸 ∪ { 𝑌 } ) 𝐵 ↔ ( Disj 𝑥 ∈ 𝐸 𝐵 ∧ ( ∪ 𝑥 ∈ 𝐸 𝐵 ∩ 𝐷 ) = ∅ ) ) )
12 5 10 11 syl2anc ⊢ ( 𝜑 → ( Disj 𝑥 ∈ ( 𝐸 ∪ { 𝑌 } ) 𝐵 ↔ ( Disj 𝑥 ∈ 𝐸 𝐵 ∧ ( ∪ 𝑥 ∈ 𝐸 𝐵 ∩ 𝐷 ) = ∅ ) ) )
13 9 12 mpbid ⊢ ( 𝜑 → ( Disj 𝑥 ∈ 𝐸 𝐵 ∧ ( ∪ 𝑥 ∈ 𝐸 𝐵 ∩ 𝐷 ) = ∅ ) )
14 13 simprd ⊢ ( 𝜑 → ( ∪ 𝑥 ∈ 𝐸 𝐵 ∩ 𝐷 ) = ∅ )