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

Metamath Proof Explorer

Theorem disjiun2

Description: In a disjoint collection, an indexed union is disjoint from an additional term. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses disjiun2.1 ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
disjiun2.2 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
disjiun2.3 ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 ∖ 𝐶 ) )
disjiun2.4 ⊢ ( 𝑥 = 𝐷 → 𝐵 = 𝐸 )
Assertion disjiun2 ( 𝜑 → ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ 𝐸 ) = ∅ )

Proof

Step Hyp Ref Expression
1 disjiun2.1 ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
2 disjiun2.2 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
3 disjiun2.3 ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 ∖ 𝐶 ) )
4 disjiun2.4 ⊢ ( 𝑥 = 𝐷 → 𝐵 = 𝐸 )
5 4 iunxsng ⊢ ( 𝐷 ∈ ( 𝐴 ∖ 𝐶 ) → ∪ 𝑥 ∈ { 𝐷 } 𝐵 = 𝐸 )
6 3 5 syl ⊢ ( 𝜑 → ∪ 𝑥 ∈ { 𝐷 } 𝐵 = 𝐸 )
7 6 ineq2d ⊢ ( 𝜑 → ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ { 𝐷 } 𝐵 ) = ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ 𝐸 ) )
8 eldifi ⊢ ( 𝐷 ∈ ( 𝐴 ∖ 𝐶 ) → 𝐷 ∈ 𝐴 )
9 snssi ⊢ ( 𝐷 ∈ 𝐴 → { 𝐷 } ⊆ 𝐴 )
10 3 8 9 3syl ⊢ ( 𝜑 → { 𝐷 } ⊆ 𝐴 )
11 3 eldifbd ⊢ ( 𝜑 → ¬ 𝐷 ∈ 𝐶 )
12 disjsn ⊢ ( ( 𝐶 ∩ { 𝐷 } ) = ∅ ↔ ¬ 𝐷 ∈ 𝐶 )
13 11 12 sylibr ⊢ ( 𝜑 → ( 𝐶 ∩ { 𝐷 } ) = ∅ )
14 disjiun ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ { 𝐷 } ⊆ 𝐴 ∧ ( 𝐶 ∩ { 𝐷 } ) = ∅ ) ) → ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ { 𝐷 } 𝐵 ) = ∅ )
15 1 2 10 13 14 syl13anc ⊢ ( 𝜑 → ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ { 𝐷 } 𝐵 ) = ∅ )
16 7 15 eqtr3d ⊢ ( 𝜑 → ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ 𝐸 ) = ∅ )