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