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