Metamath Proof Explorer

Theorem iunxdif3

Description: An indexed union where some terms are the empty set. See iunxdif2 . (Contributed by Thierry Arnoux, 4-May-2020)

Ref Expression
Hypothesis iunxdif3.1 
|- F/_ x E
Assertion iunxdif3 
|- ( A. x e. E B = (/) -> U_ x e. ( A \ E ) B = U_ x e. A B )

Proof

Step Hyp Ref Expression
1 iunxdif3.1 
 |-  F/_ x E
2 inss2 
 |-  ( A i^i E ) C_ E
3 nfcv 
 |-  F/_ x A
4 3 1 nfin 
 |-  F/_ x ( A i^i E )
5 4 1 ssrexf 
 |-  ( ( A i^i E ) C_ E -> ( E. x e. ( A i^i E ) y e. B -> E. x e. E y e. B ) )
6 eliun 
 |-  ( y e. U_ x e. ( A i^i E ) B <-> E. x e. ( A i^i E ) y e. B )
7 eliun 
 |-  ( y e. U_ x e. E B <-> E. x e. E y e. B )
8 5 6 7 3imtr4g 
 |-  ( ( A i^i E ) C_ E -> ( y e. U_ x e. ( A i^i E ) B -> y e. U_ x e. E B ) )
9 8 ssrdv 
 |-  ( ( A i^i E ) C_ E -> U_ x e. ( A i^i E ) B C_ U_ x e. E B )
10 2 9 ax-mp 
 |-  U_ x e. ( A i^i E ) B C_ U_ x e. E B
11 iuneq2 
 |-  ( A. x e. E B = (/) -> U_ x e. E B = U_ x e. E (/) )
12 iun0 
 |-  U_ x e. E (/) = (/)
13 11 12 eqtrdi 
 |-  ( A. x e. E B = (/) -> U_ x e. E B = (/) )
14 10 13 sseqtrid 
 |-  ( A. x e. E B = (/) -> U_ x e. ( A i^i E ) B C_ (/) )
15 ss0 
 |-  ( U_ x e. ( A i^i E ) B C_ (/) -> U_ x e. ( A i^i E ) B = (/) )
16 14 15 syl 
 |-  ( A. x e. E B = (/) -> U_ x e. ( A i^i E ) B = (/) )
17 16 uneq1d 
 |-  ( A. x e. E B = (/) -> ( U_ x e. ( A i^i E ) B u. U_ x e. ( A \ E ) B ) = ( (/) u. U_ x e. ( A \ E ) B ) )
18 iunxun 
 |-  U_ x e. ( ( A i^i E ) u. ( A \ E ) ) B = ( U_ x e. ( A i^i E ) B u. U_ x e. ( A \ E ) B )
19 inundif 
 |-  ( ( A i^i E ) u. ( A \ E ) ) = A
20 19 nfth 
 |-  F/ x ( ( A i^i E ) u. ( A \ E ) ) = A
21 3 1 nfdif 
 |-  F/_ x ( A \ E )
22 4 21 nfun 
 |-  F/_ x ( ( A i^i E ) u. ( A \ E ) )
23 id 
 |-  ( ( ( A i^i E ) u. ( A \ E ) ) = A -> ( ( A i^i E ) u. ( A \ E ) ) = A )
24 eqidd 
 |-  ( ( ( A i^i E ) u. ( A \ E ) ) = A -> B = B )
25 20 22 3 23 24 iuneq12df 
 |-  ( ( ( A i^i E ) u. ( A \ E ) ) = A -> U_ x e. ( ( A i^i E ) u. ( A \ E ) ) B = U_ x e. A B )
26 19 25 ax-mp 
 |-  U_ x e. ( ( A i^i E ) u. ( A \ E ) ) B = U_ x e. A B
27 18 26 eqtr3i 
 |-  ( U_ x e. ( A i^i E ) B u. U_ x e. ( A \ E ) B ) = U_ x e. A B
28 27 a1i 
 |-  ( A. x e. E B = (/) -> ( U_ x e. ( A i^i E ) B u. U_ x e. ( A \ E ) B ) = U_ x e. A B )
29 uncom 
 |-  ( (/) u. U_ x e. ( A \ E ) B ) = ( U_ x e. ( A \ E ) B u. (/) )
30 un0 
 |-  ( U_ x e. ( A \ E ) B u. (/) ) = U_ x e. ( A \ E ) B
31 29 30 eqtri 
 |-  ( (/) u. U_ x e. ( A \ E ) B ) = U_ x e. ( A \ E ) B
32 31 a1i 
 |-  ( A. x e. E B = (/) -> ( (/) u. U_ x e. ( A \ E ) B ) = U_ x e. ( A \ E ) B )
33 17 28 32 3eqtr3rd 
 |-  ( A. x e. E B = (/) -> U_ x e. ( A \ E ) B = U_ x e. A B )