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 )