Metamath Proof Explorer


Theorem unirnmap

Description: Given a subset of a set exponentiation, the base set can be restricted. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses unirnmap.a
|- ( ph -> A e. V )
unirnmap.x
|- ( ph -> X C_ ( B ^m A ) )
Assertion unirnmap
|- ( ph -> X C_ ( ran U. X ^m A ) )

Proof

Step Hyp Ref Expression
1 unirnmap.a
 |-  ( ph -> A e. V )
2 unirnmap.x
 |-  ( ph -> X C_ ( B ^m A ) )
3 2 sselda
 |-  ( ( ph /\ g e. X ) -> g e. ( B ^m A ) )
4 elmapfn
 |-  ( g e. ( B ^m A ) -> g Fn A )
5 3 4 syl
 |-  ( ( ph /\ g e. X ) -> g Fn A )
6 simplr
 |-  ( ( ( ph /\ g e. X ) /\ x e. A ) -> g e. X )
7 dffn3
 |-  ( g Fn A <-> g : A --> ran g )
8 5 7 sylib
 |-  ( ( ph /\ g e. X ) -> g : A --> ran g )
9 8 ffvelrnda
 |-  ( ( ( ph /\ g e. X ) /\ x e. A ) -> ( g ` x ) e. ran g )
10 rneq
 |-  ( f = g -> ran f = ran g )
11 10 eleq2d
 |-  ( f = g -> ( ( g ` x ) e. ran f <-> ( g ` x ) e. ran g ) )
12 11 rspcev
 |-  ( ( g e. X /\ ( g ` x ) e. ran g ) -> E. f e. X ( g ` x ) e. ran f )
13 6 9 12 syl2anc
 |-  ( ( ( ph /\ g e. X ) /\ x e. A ) -> E. f e. X ( g ` x ) e. ran f )
14 eliun
 |-  ( ( g ` x ) e. U_ f e. X ran f <-> E. f e. X ( g ` x ) e. ran f )
15 13 14 sylibr
 |-  ( ( ( ph /\ g e. X ) /\ x e. A ) -> ( g ` x ) e. U_ f e. X ran f )
16 rnuni
 |-  ran U. X = U_ f e. X ran f
17 15 16 eleqtrrdi
 |-  ( ( ( ph /\ g e. X ) /\ x e. A ) -> ( g ` x ) e. ran U. X )
18 17 ralrimiva
 |-  ( ( ph /\ g e. X ) -> A. x e. A ( g ` x ) e. ran U. X )
19 5 18 jca
 |-  ( ( ph /\ g e. X ) -> ( g Fn A /\ A. x e. A ( g ` x ) e. ran U. X ) )
20 ffnfv
 |-  ( g : A --> ran U. X <-> ( g Fn A /\ A. x e. A ( g ` x ) e. ran U. X ) )
21 19 20 sylibr
 |-  ( ( ph /\ g e. X ) -> g : A --> ran U. X )
22 ovexd
 |-  ( ph -> ( B ^m A ) e. _V )
23 22 2 ssexd
 |-  ( ph -> X e. _V )
24 23 uniexd
 |-  ( ph -> U. X e. _V )
25 rnexg
 |-  ( U. X e. _V -> ran U. X e. _V )
26 24 25 syl
 |-  ( ph -> ran U. X e. _V )
27 26 1 elmapd
 |-  ( ph -> ( g e. ( ran U. X ^m A ) <-> g : A --> ran U. X ) )
28 27 adantr
 |-  ( ( ph /\ g e. X ) -> ( g e. ( ran U. X ^m A ) <-> g : A --> ran U. X ) )
29 21 28 mpbird
 |-  ( ( ph /\ g e. X ) -> g e. ( ran U. X ^m A ) )
30 29 ralrimiva
 |-  ( ph -> A. g e. X g e. ( ran U. X ^m A ) )
31 dfss3
 |-  ( X C_ ( ran U. X ^m A ) <-> A. g e. X g e. ( ran U. X ^m A ) )
32 30 31 sylibr
 |-  ( ph -> X C_ ( ran U. X ^m A ) )