Step |
Hyp |
Ref |
Expression |
1 |
|
fmucnd.1 |
|- ( ph -> U e. ( UnifOn ` X ) ) |
2 |
|
fmucnd.2 |
|- ( ph -> V e. ( UnifOn ` Y ) ) |
3 |
|
fmucnd.3 |
|- ( ph -> F e. ( U uCn V ) ) |
4 |
|
fmucnd.4 |
|- ( ph -> C e. ( CauFilU ` U ) ) |
5 |
|
fmucnd.5 |
|- D = ran ( a e. C |-> ( F " a ) ) |
6 |
|
cfilufbas |
|- ( ( U e. ( UnifOn ` X ) /\ C e. ( CauFilU ` U ) ) -> C e. ( fBas ` X ) ) |
7 |
1 4 6
|
syl2anc |
|- ( ph -> C e. ( fBas ` X ) ) |
8 |
|
isucn |
|- ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) -> ( F e. ( U uCn V ) <-> ( F : X --> Y /\ A. v e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) v ( F ` y ) ) ) ) ) |
9 |
8
|
simprbda |
|- ( ( ( U e. ( UnifOn ` X ) /\ V e. ( UnifOn ` Y ) ) /\ F e. ( U uCn V ) ) -> F : X --> Y ) |
10 |
1 2 3 9
|
syl21anc |
|- ( ph -> F : X --> Y ) |
11 |
2
|
elfvexd |
|- ( ph -> Y e. _V ) |
12 |
5
|
fbasrn |
|- ( ( C e. ( fBas ` X ) /\ F : X --> Y /\ Y e. _V ) -> D e. ( fBas ` Y ) ) |
13 |
7 10 11 12
|
syl3anc |
|- ( ph -> D e. ( fBas ` Y ) ) |
14 |
|
simplr |
|- ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> a e. C ) |
15 |
|
eqid |
|- ( F " a ) = ( F " a ) |
16 |
|
imaeq2 |
|- ( c = a -> ( F " c ) = ( F " a ) ) |
17 |
16
|
rspceeqv |
|- ( ( a e. C /\ ( F " a ) = ( F " a ) ) -> E. c e. C ( F " a ) = ( F " c ) ) |
18 |
14 15 17
|
sylancl |
|- ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> E. c e. C ( F " a ) = ( F " c ) ) |
19 |
|
imaexg |
|- ( F e. ( U uCn V ) -> ( F " a ) e. _V ) |
20 |
|
eqid |
|- ( c e. C |-> ( F " c ) ) = ( c e. C |-> ( F " c ) ) |
21 |
20
|
elrnmpt |
|- ( ( F " a ) e. _V -> ( ( F " a ) e. ran ( c e. C |-> ( F " c ) ) <-> E. c e. C ( F " a ) = ( F " c ) ) ) |
22 |
3 19 21
|
3syl |
|- ( ph -> ( ( F " a ) e. ran ( c e. C |-> ( F " c ) ) <-> E. c e. C ( F " a ) = ( F " c ) ) ) |
23 |
22
|
ad3antrrr |
|- ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> ( ( F " a ) e. ran ( c e. C |-> ( F " c ) ) <-> E. c e. C ( F " a ) = ( F " c ) ) ) |
24 |
18 23
|
mpbird |
|- ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> ( F " a ) e. ran ( c e. C |-> ( F " c ) ) ) |
25 |
|
imaeq2 |
|- ( a = c -> ( F " a ) = ( F " c ) ) |
26 |
25
|
cbvmptv |
|- ( a e. C |-> ( F " a ) ) = ( c e. C |-> ( F " c ) ) |
27 |
26
|
rneqi |
|- ran ( a e. C |-> ( F " a ) ) = ran ( c e. C |-> ( F " c ) ) |
28 |
5 27
|
eqtri |
|- D = ran ( c e. C |-> ( F " c ) ) |
29 |
24 28
|
eleqtrrdi |
|- ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> ( F " a ) e. D ) |
30 |
10
|
ffnd |
|- ( ph -> F Fn X ) |
31 |
30
|
ad3antrrr |
|- ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> F Fn X ) |
32 |
|
fbelss |
|- ( ( C e. ( fBas ` X ) /\ a e. C ) -> a C_ X ) |
33 |
7 32
|
sylan |
|- ( ( ph /\ a e. C ) -> a C_ X ) |
34 |
33
|
ad4ant13 |
|- ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> a C_ X ) |
35 |
|
fmucndlem |
|- ( ( F Fn X /\ a C_ X ) -> ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " ( a X. a ) ) = ( ( F " a ) X. ( F " a ) ) ) |
36 |
31 34 35
|
syl2anc |
|- ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " ( a X. a ) ) = ( ( F " a ) X. ( F " a ) ) ) |
37 |
|
eqid |
|- ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) = ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) |
38 |
37
|
mpofun |
|- Fun ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) |
39 |
|
funimass2 |
|- ( ( Fun ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " ( a X. a ) ) C_ v ) |
40 |
38 39
|
mpan |
|- ( ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) -> ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " ( a X. a ) ) C_ v ) |
41 |
40
|
adantl |
|- ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " ( a X. a ) ) C_ v ) |
42 |
36 41
|
eqsstrrd |
|- ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> ( ( F " a ) X. ( F " a ) ) C_ v ) |
43 |
|
id |
|- ( b = ( F " a ) -> b = ( F " a ) ) |
44 |
43
|
sqxpeqd |
|- ( b = ( F " a ) -> ( b X. b ) = ( ( F " a ) X. ( F " a ) ) ) |
45 |
44
|
sseq1d |
|- ( b = ( F " a ) -> ( ( b X. b ) C_ v <-> ( ( F " a ) X. ( F " a ) ) C_ v ) ) |
46 |
45
|
rspcev |
|- ( ( ( F " a ) e. D /\ ( ( F " a ) X. ( F " a ) ) C_ v ) -> E. b e. D ( b X. b ) C_ v ) |
47 |
29 42 46
|
syl2anc |
|- ( ( ( ( ph /\ v e. V ) /\ a e. C ) /\ ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) -> E. b e. D ( b X. b ) C_ v ) |
48 |
1
|
adantr |
|- ( ( ph /\ v e. V ) -> U e. ( UnifOn ` X ) ) |
49 |
4
|
adantr |
|- ( ( ph /\ v e. V ) -> C e. ( CauFilU ` U ) ) |
50 |
2
|
adantr |
|- ( ( ph /\ v e. V ) -> V e. ( UnifOn ` Y ) ) |
51 |
3
|
adantr |
|- ( ( ph /\ v e. V ) -> F e. ( U uCn V ) ) |
52 |
|
simpr |
|- ( ( ph /\ v e. V ) -> v e. V ) |
53 |
|
nfcv |
|- F/_ s <. ( F ` x ) , ( F ` y ) >. |
54 |
|
nfcv |
|- F/_ t <. ( F ` x ) , ( F ` y ) >. |
55 |
|
nfcv |
|- F/_ x <. ( F ` s ) , ( F ` t ) >. |
56 |
|
nfcv |
|- F/_ y <. ( F ` s ) , ( F ` t ) >. |
57 |
|
simpl |
|- ( ( x = s /\ y = t ) -> x = s ) |
58 |
57
|
fveq2d |
|- ( ( x = s /\ y = t ) -> ( F ` x ) = ( F ` s ) ) |
59 |
|
simpr |
|- ( ( x = s /\ y = t ) -> y = t ) |
60 |
59
|
fveq2d |
|- ( ( x = s /\ y = t ) -> ( F ` y ) = ( F ` t ) ) |
61 |
58 60
|
opeq12d |
|- ( ( x = s /\ y = t ) -> <. ( F ` x ) , ( F ` y ) >. = <. ( F ` s ) , ( F ` t ) >. ) |
62 |
53 54 55 56 61
|
cbvmpo |
|- ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) = ( s e. X , t e. X |-> <. ( F ` s ) , ( F ` t ) >. ) |
63 |
48 50 51 52 62
|
ucnprima |
|- ( ( ph /\ v e. V ) -> ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) e. U ) |
64 |
|
cfiluexsm |
|- ( ( U e. ( UnifOn ` X ) /\ C e. ( CauFilU ` U ) /\ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) e. U ) -> E. a e. C ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) |
65 |
48 49 63 64
|
syl3anc |
|- ( ( ph /\ v e. V ) -> E. a e. C ( a X. a ) C_ ( `' ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " v ) ) |
66 |
47 65
|
r19.29a |
|- ( ( ph /\ v e. V ) -> E. b e. D ( b X. b ) C_ v ) |
67 |
66
|
ralrimiva |
|- ( ph -> A. v e. V E. b e. D ( b X. b ) C_ v ) |
68 |
|
iscfilu |
|- ( V e. ( UnifOn ` Y ) -> ( D e. ( CauFilU ` V ) <-> ( D e. ( fBas ` Y ) /\ A. v e. V E. b e. D ( b X. b ) C_ v ) ) ) |
69 |
2 68
|
syl |
|- ( ph -> ( D e. ( CauFilU ` V ) <-> ( D e. ( fBas ` Y ) /\ A. v e. V E. b e. D ( b X. b ) C_ v ) ) ) |
70 |
13 67 69
|
mpbir2and |
|- ( ph -> D e. ( CauFilU ` V ) ) |