Theorem coef2

Description: The domain and range of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Hypothesis	dgrval.1	|- A = ( coeff ` F )
Assertion	coef2	|- ( ( F e. ( Poly ` S ) /\ 0 e. S ) -> A : NN0 --> S )

Proof

Step	Hyp	Ref	Expression
1		dgrval.1	|- A = ( coeff ` F )
2	1	coef	|- ( F e. ( Poly ` S ) -> A : NN0 --> ( S u. { 0 } ) )
3	2	adantr	|- ( ( F e. ( Poly ` S ) /\ 0 e. S ) -> A : NN0 --> ( S u. { 0 } ) )
4		simpr	|- ( ( F e. ( Poly ` S ) /\ 0 e. S ) -> 0 e. S )
5	4	snssd	|- ( ( F e. ( Poly ` S ) /\ 0 e. S ) -> { 0 } C_ S )
6		ssequn2	|- ( { 0 } C_ S <-> ( S u. { 0 } ) = S )
7	5 6	sylib	|- ( ( F e. ( Poly ` S ) /\ 0 e. S ) -> ( S u. { 0 } ) = S )
8	7	feq3d	|- ( ( F e. ( Poly ` S ) /\ 0 e. S ) -> ( A : NN0 --> ( S u. { 0 } ) <-> A : NN0 --> S ) )
9	3 8	mpbid	|- ( ( F e. ( Poly ` S ) /\ 0 e. S ) -> A : NN0 --> S )