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 ( 𝜑 → ( 𝑥𝐶 𝐵𝐸 ) = ∅ )