Description: The polynomial set function preserves the subset relation. (Contributed by Mario Carneiro, 17-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | plyss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr | |
|
2 | cnex | |
|
3 | ssexg | |
|
4 | 1 2 3 | sylancl | |
5 | snex | |
|
6 | unexg | |
|
7 | 4 5 6 | sylancl | |
8 | unss1 | |
|
9 | 8 | adantr | |
10 | mapss | |
|
11 | 7 9 10 | syl2anc | |
12 | ssrexv | |
|
13 | 11 12 | syl | |
14 | 13 | reximdv | |
15 | 14 | ss2abdv | |
16 | sstr | |
|
17 | plyval | |
|
18 | 16 17 | syl | |
19 | plyval | |
|
20 | 19 | adantl | |
21 | 15 18 20 | 3sstr4d | |