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