Metamath Proof Explorer

Theorem pmss12g

Description: Subset relation for the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013)

Ref Expression
Assertion pmss12g 
|- ( ( ( A C_ C /\ B C_ D ) /\ ( C e. V /\ D e. W ) ) -> ( A ^pm B ) C_ ( C ^pm D ) )

Proof

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