Step | Hyp | Ref
| Expression |
1 | | caures.1 |
. . . . . . . . . . 11
β’ π =
(β€β₯βπ) |
2 | 1 | uztrn2 12790 |
. . . . . . . . . 10
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
3 | 2 | adantll 713 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
4 | 3 | biantrurd 534 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (π β dom πΉ β (π β π β§ π β dom πΉ))) |
5 | | dmres 5963 |
. . . . . . . . 9
β’ dom
(πΉ βΎ π) = (π β© dom πΉ) |
6 | 5 | elin2 4161 |
. . . . . . . 8
β’ (π β dom (πΉ βΎ π) β (π β π β§ π β dom πΉ)) |
7 | 4, 6 | bitr4di 289 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (π β dom πΉ β π β dom (πΉ βΎ π))) |
8 | 7 | 3anbi1d 1441 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β (π β dom (πΉ βΎ π) β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
9 | 8 | ralbidva 3169 |
. . . . 5
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)(π β dom (πΉ βΎ π) β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
10 | 9 | rexbidva 3170 |
. . . 4
β’ (π β (βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β βπ β π βπ β (β€β₯βπ)(π β dom (πΉ βΎ π) β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
11 | 10 | ralbidv 3171 |
. . 3
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom (πΉ βΎ π) β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯))) |
12 | | caures.5 |
. . . 4
β’ (π β πΉ β (π βpm
β)) |
13 | 12 | biantrurd 534 |
. . 3
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |
14 | | caures.4 |
. . . . . . 7
β’ (π β π· β (Metβπ)) |
15 | | elfvdm 6883 |
. . . . . . 7
β’ (π· β (Metβπ) β π β dom Met) |
16 | 14, 15 | syl 17 |
. . . . . 6
β’ (π β π β dom Met) |
17 | | cnex 11140 |
. . . . . 6
β’ β
β V |
18 | | ssid 3970 |
. . . . . . 7
β’ π β π |
19 | | uzssz 12792 |
. . . . . . . . 9
β’
(β€β₯βπ) β β€ |
20 | | zsscn 12515 |
. . . . . . . . 9
β’ β€
β β |
21 | 19, 20 | sstri 3957 |
. . . . . . . 8
β’
(β€β₯βπ) β β |
22 | 1, 21 | eqsstri 3982 |
. . . . . . 7
β’ π β
β |
23 | | pmss12g 8813 |
. . . . . . 7
β’ (((π β π β§ π β β) β§ (π β dom Met β§ β β V))
β (π
βpm π)
β (π
βpm β)) |
24 | 18, 22, 23 | mpanl12 701 |
. . . . . 6
β’ ((π β dom Met β§ β
β V) β (π
βpm π)
β (π
βpm β)) |
25 | 16, 17, 24 | sylancl 587 |
. . . . 5
β’ (π β (π βpm π) β (π βpm
β)) |
26 | 1 | fvexi 6860 |
. . . . . 6
β’ π β V |
27 | | pmresg 8814 |
. . . . . 6
β’ ((π β V β§ πΉ β (π βpm β)) β (πΉ βΎ π) β (π βpm π)) |
28 | 26, 12, 27 | sylancr 588 |
. . . . 5
β’ (π β (πΉ βΎ π) β (π βpm π)) |
29 | 25, 28 | sseldd 3949 |
. . . 4
β’ (π β (πΉ βΎ π) β (π βpm
β)) |
30 | 29 | biantrurd 534 |
. . 3
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(π β dom (πΉ βΎ π) β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯) β ((πΉ βΎ π) β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom (πΉ βΎ π) β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |
31 | 11, 13, 30 | 3bitr3d 309 |
. 2
β’ (π β ((πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)) β ((πΉ βΎ π) β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom (πΉ βΎ π) β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |
32 | | metxmet 23710 |
. . . 4
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
33 | 14, 32 | syl 17 |
. . 3
β’ (π β π· β (βMetβπ)) |
34 | | caures.3 |
. . 3
β’ (π β π β β€) |
35 | | eqidd 2734 |
. . 3
β’ ((π β§ π β π) β (πΉβπ) = (πΉβπ)) |
36 | | eqidd 2734 |
. . 3
β’ ((π β§ π β π) β (πΉβπ) = (πΉβπ)) |
37 | 1, 33, 34, 35, 36 | iscau4 24666 |
. 2
β’ (π β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |
38 | | fvres 6865 |
. . . 4
β’ (π β π β ((πΉ βΎ π)βπ) = (πΉβπ)) |
39 | 38 | adantl 483 |
. . 3
β’ ((π β§ π β π) β ((πΉ βΎ π)βπ) = (πΉβπ)) |
40 | | fvres 6865 |
. . . 4
β’ (π β π β ((πΉ βΎ π)βπ) = (πΉβπ)) |
41 | 40 | adantl 483 |
. . 3
β’ ((π β§ π β π) β ((πΉ βΎ π)βπ) = (πΉβπ)) |
42 | 1, 33, 34, 39, 41 | iscau4 24666 |
. 2
β’ (π β ((πΉ βΎ π) β (Cauβπ·) β ((πΉ βΎ π) β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom (πΉ βΎ π) β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) |
43 | 31, 37, 42 | 3bitr4d 311 |
1
β’ (π β (πΉ β (Cauβπ·) β (πΉ βΎ π) β (Cauβπ·))) |