Metamath Proof Explorer

Theorem djudisj

Description: Disjoint unions with disjoint index sets are disjoint. (Contributed by Stefan O'Rear, 21-Nov-2014)

Ref Expression
Assertion djudisj 
|- ( ( A i^i B ) = (/) -> ( U_ x e. A ( { x } X. C ) i^i U_ y e. B ( { y } X. D ) ) = (/) )

Proof

Step Hyp Ref Expression
1 djussxp 
 |-  U_ x e. A ( { x } X. C ) C_ ( A X. _V )
2 incom 
 |-  ( ( A X. _V ) i^i U_ y e. B ( { y } X. D ) ) = ( U_ y e. B ( { y } X. D ) i^i ( A X. _V ) )
3 djussxp 
 |-  U_ y e. B ( { y } X. D ) C_ ( B X. _V )
4 incom 
 |-  ( ( B X. _V ) i^i ( A X. _V ) ) = ( ( A X. _V ) i^i ( B X. _V ) )
5 xpdisj1 
 |-  ( ( A i^i B ) = (/) -> ( ( A X. _V ) i^i ( B X. _V ) ) = (/) )
6 4 5 syl5eq 
 |-  ( ( A i^i B ) = (/) -> ( ( B X. _V ) i^i ( A X. _V ) ) = (/) )
7 ssdisj 
 |-  ( ( U_ y e. B ( { y } X. D ) C_ ( B X. _V ) /\ ( ( B X. _V ) i^i ( A X. _V ) ) = (/) ) -> ( U_ y e. B ( { y } X. D ) i^i ( A X. _V ) ) = (/) )
8 3 6 7 sylancr 
 |-  ( ( A i^i B ) = (/) -> ( U_ y e. B ( { y } X. D ) i^i ( A X. _V ) ) = (/) )
9 2 8 syl5eq 
 |-  ( ( A i^i B ) = (/) -> ( ( A X. _V ) i^i U_ y e. B ( { y } X. D ) ) = (/) )
10 ssdisj 
 |-  ( ( U_ x e. A ( { x } X. C ) C_ ( A X. _V ) /\ ( ( A X. _V ) i^i U_ y e. B ( { y } X. D ) ) = (/) ) -> ( U_ x e. A ( { x } X. C ) i^i U_ y e. B ( { y } X. D ) ) = (/) )
11 1 9 10 sylancr 
 |-  ( ( A i^i B ) = (/) -> ( U_ x e. A ( { x } X. C ) i^i U_ y e. B ( { y } X. D ) ) = (/) )