Step |
Hyp |
Ref |
Expression |
0 |
|
ccau |
β’ Cau |
1 |
|
vd |
β’ π |
2 |
|
cxmet |
β’ βMet |
3 |
2
|
crn |
β’ ran βMet |
4 |
3
|
cuni |
β’ βͺ ran βMet |
5 |
|
vf |
β’ π |
6 |
1
|
cv |
β’ π |
7 |
6
|
cdm |
β’ dom π |
8 |
7
|
cdm |
β’ dom dom π |
9 |
|
cpm |
β’ βpm |
10 |
|
cc |
β’ β |
11 |
8 10 9
|
co |
β’ ( dom dom π βpm β ) |
12 |
|
vx |
β’ π₯ |
13 |
|
crp |
β’ β+ |
14 |
|
vj |
β’ π |
15 |
|
cz |
β’ β€ |
16 |
5
|
cv |
β’ π |
17 |
|
cuz |
β’ β€β₯ |
18 |
14
|
cv |
β’ π |
19 |
18 17
|
cfv |
β’ ( β€β₯ β π ) |
20 |
16 19
|
cres |
β’ ( π βΎ ( β€β₯ β π ) ) |
21 |
18 16
|
cfv |
β’ ( π β π ) |
22 |
|
cbl |
β’ ball |
23 |
6 22
|
cfv |
β’ ( ball β π ) |
24 |
12
|
cv |
β’ π₯ |
25 |
21 24 23
|
co |
β’ ( ( π β π ) ( ball β π ) π₯ ) |
26 |
19 25 20
|
wf |
β’ ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π ) π₯ ) |
27 |
26 14 15
|
wrex |
β’ β π β β€ ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π ) π₯ ) |
28 |
27 12 13
|
wral |
β’ β π₯ β β+ β π β β€ ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π ) π₯ ) |
29 |
28 5 11
|
crab |
β’ { π β ( dom dom π βpm β ) β£ β π₯ β β+ β π β β€ ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π ) π₯ ) } |
30 |
1 4 29
|
cmpt |
β’ ( π β βͺ ran βMet β¦ { π β ( dom dom π βpm β ) β£ β π₯ β β+ β π β β€ ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π ) π₯ ) } ) |
31 |
0 30
|
wceq |
β’ Cau = ( π β βͺ ran βMet β¦ { π β ( dom dom π βpm β ) β£ β π₯ β β+ β π β β€ ( π βΎ ( β€β₯ β π ) ) : ( β€β₯ β π ) βΆ ( ( π β π ) ( ball β π ) π₯ ) } ) |