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