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\in \left(B^{\left(1\dots M\right)}\right)\to {A\upharpoonright }_{\left(1\dots N\right)}\in \left(B^{\left(1\dots N\right)}\right)$$

Proof

Step	Hyp	Ref	Expression
1		mapfzcons.1	$$⊢M=N+1$$
2		fzssp1	$$⊢\left(1\dots N\right)\subseteq \left(1\dots N+1\right)$$
3	1	oveq2i	$$⊢\left(1\dots M\right)=\left(1\dots N+1\right)$$
4	2 3	sseqtrri	$$⊢\left(1\dots N\right)\subseteq \left(1\dots M\right)$$
5		elmapssres	$$⊢\left(A\in \left(B^{\left(1\dots M\right)}\right)\wedge \left(1\dots N\right)\subseteq \left(1\dots M\right)\right)\to {A\upharpoonright }_{\left(1\dots N\right)}\in \left(B^{\left(1\dots N\right)}\right)$$
6	4 5	mpan2	$$⊢A\in \left(B^{\left(1\dots M\right)}\right)\to {A\upharpoonright }_{\left(1\dots N\right)}\in \left(B^{\left(1\dots N\right)}\right)$$