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

Metamath Proof Explorer

Theorem mapss

Description: Subset inheritance for set exponentiation. Theorem 99 of Suppes p. 89. (Contributed by NM, 10-Dec-2003) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion mapss 
|- ( ( B e. V /\ A C_ B ) -> ( A ^m C ) C_ ( B ^m C ) )

Proof

Step Hyp Ref Expression
1 elmapi 
 |-  ( f e. ( A ^m C ) -> f : C --> A )
2 1 adantl 
 |-  ( ( ( B e. V /\ A C_ B ) /\ f e. ( A ^m C ) ) -> f : C --> A )
3 simplr 
 |-  ( ( ( B e. V /\ A C_ B ) /\ f e. ( A ^m C ) ) -> A C_ B )
4 2 3 fssd 
 |-  ( ( ( B e. V /\ A C_ B ) /\ f e. ( A ^m C ) ) -> f : C --> B )
5 simpll 
 |-  ( ( ( B e. V /\ A C_ B ) /\ f e. ( A ^m C ) ) -> B e. V )
6 elmapex 
 |-  ( f e. ( A ^m C ) -> ( A e. _V /\ C e. _V ) )
7 6 simprd 
 |-  ( f e. ( A ^m C ) -> C e. _V )
8 7 adantl 
 |-  ( ( ( B e. V /\ A C_ B ) /\ f e. ( A ^m C ) ) -> C e. _V )
9 5 8 elmapd 
 |-  ( ( ( B e. V /\ A C_ B ) /\ f e. ( A ^m C ) ) -> ( f e. ( B ^m C ) <-> f : C --> B ) )
10 4 9 mpbird 
 |-  ( ( ( B e. V /\ A C_ B ) /\ f e. ( A ^m C ) ) -> f e. ( B ^m C ) )
11 10 ex 
 |-  ( ( B e. V /\ A C_ B ) -> ( f e. ( A ^m C ) -> f e. ( B ^m C ) ) )
12 11 ssrdv 
 |-  ( ( B e. V /\ A C_ B ) -> ( A ^m C ) C_ ( B ^m C ) )