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