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