Theorem elmapssres

Description: A restricted mapping is a mapping. (Contributed by Stefan O'Rear, 9-Oct-2014) (Revised by Mario Carneiro, 5-May-2015)

	Ref	Expression
Assertion	elmapssres	|- ( ( A e. ( B ^m C ) /\ D C_ C ) -> ( A |` D ) e. ( B ^m D ) )

Proof

Step	Hyp	Ref	Expression
1		elmapi	|- ( A e. ( B ^m C ) -> A : C --> B )
2		fssres	|- ( ( A : C --> B /\ D C_ C ) -> ( A |` D ) : D --> B )
3	1 2	sylan	|- ( ( A e. ( B ^m C ) /\ D C_ C ) -> ( A |` D ) : D --> B )
4		elmapex	|- ( A e. ( B ^m C ) -> ( B e. _V /\ C e. _V ) )
5	4	simpld	|- ( A e. ( B ^m C ) -> B e. _V )
6	5	adantr	|- ( ( A e. ( B ^m C ) /\ D C_ C ) -> B e. _V )
7	4	simprd	|- ( A e. ( B ^m C ) -> C e. _V )
8		ssexg	|- ( ( D C_ C /\ C e. _V ) -> D e. _V )
9	8	ancoms	|- ( ( C e. _V /\ D C_ C ) -> D e. _V )
10	7 9	sylan	|- ( ( A e. ( B ^m C ) /\ D C_ C ) -> D e. _V )
11	6 10	elmapd	|- ( ( A e. ( B ^m C ) /\ D C_ C ) -> ( ( A |` D ) e. ( B ^m D ) <-> ( A |` D ) : D --> B ) )
12	3 11	mpbird	|- ( ( A e. ( B ^m C ) /\ D C_ C ) -> ( A |` D ) e. ( B ^m D ) )