Theorem 1arithlem3

Description: Lemma for 1arith . (Contributed by Mario Carneiro, 30-May-2014)

	Ref	Expression
Hypothesis	1arith.1	|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )
Assertion	1arithlem3	|- ( N e. NN -> ( M ` N ) : Prime --> NN0 )

Proof

Step	Hyp	Ref	Expression
1		1arith.1	|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )
2	1	1arithlem1	|- ( N e. NN -> ( M ` N ) = ( p e. Prime |-> ( p pCnt N ) ) )
3		pccl	|- ( ( p e. Prime /\ N e. NN ) -> ( p pCnt N ) e. NN0 )
4	3	ancoms	|- ( ( N e. NN /\ p e. Prime ) -> ( p pCnt N ) e. NN0 )
5	2 4	fmpt3d	|- ( N e. NN -> ( M ` N ) : Prime --> NN0 )