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

Proof

Step	Hyp	Ref	Expression
1		disjiun2.1	|- ( ph -> Disj_ x e. A B )
2		disjiun2.2	|- ( ph -> C C_ A )
3		disjiun2.3	|- ( ph -> D e. ( A \ C ) )
4		disjiun2.4	|- ( x = D -> B = E )
5	4	iunxsng	|- ( D e. ( A \ C ) -> U_ x e. { D } B = E )
6	3 5	syl	|- ( ph -> U_ x e. { D } B = E )
7	6	ineq2d	|- ( ph -> ( U_ x e. C B i^i U_ x e. { D } B ) = ( U_ x e. C B i^i E ) )
8		eldifi	|- ( D e. ( A \ C ) -> D e. A )
9		snssi	|- ( D e. A -> { D } C_ A )
10	3 8 9	3syl	|- ( ph -> { D } C_ A )
11	3	eldifbd	|- ( ph -> -. D e. C )
12		disjsn	|- ( ( C i^i { D } ) = (/) <-> -. D e. C )
13	11 12	sylibr	|- ( ph -> ( C i^i { D } ) = (/) )
14		disjiun	|- ( ( Disj_ x e. A B /\ ( C C_ A /\ { D } C_ A /\ ( C i^i { D } ) = (/) ) ) -> ( U_ x e. C B i^i U_ x e. { D } B ) = (/) )
15	1 2 10 13 14	syl13anc	|- ( ph -> ( U_ x e. C B i^i U_ x e. { D } B ) = (/) )
16	7 15	eqtr3d	|- ( ph -> ( U_ x e. C B i^i E ) = (/) )