Theorem mapfzcons1cl

Description: A nonempty mapping has a prefix. (Contributed by Stefan O'Rear, 10-Oct-2014) (Revised by Stefan O'Rear, 5-May-2015)

	Ref	Expression
Hypothesis	mapfzcons.1	|- M = ( N + 1 )
Assertion	mapfzcons1cl	|- ( A e. ( B ^m ( 1 ... M ) ) -> ( A |` ( 1 ... N ) ) e. ( B ^m ( 1 ... N ) ) )

Proof

Step	Hyp	Ref	Expression
1		mapfzcons.1	|- M = ( N + 1 )
2		fzssp1	|- ( 1 ... N ) C_ ( 1 ... ( N + 1 ) )
3	1	oveq2i	|- ( 1 ... M ) = ( 1 ... ( N + 1 ) )
4	2 3	sseqtrri	|- ( 1 ... N ) C_ ( 1 ... M )
5		elmapssres	|- ( ( A e. ( B ^m ( 1 ... M ) ) /\ ( 1 ... N ) C_ ( 1 ... M ) ) -> ( A |` ( 1 ... N ) ) e. ( B ^m ( 1 ... N ) ) )
6	4 5	mpan2	|- ( A e. ( B ^m ( 1 ... M ) ) -> ( A |` ( 1 ... N ) ) e. ( B ^m ( 1 ... N ) ) )