Description: The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | imasaddf.f | |
|
imasaddf.e | |
||
imasaddflem.a | |
||
imasaddflem.c | |
||
Assertion | imasaddflem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imasaddf.f | |
|
2 | imasaddf.e | |
|
3 | imasaddflem.a | |
|
4 | imasaddflem.c | |
|
5 | 1 2 3 | imasaddfnlem | |
6 | fof | |
|
7 | 1 6 | syl | |
8 | ffvelrn | |
|
9 | ffvelrn | |
|
10 | 8 9 | anim12dan | |
11 | opelxpi | |
|
12 | 10 11 | syl | |
13 | 7 12 | sylan | |
14 | ffvelrn | |
|
15 | 7 4 14 | syl2an2r | |
16 | 13 15 | opelxpd | |
17 | 16 | snssd | |
18 | 17 | anassrs | |
19 | 18 | iunssd | |
20 | 19 | iunssd | |
21 | 3 20 | eqsstrd | |
22 | dff2 | |
|
23 | 5 21 22 | sylanbrc | |