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