Step |
Hyp |
Ref |
Expression |
1 |
|
ucnval |
|- ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( U uCn V ) = { f e. ( Y ^m X ) | A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( f ` x ) s ( f ` y ) ) } ) |
2 |
1
|
eleq2d |
|- ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( F e. ( U uCn V ) <-> F e. { f e. ( Y ^m X ) | A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( f ` x ) s ( f ` y ) ) } ) ) |
3 |
|
fveq1 |
|- ( f = F -> ( f ` x ) = ( F ` x ) ) |
4 |
|
fveq1 |
|- ( f = F -> ( f ` y ) = ( F ` y ) ) |
5 |
3 4
|
breq12d |
|- ( f = F -> ( ( f ` x ) s ( f ` y ) <-> ( F ` x ) s ( F ` y ) ) ) |
6 |
5
|
imbi2d |
|- ( f = F -> ( ( x r y -> ( f ` x ) s ( f ` y ) ) <-> ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) |
7 |
6
|
ralbidv |
|- ( f = F -> ( A. y e. X ( x r y -> ( f ` x ) s ( f ` y ) ) <-> A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) |
8 |
7
|
rexralbidv |
|- ( f = F -> ( E. r e. U A. x e. X A. y e. X ( x r y -> ( f ` x ) s ( f ` y ) ) <-> E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) |
9 |
8
|
ralbidv |
|- ( f = F -> ( A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( f ` x ) s ( f ` y ) ) <-> A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) |
10 |
9
|
elrab |
|- ( F e. { f e. ( Y ^m X ) | A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( f ` x ) s ( f ` y ) ) } <-> ( F e. ( Y ^m X ) /\ A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) |
11 |
2 10
|
bitrdi |
|- ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( F e. ( U uCn V ) <-> ( F e. ( Y ^m X ) /\ A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) ) |
12 |
|
elfvex |
|- ( V e. ( UnifOn ` Y ) -> Y e. _V ) |
13 |
|
elfvex |
|- ( U e. ( UnifOn ` X ) -> X e. _V ) |
14 |
|
elmapg |
|- ( ( Y e. _V /\ X e. _V ) -> ( F e. ( Y ^m X ) <-> F : X --> Y ) ) |
15 |
12 13 14
|
syl2anr |
|- ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( F e. ( Y ^m X ) <-> F : X --> Y ) ) |
16 |
15
|
anbi1d |
|- ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( ( F e. ( Y ^m X ) /\ A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) <-> ( F : X --> Y /\ A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) ) |
17 |
11 16
|
bitrd |
|- ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( F e. ( U uCn V ) <-> ( F : X --> Y /\ A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) ) |