This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem coef2

Description: The domain and codomain 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 )