Description: Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | founiiun | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniiun | |
|
2 | foelcdmi | |
|
3 | eqimss2 | |
|
4 | 3 | reximi | |
5 | 2 4 | syl | |
6 | 5 | ralrimiva | |
7 | iunss2 | |
|
8 | 6 7 | syl | |
9 | fof | |
|
10 | 9 | ffvelcdmda | |
11 | ssidd | |
|
12 | sseq2 | |
|
13 | 12 | rspcev | |
14 | 10 11 13 | syl2anc | |
15 | 14 | ralrimiva | |
16 | iunss2 | |
|
17 | 15 16 | syl | |
18 | 8 17 | eqssd | |
19 | 1 18 | eqtrid | |