Step | Hyp | Ref
| Expression |
1 | | inss1 4192 |
. . . . . . . . 9
β’ (π β© π) β π |
2 | | xpss2 5657 |
. . . . . . . . 9
β’ ((π β© π) β π β (β Γ (π β© π)) β (β Γ π)) |
3 | 1, 2 | ax-mp 5 |
. . . . . . . 8
β’ (β
Γ (π β© π)) β (β Γ
π) |
4 | | sstr 3956 |
. . . . . . . 8
β’ ((π β (β Γ (π β© π)) β§ (β Γ (π β© π)) β (β Γ π)) β π β (β Γ π)) |
5 | 3, 4 | mpan2 690 |
. . . . . . 7
β’ (π β (β Γ (π β© π)) β π β (β Γ π)) |
6 | 5 | anim2i 618 |
. . . . . 6
β’ ((Fun
π β§ π β (β Γ (π β© π))) β (Fun π β§ π β (β Γ π))) |
7 | 6 | a1i 11 |
. . . . 5
β’ (π· β (βMetβπ) β ((Fun π β§ π β (β Γ (π β© π))) β (Fun π β§ π β (β Γ π)))) |
8 | | elfvdm 6883 |
. . . . . . 7
β’ (π· β (βMetβπ) β π β dom βMet) |
9 | | inex1g 5280 |
. . . . . . 7
β’ (π β dom βMet β
(π β© π) β V) |
10 | 8, 9 | syl 17 |
. . . . . 6
β’ (π· β (βMetβπ) β (π β© π) β V) |
11 | | cnex 11140 |
. . . . . 6
β’ β
β V |
12 | | elpmg 8787 |
. . . . . 6
β’ (((π β© π) β V β§ β β V) β
(π β ((π β© π) βpm β) β (Fun
π β§ π β (β Γ (π β© π))))) |
13 | 10, 11, 12 | sylancl 587 |
. . . . 5
β’ (π· β (βMetβπ) β (π β ((π β© π) βpm β) β (Fun
π β§ π β (β Γ (π β© π))))) |
14 | | elpmg 8787 |
. . . . . 6
β’ ((π β dom βMet β§
β β V) β (π
β (π
βpm β) β (Fun π β§ π β (β Γ π)))) |
15 | 8, 11, 14 | sylancl 587 |
. . . . 5
β’ (π· β (βMetβπ) β (π β (π βpm β) β (Fun
π β§ π β (β Γ π)))) |
16 | 7, 13, 15 | 3imtr4d 294 |
. . . 4
β’ (π· β (βMetβπ) β (π β ((π β© π) βpm β) β π β (π βpm
β))) |
17 | | uzid 12786 |
. . . . . . . . . 10
β’ (π¦ β β€ β π¦ β
(β€β₯βπ¦)) |
18 | 17 | adantl 483 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π¦ β β€) β π¦ β (β€β₯βπ¦)) |
19 | | simp2 1138 |
. . . . . . . . . 10
β’ ((π§ β dom π β§ (πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯) β (πβπ§) β (π β© π)) |
20 | 19 | ralimi 3083 |
. . . . . . . . 9
β’
(βπ§ β
(β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯) β βπ§ β (β€β₯βπ¦)(πβπ§) β (π β© π)) |
21 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π§ = π¦ β (πβπ§) = (πβπ¦)) |
22 | 21 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π§ = π¦ β ((πβπ§) β (π β© π) β (πβπ¦) β (π β© π))) |
23 | 22 | rspcva 3581 |
. . . . . . . . 9
β’ ((π¦ β
(β€β₯βπ¦) β§ βπ§ β (β€β₯βπ¦)(πβπ§) β (π β© π)) β (πβπ¦) β (π β© π)) |
24 | 18, 20, 23 | syl2an 597 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π¦ β β€) β§ βπ§ β
(β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯)) β (πβπ¦) β (π β© π)) |
25 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β (π β© π)) β (πβπ¦) β (π β© π)) |
26 | 25 | elin2d 4163 |
. . . . . . . . . . . . 13
β’ (((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β (π β© π)) β (πβπ¦) β π) |
27 | | inss2 4193 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β© π) β π |
28 | 27 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β π) β (π β© π) β π) |
29 | 28 | sselda 3948 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β π) β§ (πβπ§) β (π β© π)) β (πβπ§) β π) |
30 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β π) β§ (πβπ§) β (π β© π)) β (πβπ¦) β π) |
31 | 29, 30 | ovresd 7525 |
. . . . . . . . . . . . . . . . 17
β’ ((((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β π) β§ (πβπ§) β (π β© π)) β ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) = ((πβπ§)π·(πβπ¦))) |
32 | 31 | breq1d 5119 |
. . . . . . . . . . . . . . . 16
β’ ((((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β π) β§ (πβπ§) β (π β© π)) β (((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯ β ((πβπ§)π·(πβπ¦)) < π₯)) |
33 | 32 | biimpd 228 |
. . . . . . . . . . . . . . 15
β’ ((((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β π) β§ (πβπ§) β (π β© π)) β (((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯ β ((πβπ§)π·(πβπ¦)) < π₯)) |
34 | 33 | imdistanda 573 |
. . . . . . . . . . . . . 14
β’ (((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β π) β (((πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯) β ((πβπ§) β (π β© π) β§ ((πβπ§)π·(πβπ¦)) < π₯))) |
35 | 1 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β π) β (π β© π) β π) |
36 | 35 | sseld 3947 |
. . . . . . . . . . . . . . 15
β’ (((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β π) β ((πβπ§) β (π β© π) β (πβπ§) β π)) |
37 | 36 | anim1d 612 |
. . . . . . . . . . . . . 14
β’ (((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β π) β (((πβπ§) β (π β© π) β§ ((πβπ§)π·(πβπ¦)) < π₯) β ((πβπ§) β π β§ ((πβπ§)π·(πβπ¦)) < π₯))) |
38 | 34, 37 | syld 47 |
. . . . . . . . . . . . 13
β’ (((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β π) β (((πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯) β ((πβπ§) β π β§ ((πβπ§)π·(πβπ¦)) < π₯))) |
39 | 26, 38 | syldan 592 |
. . . . . . . . . . . 12
β’ (((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β (π β© π)) β (((πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯) β ((πβπ§) β π β§ ((πβπ§)π·(πβπ¦)) < π₯))) |
40 | 39 | anim2d 613 |
. . . . . . . . . . 11
β’ (((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β (π β© π)) β ((π§ β dom π β§ ((πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯)) β (π§ β dom π β§ ((πβπ§) β π β§ ((πβπ§)π·(πβπ¦)) < π₯)))) |
41 | | 3anass 1096 |
. . . . . . . . . . 11
β’ ((π§ β dom π β§ (πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯) β (π§ β dom π β§ ((πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯))) |
42 | | 3anass 1096 |
. . . . . . . . . . 11
β’ ((π§ β dom π β§ (πβπ§) β π β§ ((πβπ§)π·(πβπ¦)) < π₯) β (π§ β dom π β§ ((πβπ§) β π β§ ((πβπ§)π·(πβπ¦)) < π₯))) |
43 | 40, 41, 42 | 3imtr4g 296 |
. . . . . . . . . 10
β’ (((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β (π β© π)) β ((π§ β dom π β§ (πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯) β (π§ β dom π β§ (πβπ§) β π β§ ((πβπ§)π·(πβπ¦)) < π₯))) |
44 | 43 | ralimdv 3163 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π¦ β β€) β§ (πβπ¦) β (π β© π)) β (βπ§ β (β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯) β βπ§ β (β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β π β§ ((πβπ§)π·(πβπ¦)) < π₯))) |
45 | 44 | impancom 453 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π¦ β β€) β§ βπ§ β
(β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯)) β ((πβπ¦) β (π β© π) β βπ§ β (β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β π β§ ((πβπ§)π·(πβπ¦)) < π₯))) |
46 | 24, 45 | mpd 15 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π¦ β β€) β§ βπ§ β
(β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯)) β βπ§ β (β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β π β§ ((πβπ§)π·(πβπ¦)) < π₯)) |
47 | 46 | ex 414 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π¦ β β€) β (βπ§ β
(β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯) β βπ§ β (β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β π β§ ((πβπ§)π·(πβπ¦)) < π₯))) |
48 | 47 | reximdva 3162 |
. . . . 5
β’ (π· β (βMetβπ) β (βπ¦ β β€ βπ§ β
(β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯) β βπ¦ β β€ βπ§ β (β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β π β§ ((πβπ§)π·(πβπ¦)) < π₯))) |
49 | 48 | ralimdv 3163 |
. . . 4
β’ (π· β (βMetβπ) β (βπ₯ β β+
βπ¦ β β€
βπ§ β
(β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯) β βπ₯ β β+ βπ¦ β β€ βπ§ β
(β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β π β§ ((πβπ§)π·(πβπ¦)) < π₯))) |
50 | 16, 49 | anim12d 610 |
. . 3
β’ (π· β (βMetβπ) β ((π β ((π β© π) βpm β) β§
βπ₯ β
β+ βπ¦ β β€ βπ§ β (β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯)) β (π β (π βpm β) β§
βπ₯ β
β+ βπ¦ β β€ βπ§ β (β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β π β§ ((πβπ§)π·(πβπ¦)) < π₯)))) |
51 | | xmetres 23740 |
. . . 4
β’ (π· β (βMetβπ) β (π· βΎ (π Γ π)) β (βMetβ(π β© π))) |
52 | | iscau2 24664 |
. . . 4
β’ ((π· βΎ (π Γ π)) β (βMetβ(π β© π)) β (π β (Cauβ(π· βΎ (π Γ π))) β (π β ((π β© π) βpm β) β§
βπ₯ β
β+ βπ¦ β β€ βπ§ β (β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯)))) |
53 | 51, 52 | syl 17 |
. . 3
β’ (π· β (βMetβπ) β (π β (Cauβ(π· βΎ (π Γ π))) β (π β ((π β© π) βpm β) β§
βπ₯ β
β+ βπ¦ β β€ βπ§ β (β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β (π β© π) β§ ((πβπ§)(π· βΎ (π Γ π))(πβπ¦)) < π₯)))) |
54 | | iscau2 24664 |
. . 3
β’ (π· β (βMetβπ) β (π β (Cauβπ·) β (π β (π βpm β) β§
βπ₯ β
β+ βπ¦ β β€ βπ§ β (β€β₯βπ¦)(π§ β dom π β§ (πβπ§) β π β§ ((πβπ§)π·(πβπ¦)) < π₯)))) |
55 | 50, 53, 54 | 3imtr4d 294 |
. 2
β’ (π· β (βMetβπ) β (π β (Cauβ(π· βΎ (π Γ π))) β π β (Cauβπ·))) |
56 | 55 | ssrdv 3954 |
1
β’ (π· β (βMetβπ) β (Cauβ(π· βΎ (π Γ π))) β (Cauβπ·)) |