Metamath Proof Explorer


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 ) )