Step |
Hyp |
Ref |
Expression |
1 |
|
xpss12 |
|- ( ( B C_ D /\ A C_ C ) -> ( B X. A ) C_ ( D X. C ) ) |
2 |
1
|
ancoms |
|- ( ( A C_ C /\ B C_ D ) -> ( B X. A ) C_ ( D X. C ) ) |
3 |
|
sstr |
|- ( ( f C_ ( B X. A ) /\ ( B X. A ) C_ ( D X. C ) ) -> f C_ ( D X. C ) ) |
4 |
3
|
expcom |
|- ( ( B X. A ) C_ ( D X. C ) -> ( f C_ ( B X. A ) -> f C_ ( D X. C ) ) ) |
5 |
2 4
|
syl |
|- ( ( A C_ C /\ B C_ D ) -> ( f C_ ( B X. A ) -> f C_ ( D X. C ) ) ) |
6 |
5
|
anim2d |
|- ( ( A C_ C /\ B C_ D ) -> ( ( Fun f /\ f C_ ( B X. A ) ) -> ( Fun f /\ f C_ ( D X. C ) ) ) ) |
7 |
6
|
adantr |
|- ( ( ( A C_ C /\ B C_ D ) /\ ( C e. V /\ D e. W ) ) -> ( ( Fun f /\ f C_ ( B X. A ) ) -> ( Fun f /\ f C_ ( D X. C ) ) ) ) |
8 |
|
ssexg |
|- ( ( A C_ C /\ C e. V ) -> A e. _V ) |
9 |
|
ssexg |
|- ( ( B C_ D /\ D e. W ) -> B e. _V ) |
10 |
|
elpmg |
|- ( ( A e. _V /\ B e. _V ) -> ( f e. ( A ^pm B ) <-> ( Fun f /\ f C_ ( B X. A ) ) ) ) |
11 |
8 9 10
|
syl2an |
|- ( ( ( A C_ C /\ C e. V ) /\ ( B C_ D /\ D e. W ) ) -> ( f e. ( A ^pm B ) <-> ( Fun f /\ f C_ ( B X. A ) ) ) ) |
12 |
11
|
an4s |
|- ( ( ( A C_ C /\ B C_ D ) /\ ( C e. V /\ D e. W ) ) -> ( f e. ( A ^pm B ) <-> ( Fun f /\ f C_ ( B X. A ) ) ) ) |
13 |
|
elpmg |
|- ( ( C e. V /\ D e. W ) -> ( f e. ( C ^pm D ) <-> ( Fun f /\ f C_ ( D X. C ) ) ) ) |
14 |
13
|
adantl |
|- ( ( ( A C_ C /\ B C_ D ) /\ ( C e. V /\ D e. W ) ) -> ( f e. ( C ^pm D ) <-> ( Fun f /\ f C_ ( D X. C ) ) ) ) |
15 |
7 12 14
|
3imtr4d |
|- ( ( ( A C_ C /\ B C_ D ) /\ ( C e. V /\ D e. W ) ) -> ( f e. ( A ^pm B ) -> f e. ( C ^pm D ) ) ) |
16 |
15
|
ssrdv |
|- ( ( ( A C_ C /\ B C_ D ) /\ ( C e. V /\ D e. W ) ) -> ( A ^pm B ) C_ ( C ^pm D ) ) |