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