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	|- ( ph -> Disj_ x e. A B )
	disjiunel.2	|- ( x = Y -> B = D )
	disjiunel.3	|- ( ph -> E C_ A )
	disjiunel.4	|- ( ph -> Y e. ( A \ E ) )
Assertion	disjiunel	|- ( ph -> ( U_ x e. E B i^i D ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		disjiunel.1	|- ( ph -> Disj_ x e. A B )
2		disjiunel.2	|- ( x = Y -> B = D )
3		disjiunel.3	|- ( ph -> E C_ A )
4		disjiunel.4	|- ( ph -> Y e. ( A \ E ) )
5	4	eldifad	|- ( ph -> Y e. A )
6	5	snssd	|- ( ph -> { Y } C_ A )
7	3 6	unssd	|- ( ph -> ( E u. { Y } ) C_ A )
8		disjss1	|- ( ( E u. { Y } ) C_ A -> ( Disj_ x e. A B -> Disj_ x e. ( E u. { Y } ) B ) )
9	7 1 8	sylc	|- ( ph -> Disj_ x e. ( E u. { Y } ) B )
10	4	eldifbd	|- ( ph -> -. Y e. E )
11	2	disjunsn	|- ( ( Y e. A /\ -. Y e. E ) -> ( Disj_ x e. ( E u. { Y } ) B <-> ( Disj_ x e. E B /\ ( U_ x e. E B i^i D ) = (/) ) ) )
12	5 10 11	syl2anc	|- ( ph -> ( Disj_ x e. ( E u. { Y } ) B <-> ( Disj_ x e. E B /\ ( U_ x e. E B i^i D ) = (/) ) ) )
13	9 12	mpbid	|- ( ph -> ( Disj_ x e. E B /\ ( U_ x e. E B i^i D ) = (/) ) )
14	13	simprd	|- ( ph -> ( U_ x e. E B i^i D ) = (/) )