Metamath Proof Explorer

Theorem inmap

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

Ref Expression
Hypotheses inmap.a 
|- ( ph -> A e. V )
inmap.b 
|- ( ph -> B e. W )
inmap.c 
|- ( ph -> C e. Z )
Assertion inmap 
|- ( ph -> ( ( A ^m C ) i^i ( B ^m C ) ) = ( ( A i^i B ) ^m C ) )

Proof

Step Hyp Ref Expression
1 inmap.a 
 |-  ( ph -> A e. V )
2 inmap.b 
 |-  ( ph -> B e. W )
3 inmap.c 
 |-  ( ph -> C e. Z )
4 elinel1 
 |-  ( f e. ( ( A ^m C ) i^i ( B ^m C ) ) -> f e. ( A ^m C ) )
5 elmapi 
 |-  ( f e. ( A ^m C ) -> f : C --> A )
6 4 5 syl 
 |-  ( f e. ( ( A ^m C ) i^i ( B ^m C ) ) -> f : C --> A )
7 elinel2 
 |-  ( f e. ( ( A ^m C ) i^i ( B ^m C ) ) -> f e. ( B ^m C ) )
8 elmapi 
 |-  ( f e. ( B ^m C ) -> f : C --> B )
9 7 8 syl 
 |-  ( f e. ( ( A ^m C ) i^i ( B ^m C ) ) -> f : C --> B )
10 6 9 jca 
 |-  ( f e. ( ( A ^m C ) i^i ( B ^m C ) ) -> ( f : C --> A /\ f : C --> B ) )
11 fin 
 |-  ( f : C --> ( A i^i B ) <-> ( f : C --> A /\ f : C --> B ) )
12 10 11 sylibr 
 |-  ( f e. ( ( A ^m C ) i^i ( B ^m C ) ) -> f : C --> ( A i^i B ) )
13 12 adantl 
 |-  ( ( ph /\ f e. ( ( A ^m C ) i^i ( B ^m C ) ) ) -> f : C --> ( A i^i B ) )
14 inss1 
 |-  ( A i^i B ) C_ A
15 14 a1i 
 |-  ( ph -> ( A i^i B ) C_ A )
16 1 15 ssexd 
 |-  ( ph -> ( A i^i B ) e. _V )
17 16 3 elmapd 
 |-  ( ph -> ( f e. ( ( A i^i B ) ^m C ) <-> f : C --> ( A i^i B ) ) )
18 17 adantr 
 |-  ( ( ph /\ f e. ( ( A ^m C ) i^i ( B ^m C ) ) ) -> ( f e. ( ( A i^i B ) ^m C ) <-> f : C --> ( A i^i B ) ) )
19 13 18 mpbird 
 |-  ( ( ph /\ f e. ( ( A ^m C ) i^i ( B ^m C ) ) ) -> f e. ( ( A i^i B ) ^m C ) )
20 19 ralrimiva 
 |-  ( ph -> A. f e. ( ( A ^m C ) i^i ( B ^m C ) ) f e. ( ( A i^i B ) ^m C ) )
21 dfss3 
 |-  ( ( ( A ^m C ) i^i ( B ^m C ) ) C_ ( ( A i^i B ) ^m C ) <-> A. f e. ( ( A ^m C ) i^i ( B ^m C ) ) f e. ( ( A i^i B ) ^m C ) )
22 20 21 sylibr 
 |-  ( ph -> ( ( A ^m C ) i^i ( B ^m C ) ) C_ ( ( A i^i B ) ^m C ) )
23 mapss 
 |-  ( ( A e. V /\ ( A i^i B ) C_ A ) -> ( ( A i^i B ) ^m C ) C_ ( A ^m C ) )
24 1 15 23 syl2anc 
 |-  ( ph -> ( ( A i^i B ) ^m C ) C_ ( A ^m C ) )
25 inss2 
 |-  ( A i^i B ) C_ B
26 25 a1i 
 |-  ( ph -> ( A i^i B ) C_ B )
27 mapss 
 |-  ( ( B e. W /\ ( A i^i B ) C_ B ) -> ( ( A i^i B ) ^m C ) C_ ( B ^m C ) )
28 2 26 27 syl2anc 
 |-  ( ph -> ( ( A i^i B ) ^m C ) C_ ( B ^m C ) )
29 24 28 ssind 
 |-  ( ph -> ( ( A i^i B ) ^m C ) C_ ( ( A ^m C ) i^i ( B ^m C ) ) )
30 22 29 eqssd 
 |-  ( ph -> ( ( A ^m C ) i^i ( B ^m C ) ) = ( ( A i^i B ) ^m C ) )