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