Metamath Proof Explorer

Theorem difmap

Description: Difference of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses difmap.a 
|- ( ph -> A e. V )
difmap.b 
|- ( ph -> B e. W )
difmap.v 
|- ( ph -> C e. Z )
difmap.n 
|- ( ph -> C =/= (/) )
Assertion difmap 
|- ( ph -> ( ( A \ B ) ^m C ) C_ ( ( A ^m C ) \ ( B ^m C ) ) )

Proof

Step Hyp Ref Expression
1 difmap.a 
 |-  ( ph -> A e. V )
2 difmap.b 
 |-  ( ph -> B e. W )
3 difmap.v 
 |-  ( ph -> C e. Z )
4 difmap.n 
 |-  ( ph -> C =/= (/) )
5 difssd 
 |-  ( ph -> ( A \ B ) C_ A )
6 mapss 
 |-  ( ( A e. V /\ ( A \ B ) C_ A ) -> ( ( A \ B ) ^m C ) C_ ( A ^m C ) )
7 1 5 6 syl2anc 
 |-  ( ph -> ( ( A \ B ) ^m C ) C_ ( A ^m C ) )
8 7 adantr 
 |-  ( ( ph /\ f e. ( ( A \ B ) ^m C ) ) -> ( ( A \ B ) ^m C ) C_ ( A ^m C ) )
9 simpr 
 |-  ( ( ph /\ f e. ( ( A \ B ) ^m C ) ) -> f e. ( ( A \ B ) ^m C ) )
10 8 9 sseldd 
 |-  ( ( ph /\ f e. ( ( A \ B ) ^m C ) ) -> f e. ( A ^m C ) )
11 n0 
 |-  ( C =/= (/) <-> E. x x e. C )
12 4 11 sylib 
 |-  ( ph -> E. x x e. C )
13 12 adantr 
 |-  ( ( ph /\ f e. ( ( A \ B ) ^m C ) ) -> E. x x e. C )
14 simpr 
 |-  ( ( x e. C /\ f : C --> B ) -> f : C --> B )
15 simpl 
 |-  ( ( x e. C /\ f : C --> B ) -> x e. C )
16 14 15 ffvelrnd 
 |-  ( ( x e. C /\ f : C --> B ) -> ( f ` x ) e. B )
17 16 adantll 
 |-  ( ( ( ( ph /\ f e. ( ( A \ B ) ^m C ) ) /\ x e. C ) /\ f : C --> B ) -> ( f ` x ) e. B )
18 elmapi 
 |-  ( f e. ( ( A \ B ) ^m C ) -> f : C --> ( A \ B ) )
19 18 adantr 
 |-  ( ( f e. ( ( A \ B ) ^m C ) /\ x e. C ) -> f : C --> ( A \ B ) )
20 simpr 
 |-  ( ( f e. ( ( A \ B ) ^m C ) /\ x e. C ) -> x e. C )
21 19 20 ffvelrnd 
 |-  ( ( f e. ( ( A \ B ) ^m C ) /\ x e. C ) -> ( f ` x ) e. ( A \ B ) )
22 eldifn 
 |-  ( ( f ` x ) e. ( A \ B ) -> -. ( f ` x ) e. B )
23 21 22 syl 
 |-  ( ( f e. ( ( A \ B ) ^m C ) /\ x e. C ) -> -. ( f ` x ) e. B )
24 23 ad4ant23 
 |-  ( ( ( ( ph /\ f e. ( ( A \ B ) ^m C ) ) /\ x e. C ) /\ f : C --> B ) -> -. ( f ` x ) e. B )
25 17 24 pm2.65da 
 |-  ( ( ( ph /\ f e. ( ( A \ B ) ^m C ) ) /\ x e. C ) -> -. f : C --> B )
26 25 ex 
 |-  ( ( ph /\ f e. ( ( A \ B ) ^m C ) ) -> ( x e. C -> -. f : C --> B ) )
27 26 exlimdv 
 |-  ( ( ph /\ f e. ( ( A \ B ) ^m C ) ) -> ( E. x x e. C -> -. f : C --> B ) )
28 13 27 mpd 
 |-  ( ( ph /\ f e. ( ( A \ B ) ^m C ) ) -> -. f : C --> B )
29 elmapg 
 |-  ( ( B e. W /\ C e. Z ) -> ( f e. ( B ^m C ) <-> f : C --> B ) )
30 2 3 29 syl2anc 
 |-  ( ph -> ( f e. ( B ^m C ) <-> f : C --> B ) )
31 30 adantr 
 |-  ( ( ph /\ f e. ( ( A \ B ) ^m C ) ) -> ( f e. ( B ^m C ) <-> f : C --> B ) )
32 28 31 mtbird 
 |-  ( ( ph /\ f e. ( ( A \ B ) ^m C ) ) -> -. f e. ( B ^m C ) )
33 10 32 eldifd 
 |-  ( ( ph /\ f e. ( ( A \ B ) ^m C ) ) -> f e. ( ( A ^m C ) \ ( B ^m C ) ) )
34 33 ralrimiva 
 |-  ( ph -> A. f e. ( ( A \ B ) ^m C ) f e. ( ( A ^m C ) \ ( B ^m C ) ) )
35 dfss3 
 |-  ( ( ( A \ B ) ^m C ) C_ ( ( A ^m C ) \ ( B ^m C ) ) <-> A. f e. ( ( A \ B ) ^m C ) f e. ( ( A ^m C ) \ ( B ^m C ) ) )
36 34 35 sylibr 
 |-  ( ph -> ( ( A \ B ) ^m C ) C_ ( ( A ^m C ) \ ( B ^m C ) ) )