This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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