Step |
Hyp |
Ref |
Expression |
1 |
|
caucfil.1 |
β’ π = ( β€β₯ β π ) |
2 |
|
caucfil.2 |
β’ πΏ = ( ( π FilMap πΉ ) β ( β€β₯ β π ) ) |
3 |
|
df-3an |
β’ ( ( π β dom πΉ β§ ( πΉ β π ) β π β§ β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β ( ( π β dom πΉ β§ ( πΉ β π ) β π ) β§ β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
4 |
1
|
uztrn2 |
β’ ( ( π β π β§ π β ( β€β₯ β π ) ) β π β π ) |
5 |
4
|
adantll |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ π β ( β€β₯ β π ) ) β π β π ) |
6 |
|
simpll3 |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ π β ( β€β₯ β π ) ) β πΉ : π βΆ π ) |
7 |
6
|
fdmd |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ π β ( β€β₯ β π ) ) β dom πΉ = π ) |
8 |
5 7
|
eleqtrrd |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ π β ( β€β₯ β π ) ) β π β dom πΉ ) |
9 |
6 5
|
ffvelcdmd |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ π β ( β€β₯ β π ) ) β ( πΉ β π ) β π ) |
10 |
8 9
|
jca |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ π β ( β€β₯ β π ) ) β ( π β dom πΉ β§ ( πΉ β π ) β π ) ) |
11 |
10
|
biantrurd |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ π β ( β€β₯ β π ) ) β ( β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ β ( ( π β dom πΉ β§ ( πΉ β π ) β π ) β§ β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) |
12 |
|
uzss |
β’ ( π β ( β€β₯ β π ) β ( β€β₯ β π ) β ( β€β₯ β π ) ) |
13 |
12
|
adantl |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ π β ( β€β₯ β π ) ) β ( β€β₯ β π ) β ( β€β₯ β π ) ) |
14 |
13
|
sseld |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ π β ( β€β₯ β π ) ) β ( π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ) ) |
15 |
14
|
pm4.71rd |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ π β ( β€β₯ β π ) ) β ( π β ( β€β₯ β π ) β ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) ) ) |
16 |
15
|
imbi1d |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ π β ( β€β₯ β π ) ) β ( ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β ( ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) |
17 |
|
impexp |
β’ ( ( ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β ( π β ( β€β₯ β π ) β ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) |
18 |
16 17
|
bitrdi |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ π β ( β€β₯ β π ) ) β ( ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β ( π β ( β€β₯ β π ) β ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) ) |
19 |
18
|
ralbidv2 |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ π β ( β€β₯ β π ) ) β ( β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ β β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) |
20 |
11 19
|
bitr3d |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ π β ( β€β₯ β π ) ) β ( ( ( π β dom πΉ β§ ( πΉ β π ) β π ) β§ β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) |
21 |
3 20
|
bitrid |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ π β ( β€β₯ β π ) ) β ( ( π β dom πΉ β§ ( πΉ β π ) β π β§ β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) |
22 |
21
|
ralbidva |
β’ ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β ( β π β ( β€β₯ β π ) ( π β dom πΉ β§ ( πΉ β π ) β π β§ β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) |
23 |
|
r19.26-2 |
β’ ( β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β§ ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) β ( β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β§ β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) |
24 |
|
eleq1w |
β’ ( π’ = π β ( π’ β ( β€β₯ β π ) β π β ( β€β₯ β π ) ) ) |
25 |
|
fveq2 |
β’ ( π’ = π β ( πΉ β π’ ) = ( πΉ β π ) ) |
26 |
25
|
oveq2d |
β’ ( π’ = π β ( ( πΉ β π ) π· ( πΉ β π’ ) ) = ( ( πΉ β π ) π· ( πΉ β π ) ) ) |
27 |
26
|
breq1d |
β’ ( π’ = π β ( ( ( πΉ β π ) π· ( πΉ β π’ ) ) < π₯ β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
28 |
24 27
|
imbi12d |
β’ ( π’ = π β ( ( π’ β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π’ ) ) < π₯ ) β ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) |
29 |
28
|
cbvralvw |
β’ ( β π’ β ( β€β₯ β π ) ( π’ β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π’ ) ) < π₯ ) β β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
30 |
29
|
ralbii |
β’ ( β π β ( β€β₯ β π ) β π’ β ( β€β₯ β π ) ( π’ β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π’ ) ) < π₯ ) β β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
31 |
|
fveq2 |
β’ ( π = π β ( β€β₯ β π ) = ( β€β₯ β π ) ) |
32 |
31
|
eleq2d |
β’ ( π = π β ( π’ β ( β€β₯ β π ) β π’ β ( β€β₯ β π ) ) ) |
33 |
|
fveq2 |
β’ ( π = π β ( πΉ β π ) = ( πΉ β π ) ) |
34 |
33
|
oveq1d |
β’ ( π = π β ( ( πΉ β π ) π· ( πΉ β π’ ) ) = ( ( πΉ β π ) π· ( πΉ β π’ ) ) ) |
35 |
34
|
breq1d |
β’ ( π = π β ( ( ( πΉ β π ) π· ( πΉ β π’ ) ) < π₯ β ( ( πΉ β π ) π· ( πΉ β π’ ) ) < π₯ ) ) |
36 |
32 35
|
imbi12d |
β’ ( π = π β ( ( π’ β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π’ ) ) < π₯ ) β ( π’ β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π’ ) ) < π₯ ) ) ) |
37 |
|
eleq1w |
β’ ( π’ = π β ( π’ β ( β€β₯ β π ) β π β ( β€β₯ β π ) ) ) |
38 |
|
fveq2 |
β’ ( π’ = π β ( πΉ β π’ ) = ( πΉ β π ) ) |
39 |
38
|
oveq2d |
β’ ( π’ = π β ( ( πΉ β π ) π· ( πΉ β π’ ) ) = ( ( πΉ β π ) π· ( πΉ β π ) ) ) |
40 |
39
|
breq1d |
β’ ( π’ = π β ( ( ( πΉ β π ) π· ( πΉ β π’ ) ) < π₯ β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
41 |
37 40
|
imbi12d |
β’ ( π’ = π β ( ( π’ β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π’ ) ) < π₯ ) β ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) |
42 |
36 41
|
cbvral2vw |
β’ ( β π β ( β€β₯ β π ) β π’ β ( β€β₯ β π ) ( π’ β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π’ ) ) < π₯ ) β β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
43 |
|
ralcom |
β’ ( β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
44 |
30 42 43
|
3bitr3i |
β’ ( β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
45 |
44
|
anbi2i |
β’ ( ( β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β§ β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) β ( β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β§ β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) |
46 |
|
anidm |
β’ ( ( β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β§ β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) β β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
47 |
23 45 46
|
3bitr2i |
β’ ( β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β§ ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) β β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
48 |
|
simpll1 |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) ) β π· β ( βMet β π ) ) |
49 |
|
simpll3 |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) ) β πΉ : π βΆ π ) |
50 |
1
|
uztrn2 |
β’ ( ( π β π β§ π β ( β€β₯ β π ) ) β π β π ) |
51 |
50
|
ad2ant2l |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) ) β π β π ) |
52 |
49 51
|
ffvelcdmd |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) ) β ( πΉ β π ) β π ) |
53 |
9
|
adantrr |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) ) β ( πΉ β π ) β π ) |
54 |
|
xmetsym |
β’ ( ( π· β ( βMet β π ) β§ ( πΉ β π ) β π β§ ( πΉ β π ) β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) = ( ( πΉ β π ) π· ( πΉ β π ) ) ) |
55 |
48 52 53 54
|
syl3anc |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) ) β ( ( πΉ β π ) π· ( πΉ β π ) ) = ( ( πΉ β π ) π· ( πΉ β π ) ) ) |
56 |
55
|
breq1d |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) ) β ( ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
57 |
56
|
imbi2d |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) ) β ( ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) |
58 |
57
|
anbi2d |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) ) β ( ( ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β§ ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) β ( ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β§ ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) ) |
59 |
|
jaob |
β’ ( ( ( π β ( β€β₯ β π ) β¨ π β ( β€β₯ β π ) ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β ( ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β§ ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) |
60 |
|
eluzelz |
β’ ( π β ( β€β₯ β π ) β π β β€ ) |
61 |
|
eluzelz |
β’ ( π β ( β€β₯ β π ) β π β β€ ) |
62 |
|
uztric |
β’ ( ( π β β€ β§ π β β€ ) β ( π β ( β€β₯ β π ) β¨ π β ( β€β₯ β π ) ) ) |
63 |
60 61 62
|
syl2an |
β’ ( ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) β ( π β ( β€β₯ β π ) β¨ π β ( β€β₯ β π ) ) ) |
64 |
63
|
adantl |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) ) β ( π β ( β€β₯ β π ) β¨ π β ( β€β₯ β π ) ) ) |
65 |
|
pm5.5 |
β’ ( ( π β ( β€β₯ β π ) β¨ π β ( β€β₯ β π ) ) β ( ( ( π β ( β€β₯ β π ) β¨ π β ( β€β₯ β π ) ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
66 |
64 65
|
syl |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) ) β ( ( ( π β ( β€β₯ β π ) β¨ π β ( β€β₯ β π ) ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
67 |
59 66
|
bitr3id |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) ) β ( ( ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β§ ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
68 |
58 67
|
bitrd |
β’ ( ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β§ ( π β ( β€β₯ β π ) β§ π β ( β€β₯ β π ) ) ) β ( ( ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β§ ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
69 |
68
|
2ralbidva |
β’ ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β ( β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β§ ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) β β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
70 |
47 69
|
bitr3id |
β’ ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β ( β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( π β ( β€β₯ β π ) β ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
71 |
22 70
|
bitrd |
β’ ( ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β§ π β π ) β ( β π β ( β€β₯ β π ) ( π β dom πΉ β§ ( πΉ β π ) β π β§ β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
72 |
71
|
rexbidva |
β’ ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β ( β π β π β π β ( β€β₯ β π ) ( π β dom πΉ β§ ( πΉ β π ) β π β§ β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β β π β π β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
73 |
|
uzf |
β’ β€β₯ : β€ βΆ π« β€ |
74 |
|
ffn |
β’ ( β€β₯ : β€ βΆ π« β€ β β€β₯ Fn β€ ) |
75 |
73 74
|
ax-mp |
β’ β€β₯ Fn β€ |
76 |
|
uzssz |
β’ ( β€β₯ β π ) β β€ |
77 |
1 76
|
eqsstri |
β’ π β β€ |
78 |
|
raleq |
β’ ( π’ = ( β€β₯ β π ) β ( β π β π’ ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ β β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
79 |
78
|
raleqbi1dv |
β’ ( π’ = ( β€β₯ β π ) β ( β π β π’ β π β π’ ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ β β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
80 |
79
|
rexima |
β’ ( ( β€β₯ Fn β€ β§ π β β€ ) β ( β π’ β ( β€β₯ β π ) β π β π’ β π β π’ ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ β β π β π β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
81 |
75 77 80
|
mp2an |
β’ ( β π’ β ( β€β₯ β π ) β π β π’ β π β π’ ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ β β π β π β π β ( β€β₯ β π ) β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) |
82 |
72 81
|
bitr4di |
β’ ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β ( β π β π β π β ( β€β₯ β π ) ( π β dom πΉ β§ ( πΉ β π ) β π β§ β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β β π’ β ( β€β₯ β π ) β π β π’ β π β π’ ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
83 |
82
|
ralbidv |
β’ ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β ( β π₯ β β+ β π β π β π β ( β€β₯ β π ) ( π β dom πΉ β§ ( πΉ β π ) β π β§ β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) β β π₯ β β+ β π’ β ( β€β₯ β π ) β π β π’ β π β π’ ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
84 |
|
elfvdm |
β’ ( π· β ( βMet β π ) β π β dom βMet ) |
85 |
84
|
adantr |
β’ ( ( π· β ( βMet β π ) β§ π β β€ ) β π β dom βMet ) |
86 |
|
cnex |
β’ β β V |
87 |
85 86
|
jctir |
β’ ( ( π· β ( βMet β π ) β§ π β β€ ) β ( π β dom βMet β§ β β V ) ) |
88 |
|
zsscn |
β’ β€ β β |
89 |
77 88
|
sstri |
β’ π β β |
90 |
89
|
jctr |
β’ ( πΉ : π βΆ π β ( πΉ : π βΆ π β§ π β β ) ) |
91 |
|
elpm2r |
β’ ( ( ( π β dom βMet β§ β β V ) β§ ( πΉ : π βΆ π β§ π β β ) ) β πΉ β ( π βpm β ) ) |
92 |
87 90 91
|
syl2an |
β’ ( ( ( π· β ( βMet β π ) β§ π β β€ ) β§ πΉ : π βΆ π ) β πΉ β ( π βpm β ) ) |
93 |
|
simpl |
β’ ( ( π· β ( βMet β π ) β§ π β β€ ) β π· β ( βMet β π ) ) |
94 |
|
simpr |
β’ ( ( π· β ( βMet β π ) β§ π β β€ ) β π β β€ ) |
95 |
1 93 94
|
iscau3 |
β’ ( ( π· β ( βMet β π ) β§ π β β€ ) β ( πΉ β ( Cau β π· ) β ( πΉ β ( π βpm β ) β§ β π₯ β β+ β π β π β π β ( β€β₯ β π ) ( π β dom πΉ β§ ( πΉ β π ) β π β§ β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) ) |
96 |
95
|
baibd |
β’ ( ( ( π· β ( βMet β π ) β§ π β β€ ) β§ πΉ β ( π βpm β ) ) β ( πΉ β ( Cau β π· ) β β π₯ β β+ β π β π β π β ( β€β₯ β π ) ( π β dom πΉ β§ ( πΉ β π ) β π β§ β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) |
97 |
92 96
|
syldan |
β’ ( ( ( π· β ( βMet β π ) β§ π β β€ ) β§ πΉ : π βΆ π ) β ( πΉ β ( Cau β π· ) β β π₯ β β+ β π β π β π β ( β€β₯ β π ) ( π β dom πΉ β§ ( πΉ β π ) β π β§ β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) |
98 |
97
|
3impa |
β’ ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β ( πΉ β ( Cau β π· ) β β π₯ β β+ β π β π β π β ( β€β₯ β π ) ( π β dom πΉ β§ ( πΉ β π ) β π β§ β π β ( β€β₯ β π ) ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) ) |
99 |
2
|
eleq1i |
β’ ( πΏ β ( CauFil β π· ) β ( ( π FilMap πΉ ) β ( β€β₯ β π ) ) β ( CauFil β π· ) ) |
100 |
1
|
uzfbas |
β’ ( π β β€ β ( β€β₯ β π ) β ( fBas β π ) ) |
101 |
|
fmcfil |
β’ ( ( π· β ( βMet β π ) β§ ( β€β₯ β π ) β ( fBas β π ) β§ πΉ : π βΆ π ) β ( ( ( π FilMap πΉ ) β ( β€β₯ β π ) ) β ( CauFil β π· ) β β π₯ β β+ β π’ β ( β€β₯ β π ) β π β π’ β π β π’ ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
102 |
100 101
|
syl3an2 |
β’ ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β ( ( ( π FilMap πΉ ) β ( β€β₯ β π ) ) β ( CauFil β π· ) β β π₯ β β+ β π’ β ( β€β₯ β π ) β π β π’ β π β π’ ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
103 |
99 102
|
bitrid |
β’ ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β ( πΏ β ( CauFil β π· ) β β π₯ β β+ β π’ β ( β€β₯ β π ) β π β π’ β π β π’ ( ( πΉ β π ) π· ( πΉ β π ) ) < π₯ ) ) |
104 |
83 98 103
|
3bitr4d |
β’ ( ( π· β ( βMet β π ) β§ π β β€ β§ πΉ : π βΆ π ) β ( πΉ β ( Cau β π· ) β πΏ β ( CauFil β π· ) ) ) |