Metamath Proof Explorer

Theorem mapss2

Description: Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021)

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

Proof

Step Hyp Ref Expression
1 mapss2.a 
 |-  ( ph -> A e. V )
2 mapss2.b 
 |-  ( ph -> B e. W )
3 mapss2.c 
 |-  ( ph -> C e. Z )
4 mapss2.n 
 |-  ( ph -> C =/= (/) )
5 2 adantr 
 |-  ( ( ph /\ A C_ B ) -> B e. W )
6 simpr 
 |-  ( ( ph /\ A C_ B ) -> A C_ B )
7 mapss 
 |-  ( ( B e. W /\ A C_ B ) -> ( A ^m C ) C_ ( B ^m C ) )
8 5 6 7 syl2anc 
 |-  ( ( ph /\ A C_ B ) -> ( A ^m C ) C_ ( B ^m C ) )
9 8 ex 
 |-  ( ph -> ( A C_ B -> ( A ^m C ) C_ ( B ^m C ) ) )
10 n0 
 |-  ( C =/= (/) <-> E. x x e. C )
11 4 10 sylib 
 |-  ( ph -> E. x x e. C )
12 11 adantr 
 |-  ( ( ph /\ ( A ^m C ) C_ ( B ^m C ) ) -> E. x x e. C )
13 eqidd 
 |-  ( ( ph /\ x e. C ) -> ( w e. C |-> y ) = ( w e. C |-> y ) )
14 eqidd 
 |-  ( ( ( ph /\ x e. C ) /\ w = x ) -> y = y )
15 simpr 
 |-  ( ( ph /\ x e. C ) -> x e. C )
16 vex 
 |-  y e. _V
17 16 a1i 
 |-  ( ( ph /\ x e. C ) -> y e. _V )
18 13 14 15 17 fvmptd 
 |-  ( ( ph /\ x e. C ) -> ( ( w e. C |-> y ) ` x ) = y )
19 18 eqcomd 
 |-  ( ( ph /\ x e. C ) -> y = ( ( w e. C |-> y ) ` x ) )
20 19 ad4ant13 
 |-  ( ( ( ( ph /\ ( A ^m C ) C_ ( B ^m C ) ) /\ x e. C ) /\ y e. A ) -> y = ( ( w e. C |-> y ) ` x ) )
21 simplr 
 |-  ( ( ( ph /\ ( A ^m C ) C_ ( B ^m C ) ) /\ y e. A ) -> ( A ^m C ) C_ ( B ^m C ) )
22 simplr 
 |-  ( ( ( ph /\ y e. A ) /\ w e. C ) -> y e. A )
23 22 fmpttd 
 |-  ( ( ph /\ y e. A ) -> ( w e. C |-> y ) : C --> A )
24 1 adantr 
 |-  ( ( ph /\ y e. A ) -> A e. V )
25 3 adantr 
 |-  ( ( ph /\ y e. A ) -> C e. Z )
26 24 25 elmapd 
 |-  ( ( ph /\ y e. A ) -> ( ( w e. C |-> y ) e. ( A ^m C ) <-> ( w e. C |-> y ) : C --> A ) )
27 23 26 mpbird 
 |-  ( ( ph /\ y e. A ) -> ( w e. C |-> y ) e. ( A ^m C ) )
28 27 adantlr 
 |-  ( ( ( ph /\ ( A ^m C ) C_ ( B ^m C ) ) /\ y e. A ) -> ( w e. C |-> y ) e. ( A ^m C ) )
29 21 28 sseldd 
 |-  ( ( ( ph /\ ( A ^m C ) C_ ( B ^m C ) ) /\ y e. A ) -> ( w e. C |-> y ) e. ( B ^m C ) )
30 elmapi 
 |-  ( ( w e. C |-> y ) e. ( B ^m C ) -> ( w e. C |-> y ) : C --> B )
31 29 30 syl 
 |-  ( ( ( ph /\ ( A ^m C ) C_ ( B ^m C ) ) /\ y e. A ) -> ( w e. C |-> y ) : C --> B )
32 31 adantlr 
 |-  ( ( ( ( ph /\ ( A ^m C ) C_ ( B ^m C ) ) /\ x e. C ) /\ y e. A ) -> ( w e. C |-> y ) : C --> B )
33 simplr 
 |-  ( ( ( ( ph /\ ( A ^m C ) C_ ( B ^m C ) ) /\ x e. C ) /\ y e. A ) -> x e. C )
34 32 33 ffvelrnd 
 |-  ( ( ( ( ph /\ ( A ^m C ) C_ ( B ^m C ) ) /\ x e. C ) /\ y e. A ) -> ( ( w e. C |-> y ) ` x ) e. B )
35 20 34 eqeltrd 
 |-  ( ( ( ( ph /\ ( A ^m C ) C_ ( B ^m C ) ) /\ x e. C ) /\ y e. A ) -> y e. B )
36 35 ralrimiva 
 |-  ( ( ( ph /\ ( A ^m C ) C_ ( B ^m C ) ) /\ x e. C ) -> A. y e. A y e. B )
37 dfss3 
 |-  ( A C_ B <-> A. y e. A y e. B )
38 36 37 sylibr 
 |-  ( ( ( ph /\ ( A ^m C ) C_ ( B ^m C ) ) /\ x e. C ) -> A C_ B )
39 38 ex 
 |-  ( ( ph /\ ( A ^m C ) C_ ( B ^m C ) ) -> ( x e. C -> A C_ B ) )
40 39 exlimdv 
 |-  ( ( ph /\ ( A ^m C ) C_ ( B ^m C ) ) -> ( E. x x e. C -> A C_ B ) )
41 12 40 mpd 
 |-  ( ( ph /\ ( A ^m C ) C_ ( B ^m C ) ) -> A C_ B )
42 41 ex 
 |-  ( ph -> ( ( A ^m C ) C_ ( B ^m C ) -> A C_ B ) )
43 9 42 impbid 
 |-  ( ph -> ( A C_ B <-> ( A ^m C ) C_ ( B ^m C ) ) )