Step | Hyp | Ref
| Expression |
1 | | caufpm 24669 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ πΉ β (Cauβπ·)) β πΉ β (π βpm
β)) |
2 | | elfvdm 6883 |
. . . . . . . . . 10
β’ (π· β (βMetβπ) β π β dom βMet) |
3 | | cnex 11140 |
. . . . . . . . . 10
β’ β
β V |
4 | | elpmg 8787 |
. . . . . . . . . 10
β’ ((π β dom βMet β§
β β V) β (πΉ
β (π
βpm β) β (Fun πΉ β§ πΉ β (β Γ π)))) |
5 | 2, 3, 4 | sylancl 587 |
. . . . . . . . 9
β’ (π· β (βMetβπ) β (πΉ β (π βpm β) β (Fun
πΉ β§ πΉ β (β Γ π)))) |
6 | 5 | biimpa 478 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ πΉ β (π βpm β)) β (Fun
πΉ β§ πΉ β (β Γ π))) |
7 | 1, 6 | syldan 592 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ πΉ β (Cauβπ·)) β (Fun πΉ β§ πΉ β (β Γ π))) |
8 | | rnss 5898 |
. . . . . . 7
β’ (πΉ β (β Γ π) β ran πΉ β ran (β Γ π)) |
9 | 7, 8 | simpl2im 505 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ πΉ β (Cauβπ·)) β ran πΉ β ran (β Γ π)) |
10 | | rnxpss 6128 |
. . . . . 6
β’ ran
(β Γ π) β
π |
11 | 9, 10 | sstrdi 3960 |
. . . . 5
β’ ((π· β (βMetβπ) β§ πΉ β (Cauβπ·)) β ran πΉ β π) |
12 | 11 | adantlr 714 |
. . . 4
β’ (((π· β (βMetβπ) β§ πΉ:ββΆπ) β§ πΉ β (Cauβπ·)) β ran πΉ β π) |
13 | | frn 6679 |
. . . . 5
β’ (πΉ:ββΆπ β ran πΉ β π) |
14 | 13 | ad2antlr 726 |
. . . 4
β’ (((π· β (βMetβπ) β§ πΉ:ββΆπ) β§ πΉ β (Cauβπ·)) β ran πΉ β π) |
15 | 12, 14 | ssind 4196 |
. . 3
β’ (((π· β (βMetβπ) β§ πΉ:ββΆπ) β§ πΉ β (Cauβπ·)) β ran πΉ β (π β© π)) |
16 | 15 | ex 414 |
. 2
β’ ((π· β (βMetβπ) β§ πΉ:ββΆπ) β (πΉ β (Cauβπ·) β ran πΉ β (π β© π))) |
17 | | xmetres 23740 |
. . . . . . . 8
β’ (π· β (βMetβπ) β (π· βΎ (π Γ π)) β (βMetβ(π β© π))) |
18 | | caufpm 24669 |
. . . . . . . 8
β’ (((π· βΎ (π Γ π)) β (βMetβ(π β© π)) β§ πΉ β (Cauβ(π· βΎ (π Γ π)))) β πΉ β ((π β© π) βpm
β)) |
19 | 17, 18 | sylan 581 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ πΉ β (Cauβ(π· βΎ (π Γ π)))) β πΉ β ((π β© π) βpm
β)) |
20 | | inex1g 5280 |
. . . . . . . . . 10
β’ (π β dom βMet β
(π β© π) β V) |
21 | 2, 20 | syl 17 |
. . . . . . . . 9
β’ (π· β (βMetβπ) β (π β© π) β V) |
22 | | elpmg 8787 |
. . . . . . . . 9
β’ (((π β© π) β V β§ β β V) β
(πΉ β ((π β© π) βpm β) β (Fun
πΉ β§ πΉ β (β Γ (π β© π))))) |
23 | 21, 3, 22 | sylancl 587 |
. . . . . . . 8
β’ (π· β (βMetβπ) β (πΉ β ((π β© π) βpm β) β (Fun
πΉ β§ πΉ β (β Γ (π β© π))))) |
24 | 23 | biimpa 478 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ πΉ β ((π β© π) βpm β)) β (Fun
πΉ β§ πΉ β (β Γ (π β© π)))) |
25 | 19, 24 | syldan 592 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ πΉ β (Cauβ(π· βΎ (π Γ π)))) β (Fun πΉ β§ πΉ β (β Γ (π β© π)))) |
26 | | rnss 5898 |
. . . . . 6
β’ (πΉ β (β Γ (π β© π)) β ran πΉ β ran (β Γ (π β© π))) |
27 | 25, 26 | simpl2im 505 |
. . . . 5
β’ ((π· β (βMetβπ) β§ πΉ β (Cauβ(π· βΎ (π Γ π)))) β ran πΉ β ran (β Γ (π β© π))) |
28 | | rnxpss 6128 |
. . . . 5
β’ ran
(β Γ (π β©
π)) β (π β© π) |
29 | 27, 28 | sstrdi 3960 |
. . . 4
β’ ((π· β (βMetβπ) β§ πΉ β (Cauβ(π· βΎ (π Γ π)))) β ran πΉ β (π β© π)) |
30 | 29 | ex 414 |
. . 3
β’ (π· β (βMetβπ) β (πΉ β (Cauβ(π· βΎ (π Γ π))) β ran πΉ β (π β© π))) |
31 | 30 | adantr 482 |
. 2
β’ ((π· β (βMetβπ) β§ πΉ:ββΆπ) β (πΉ β (Cauβ(π· βΎ (π Γ π))) β ran πΉ β (π β© π))) |
32 | | ffn 6672 |
. . . 4
β’ (πΉ:ββΆπ β πΉ Fn β) |
33 | | df-f 6504 |
. . . . 5
β’ (πΉ:ββΆ(π β© π) β (πΉ Fn β β§ ran πΉ β (π β© π))) |
34 | 33 | simplbi2 502 |
. . . 4
β’ (πΉ Fn β β (ran πΉ β (π β© π) β πΉ:ββΆ(π β© π))) |
35 | 32, 34 | syl 17 |
. . 3
β’ (πΉ:ββΆπ β (ran πΉ β (π β© π) β πΉ:ββΆ(π β© π))) |
36 | | inss2 4193 |
. . . . . . . . 9
β’ (π β© π) β π |
37 | 36 | a1i 11 |
. . . . . . . 8
β’ (π· β (βMetβπ) β (π β© π) β π) |
38 | | fss 6689 |
. . . . . . . 8
β’ ((πΉ:ββΆ(π β© π) β§ (π β© π) β π) β πΉ:ββΆπ) |
39 | 37, 38 | sylan2 594 |
. . . . . . 7
β’ ((πΉ:ββΆ(π β© π) β§ π· β (βMetβπ)) β πΉ:ββΆπ) |
40 | 39 | ancoms 460 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ πΉ:ββΆ(π β© π)) β πΉ:ββΆπ) |
41 | | ffvelcdm 7036 |
. . . . . . . . . . . 12
β’ ((πΉ:ββΆπ β§ π¦ β β) β (πΉβπ¦) β π) |
42 | 41 | adantr 482 |
. . . . . . . . . . 11
β’ (((πΉ:ββΆπ β§ π¦ β β) β§ π§ β (β€β₯βπ¦)) β (πΉβπ¦) β π) |
43 | | eluznn 12851 |
. . . . . . . . . . . . 13
β’ ((π¦ β β β§ π§ β
(β€β₯βπ¦)) β π§ β β) |
44 | | ffvelcdm 7036 |
. . . . . . . . . . . . 13
β’ ((πΉ:ββΆπ β§ π§ β β) β (πΉβπ§) β π) |
45 | 43, 44 | sylan2 594 |
. . . . . . . . . . . 12
β’ ((πΉ:ββΆπ β§ (π¦ β β β§ π§ β (β€β₯βπ¦))) β (πΉβπ§) β π) |
46 | 45 | anassrs 469 |
. . . . . . . . . . 11
β’ (((πΉ:ββΆπ β§ π¦ β β) β§ π§ β (β€β₯βπ¦)) β (πΉβπ§) β π) |
47 | 42, 46 | ovresd 7525 |
. . . . . . . . . 10
β’ (((πΉ:ββΆπ β§ π¦ β β) β§ π§ β (β€β₯βπ¦)) β ((πΉβπ¦)(π· βΎ (π Γ π))(πΉβπ§)) = ((πΉβπ¦)π·(πΉβπ§))) |
48 | 47 | breq1d 5119 |
. . . . . . . . 9
β’ (((πΉ:ββΆπ β§ π¦ β β) β§ π§ β (β€β₯βπ¦)) β (((πΉβπ¦)(π· βΎ (π Γ π))(πΉβπ§)) < π₯ β ((πΉβπ¦)π·(πΉβπ§)) < π₯)) |
49 | 48 | ralbidva 3169 |
. . . . . . . 8
β’ ((πΉ:ββΆπ β§ π¦ β β) β (βπ§ β
(β€β₯βπ¦)((πΉβπ¦)(π· βΎ (π Γ π))(πΉβπ§)) < π₯ β βπ§ β (β€β₯βπ¦)((πΉβπ¦)π·(πΉβπ§)) < π₯)) |
50 | 49 | rexbidva 3170 |
. . . . . . 7
β’ (πΉ:ββΆπ β (βπ¦ β β βπ§ β
(β€β₯βπ¦)((πΉβπ¦)(π· βΎ (π Γ π))(πΉβπ§)) < π₯ β βπ¦ β β βπ§ β (β€β₯βπ¦)((πΉβπ¦)π·(πΉβπ§)) < π₯)) |
51 | 50 | ralbidv 3171 |
. . . . . 6
β’ (πΉ:ββΆπ β (βπ₯ β β+
βπ¦ β β
βπ§ β
(β€β₯βπ¦)((πΉβπ¦)(π· βΎ (π Γ π))(πΉβπ§)) < π₯ β βπ₯ β β+ βπ¦ β β βπ§ β
(β€β₯βπ¦)((πΉβπ¦)π·(πΉβπ§)) < π₯)) |
52 | 40, 51 | syl 17 |
. . . . 5
β’ ((π· β (βMetβπ) β§ πΉ:ββΆ(π β© π)) β (βπ₯ β β+ βπ¦ β β βπ§ β
(β€β₯βπ¦)((πΉβπ¦)(π· βΎ (π Γ π))(πΉβπ§)) < π₯ β βπ₯ β β+ βπ¦ β β βπ§ β
(β€β₯βπ¦)((πΉβπ¦)π·(πΉβπ§)) < π₯)) |
53 | | nnuz 12814 |
. . . . . 6
β’ β =
(β€β₯β1) |
54 | 17 | adantr 482 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ πΉ:ββΆ(π β© π)) β (π· βΎ (π Γ π)) β (βMetβ(π β© π))) |
55 | | 1zzd 12542 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ πΉ:ββΆ(π β© π)) β 1 β β€) |
56 | | eqidd 2734 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ πΉ:ββΆ(π β© π)) β§ π§ β β) β (πΉβπ§) = (πΉβπ§)) |
57 | | eqidd 2734 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ πΉ:ββΆ(π β© π)) β§ π¦ β β) β (πΉβπ¦) = (πΉβπ¦)) |
58 | | simpr 486 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ πΉ:ββΆ(π β© π)) β πΉ:ββΆ(π β© π)) |
59 | 53, 54, 55, 56, 57, 58 | iscauf 24667 |
. . . . 5
β’ ((π· β (βMetβπ) β§ πΉ:ββΆ(π β© π)) β (πΉ β (Cauβ(π· βΎ (π Γ π))) β βπ₯ β β+ βπ¦ β β βπ§ β
(β€β₯βπ¦)((πΉβπ¦)(π· βΎ (π Γ π))(πΉβπ§)) < π₯)) |
60 | | simpl 484 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ πΉ:ββΆ(π β© π)) β π· β (βMetβπ)) |
61 | | id 22 |
. . . . . . 7
β’ (πΉ:ββΆ(π β© π) β πΉ:ββΆ(π β© π)) |
62 | | inss1 4192 |
. . . . . . . 8
β’ (π β© π) β π |
63 | 62 | a1i 11 |
. . . . . . 7
β’ (π· β (βMetβπ) β (π β© π) β π) |
64 | | fss 6689 |
. . . . . . 7
β’ ((πΉ:ββΆ(π β© π) β§ (π β© π) β π) β πΉ:ββΆπ) |
65 | 61, 63, 64 | syl2anr 598 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ πΉ:ββΆ(π β© π)) β πΉ:ββΆπ) |
66 | 53, 60, 55, 56, 57, 65 | iscauf 24667 |
. . . . 5
β’ ((π· β (βMetβπ) β§ πΉ:ββΆ(π β© π)) β (πΉ β (Cauβπ·) β βπ₯ β β+ βπ¦ β β βπ§ β
(β€β₯βπ¦)((πΉβπ¦)π·(πΉβπ§)) < π₯)) |
67 | 52, 59, 66 | 3bitr4rd 312 |
. . . 4
β’ ((π· β (βMetβπ) β§ πΉ:ββΆ(π β© π)) β (πΉ β (Cauβπ·) β πΉ β (Cauβ(π· βΎ (π Γ π))))) |
68 | 67 | ex 414 |
. . 3
β’ (π· β (βMetβπ) β (πΉ:ββΆ(π β© π) β (πΉ β (Cauβπ·) β πΉ β (Cauβ(π· βΎ (π Γ π)))))) |
69 | 35, 68 | sylan9r 510 |
. 2
β’ ((π· β (βMetβπ) β§ πΉ:ββΆπ) β (ran πΉ β (π β© π) β (πΉ β (Cauβπ·) β πΉ β (Cauβ(π· βΎ (π Γ π)))))) |
70 | 16, 31, 69 | pm5.21ndd 381 |
1
β’ ((π· β (βMetβπ) β§ πΉ:ββΆπ) β (πΉ β (Cauβπ·) β πΉ β (Cauβ(π· βΎ (π Γ π))))) |