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 | |
|
Assertion | iunxdif3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iunxdif3.1 | |
|
2 | inss2 | |
|
3 | nfcv | |
|
4 | 3 1 | nfin | |
5 | 4 1 | ssrexf | |
6 | eliun | |
|
7 | eliun | |
|
8 | 5 6 7 | 3imtr4g | |
9 | 8 | ssrdv | |
10 | 2 9 | ax-mp | |
11 | iuneq2 | |
|
12 | iun0 | |
|
13 | 11 12 | eqtrdi | |
14 | 10 13 | sseqtrid | |
15 | ss0 | |
|
16 | 14 15 | syl | |
17 | 16 | uneq1d | |
18 | iunxun | |
|
19 | inundif | |
|
20 | 19 | nfth | |
21 | 3 1 | nfdif | |
22 | 4 21 | nfun | |
23 | id | |
|
24 | eqidd | |
|
25 | 20 22 3 23 24 | iuneq12df | |
26 | 19 25 | ax-mp | |
27 | 18 26 | eqtr3i | |
28 | 27 | a1i | |
29 | uncom | |
|
30 | un0 | |
|
31 | 29 30 | eqtri | |
32 | 31 | a1i | |
33 | 17 28 32 | 3eqtr3rd | |