Step |
Hyp |
Ref |
Expression |
1 |
|
df-cau |
β’ Cau = ( π β βͺ ran βMet β¦ { π β ( dom dom π βpm β ) β£ β π₯ β β+ β π β β€ ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π ) π₯ ) } ) |
2 |
|
dmeq |
β’ ( π = π· β dom π = dom π· ) |
3 |
2
|
dmeqd |
β’ ( π = π· β dom dom π = dom dom π· ) |
4 |
|
xmetf |
β’ ( π· β ( βMet β π ) β π· : ( π Γ π ) βΆ β* ) |
5 |
4
|
fdmd |
β’ ( π· β ( βMet β π ) β dom π· = ( π Γ π ) ) |
6 |
5
|
dmeqd |
β’ ( π· β ( βMet β π ) β dom dom π· = dom ( π Γ π ) ) |
7 |
|
dmxpid |
β’ dom ( π Γ π ) = π |
8 |
6 7
|
eqtrdi |
β’ ( π· β ( βMet β π ) β dom dom π· = π ) |
9 |
3 8
|
sylan9eqr |
β’ ( ( π· β ( βMet β π ) β§ π = π· ) β dom dom π = π ) |
10 |
9
|
oveq1d |
β’ ( ( π· β ( βMet β π ) β§ π = π· ) β ( dom dom π βpm β ) = ( π βpm β ) ) |
11 |
|
simpr |
β’ ( ( π· β ( βMet β π ) β§ π = π· ) β π = π· ) |
12 |
11
|
fveq2d |
β’ ( ( π· β ( βMet β π ) β§ π = π· ) β ( ball β π ) = ( ball β π· ) ) |
13 |
12
|
oveqd |
β’ ( ( π· β ( βMet β π ) β§ π = π· ) β ( ( π β π ) ( ball β π ) π₯ ) = ( ( π β π ) ( ball β π· ) π₯ ) ) |
14 |
13
|
feq3d |
β’ ( ( π· β ( βMet β π ) β§ π = π· ) β ( ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π ) π₯ ) β ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π· ) π₯ ) ) ) |
15 |
14
|
rexbidv |
β’ ( ( π· β ( βMet β π ) β§ π = π· ) β ( β π β β€ ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π ) π₯ ) β β π β β€ ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π· ) π₯ ) ) ) |
16 |
15
|
ralbidv |
β’ ( ( π· β ( βMet β π ) β§ π = π· ) β ( β π₯ β β+ β π β β€ ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π ) π₯ ) β β π₯ β β+ β π β β€ ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π· ) π₯ ) ) ) |
17 |
10 16
|
rabeqbidv |
β’ ( ( π· β ( βMet β π ) β§ π = π· ) β { π β ( dom dom π βpm β ) β£ β π₯ β β+ β π β β€ ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π ) π₯ ) } = { π β ( π βpm β ) β£ β π₯ β β+ β π β β€ ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π· ) π₯ ) } ) |
18 |
|
fvssunirn |
β’ ( βMet β π ) β βͺ ran βMet |
19 |
18
|
sseli |
β’ ( π· β ( βMet β π ) β π· β βͺ ran βMet ) |
20 |
|
ovex |
β’ ( π βpm β ) β V |
21 |
20
|
rabex |
β’ { π β ( π βpm β ) β£ β π₯ β β+ β π β β€ ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π· ) π₯ ) } β V |
22 |
21
|
a1i |
β’ ( π· β ( βMet β π ) β { π β ( π βpm β ) β£ β π₯ β β+ β π β β€ ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π· ) π₯ ) } β V ) |
23 |
1 17 19 22
|
fvmptd2 |
β’ ( π· β ( βMet β π ) β ( Cau β π· ) = { π β ( π βpm β ) β£ β π₯ β β+ β π β β€ ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π· ) π₯ ) } ) |