This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( 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 ) = (/) )