Metamath Proof Explorer

Theorem iunmapsn

Description: The indexed union of set exponentiations to a singleton is equal to the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses iunmapsn.x 
|- F/ x ph
iunmapsn.a 
|- ( ph -> A e. V )
iunmapsn.b 
|- ( ( ph /\ x e. A ) -> B e. W )
iunmapsn.c 
|- ( ph -> C e. Z )
Assertion iunmapsn 
|- ( ph -> U_ x e. A ( B ^m { C } ) = ( U_ x e. A B ^m { C } ) )

Proof

Step Hyp Ref Expression
1 iunmapsn.x 
 |-  F/ x ph
2 iunmapsn.a 
 |-  ( ph -> A e. V )
3 iunmapsn.b 
 |-  ( ( ph /\ x e. A ) -> B e. W )
4 iunmapsn.c 
 |-  ( ph -> C e. Z )
5 1 2 3 iunmapss 
 |-  ( ph -> U_ x e. A ( B ^m { C } ) C_ ( U_ x e. A B ^m { C } ) )
6 simpr 
 |-  ( ( ph /\ f e. ( U_ x e. A B ^m { C } ) ) -> f e. ( U_ x e. A B ^m { C } ) )
7 3 ex 
 |-  ( ph -> ( x e. A -> B e. W ) )
8 1 7 ralrimi 
 |-  ( ph -> A. x e. A B e. W )
9 iunexg 
 |-  ( ( A e. V /\ A. x e. A B e. W ) -> U_ x e. A B e. _V )
10 2 8 9 syl2anc 
 |-  ( ph -> U_ x e. A B e. _V )
11 10 4 mapsnd 
 |-  ( ph -> ( U_ x e. A B ^m { C } ) = { f | E. y e. U_ x e. A B f = { <. C , y >. } } )
12 11 adantr 
 |-  ( ( ph /\ f e. ( U_ x e. A B ^m { C } ) ) -> ( U_ x e. A B ^m { C } ) = { f | E. y e. U_ x e. A B f = { <. C , y >. } } )
13 6 12 eleqtrd 
 |-  ( ( ph /\ f e. ( U_ x e. A B ^m { C } ) ) -> f e. { f | E. y e. U_ x e. A B f = { <. C , y >. } } )
14 abid 
 |-  ( f e. { f | E. y e. U_ x e. A B f = { <. C , y >. } } <-> E. y e. U_ x e. A B f = { <. C , y >. } )
15 13 14 sylib 
 |-  ( ( ph /\ f e. ( U_ x e. A B ^m { C } ) ) -> E. y e. U_ x e. A B f = { <. C , y >. } )
16 eliun 
 |-  ( y e. U_ x e. A B <-> E. x e. A y e. B )
17 16 biimpi 
 |-  ( y e. U_ x e. A B -> E. x e. A y e. B )
18 17 3ad2ant2 
 |-  ( ( ph /\ y e. U_ x e. A B /\ f = { <. C , y >. } ) -> E. x e. A y e. B )
19 nfcv 
 |-  F/_ x y
20 nfiu1 
 |-  F/_ x U_ x e. A B
21 19 20 nfel 
 |-  F/ x y e. U_ x e. A B
22 nfv 
 |-  F/ x f = { <. C , y >. }
23 1 21 22 nf3an 
 |-  F/ x ( ph /\ y e. U_ x e. A B /\ f = { <. C , y >. } )
24 rspe 
 |-  ( ( y e. B /\ f = { <. C , y >. } ) -> E. y e. B f = { <. C , y >. } )
25 24 ancoms 
 |-  ( ( f = { <. C , y >. } /\ y e. B ) -> E. y e. B f = { <. C , y >. } )
26 abid 
 |-  ( f e. { f | E. y e. B f = { <. C , y >. } } <-> E. y e. B f = { <. C , y >. } )
27 25 26 sylibr 
 |-  ( ( f = { <. C , y >. } /\ y e. B ) -> f e. { f | E. y e. B f = { <. C , y >. } } )
28 27 adantll 
 |-  ( ( ( ph /\ f = { <. C , y >. } ) /\ y e. B ) -> f e. { f | E. y e. B f = { <. C , y >. } } )
29 28 3adant2 
 |-  ( ( ( ph /\ f = { <. C , y >. } ) /\ x e. A /\ y e. B ) -> f e. { f | E. y e. B f = { <. C , y >. } } )
30 4 adantr 
 |-  ( ( ph /\ x e. A ) -> C e. Z )
31 3 30 mapsnd 
 |-  ( ( ph /\ x e. A ) -> ( B ^m { C } ) = { f | E. y e. B f = { <. C , y >. } } )
32 31 eqcomd 
 |-  ( ( ph /\ x e. A ) -> { f | E. y e. B f = { <. C , y >. } } = ( B ^m { C } ) )
33 32 3adant3 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> { f | E. y e. B f = { <. C , y >. } } = ( B ^m { C } ) )
34 33 3adant1r 
 |-  ( ( ( ph /\ f = { <. C , y >. } ) /\ x e. A /\ y e. B ) -> { f | E. y e. B f = { <. C , y >. } } = ( B ^m { C } ) )
35 29 34 eleqtrd 
 |-  ( ( ( ph /\ f = { <. C , y >. } ) /\ x e. A /\ y e. B ) -> f e. ( B ^m { C } ) )
36 35 3exp 
 |-  ( ( ph /\ f = { <. C , y >. } ) -> ( x e. A -> ( y e. B -> f e. ( B ^m { C } ) ) ) )
37 36 3adant2 
 |-  ( ( ph /\ y e. U_ x e. A B /\ f = { <. C , y >. } ) -> ( x e. A -> ( y e. B -> f e. ( B ^m { C } ) ) ) )
38 23 37 reximdai 
 |-  ( ( ph /\ y e. U_ x e. A B /\ f = { <. C , y >. } ) -> ( E. x e. A y e. B -> E. x e. A f e. ( B ^m { C } ) ) )
39 18 38 mpd 
 |-  ( ( ph /\ y e. U_ x e. A B /\ f = { <. C , y >. } ) -> E. x e. A f e. ( B ^m { C } ) )
40 39 3exp 
 |-  ( ph -> ( y e. U_ x e. A B -> ( f = { <. C , y >. } -> E. x e. A f e. ( B ^m { C } ) ) ) )
41 40 rexlimdv 
 |-  ( ph -> ( E. y e. U_ x e. A B f = { <. C , y >. } -> E. x e. A f e. ( B ^m { C } ) ) )
42 41 adantr 
 |-  ( ( ph /\ f e. ( U_ x e. A B ^m { C } ) ) -> ( E. y e. U_ x e. A B f = { <. C , y >. } -> E. x e. A f e. ( B ^m { C } ) ) )
43 15 42 mpd 
 |-  ( ( ph /\ f e. ( U_ x e. A B ^m { C } ) ) -> E. x e. A f e. ( B ^m { C } ) )
44 eliun 
 |-  ( f e. U_ x e. A ( B ^m { C } ) <-> E. x e. A f e. ( B ^m { C } ) )
45 43 44 sylibr 
 |-  ( ( ph /\ f e. ( U_ x e. A B ^m { C } ) ) -> f e. U_ x e. A ( B ^m { C } ) )
46 5 45 eqelssd 
 |-  ( ph -> U_ x e. A ( B ^m { C } ) = ( U_ x e. A B ^m { C } ) )