Metamath Proof Explorer


Theorem plyss

Description: The polynomial set function preserves the subset relation. (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion plyss STTPolySPolyT

Proof

Step Hyp Ref Expression
1 simpr STTT
2 cnex V
3 ssexg TVTV
4 1 2 3 sylancl STTTV
5 snex 0V
6 unexg TV0VT0V
7 4 5 6 sylancl STTT0V
8 unss1 STS0T0
9 8 adantr STTS0T0
10 mapss T0VS0T0S00T00
11 7 9 10 syl2anc STTS00T00
12 ssrexv S00T00aS00f=zk=0nakzkaT00f=zk=0nakzk
13 11 12 syl STTaS00f=zk=0nakzkaT00f=zk=0nakzk
14 13 reximdv STTn0aS00f=zk=0nakzkn0aT00f=zk=0nakzk
15 14 ss2abdv STTf|n0aS00f=zk=0nakzkf|n0aT00f=zk=0nakzk
16 sstr STTS
17 plyval SPolyS=f|n0aS00f=zk=0nakzk
18 16 17 syl STTPolyS=f|n0aS00f=zk=0nakzk
19 plyval TPolyT=f|n0aT00f=zk=0nakzk
20 19 adantl STTPolyT=f|n0aT00f=zk=0nakzk
21 15 18 20 3sstr4d STTPolySPolyT