Step | Hyp | Ref
| Expression |
1 | | simp2 1135 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β πΉ β (Filβπ)) |
2 | | filfbas 23572 |
. . . . . . . 8
β’ (πΉ β (Filβπ) β πΉ β (fBasβπ)) |
3 | 1, 2 | syl 17 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β πΉ β (fBasβπ)) |
4 | | simp3 1136 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β π β πΉ) |
5 | | fbncp 23563 |
. . . . . . 7
β’ ((πΉ β (fBasβπ) β§ π β πΉ) β Β¬ (π β π) β πΉ) |
6 | 3, 4, 5 | syl2anc 582 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β Β¬ (π β π) β πΉ) |
7 | | filelss 23576 |
. . . . . . . 8
β’ ((πΉ β (Filβπ) β§ π β πΉ) β π β π) |
8 | 7 | 3adant1 1128 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β π β π) |
9 | | trfil3 23612 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ π β π) β ((πΉ βΎt π) β (Filβπ) β Β¬ (π β π) β πΉ)) |
10 | 1, 8, 9 | syl2anc 582 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β ((πΉ βΎt π) β (Filβπ) β Β¬ (π β π) β πΉ)) |
11 | 6, 10 | mpbird 256 |
. . . . 5
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (πΉ βΎt π) β (Filβπ)) |
12 | 11 | adantr 479 |
. . . 4
β’ (((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ πΉ β (CauFilβπ·)) β (πΉ βΎt π) β (Filβπ)) |
13 | | cfili 25016 |
. . . . . . 7
β’ ((πΉ β (CauFilβπ·) β§ π₯ β β+) β
βπ β πΉ βπ’ β π βπ£ β π (π’π·π£) < π₯) |
14 | 13 | adantll 710 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ πΉ β (CauFilβπ·)) β§ π₯ β β+) β
βπ β πΉ βπ’ β π βπ£ β π (π’π·π£) < π₯) |
15 | | simpll2 1211 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ πΉ β (CauFilβπ·)) β§ π₯ β β+) β πΉ β (Filβπ)) |
16 | | simpll3 1212 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ πΉ β (CauFilβπ·)) β§ π₯ β β+) β π β πΉ) |
17 | 15, 16 | jca 510 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ πΉ β (CauFilβπ·)) β§ π₯ β β+) β (πΉ β (Filβπ) β§ π β πΉ)) |
18 | | elrestr 17378 |
. . . . . . . . . 10
β’ ((πΉ β (Filβπ) β§ π β πΉ β§ π β πΉ) β (π β© π) β (πΉ βΎt π)) |
19 | 18 | 3expa 1116 |
. . . . . . . . 9
β’ (((πΉ β (Filβπ) β§ π β πΉ) β§ π β πΉ) β (π β© π) β (πΉ βΎt π)) |
20 | 17, 19 | sylan 578 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ) β§ π β πΉ) β§ πΉ β (CauFilβπ·)) β§ π₯ β β+) β§ π β πΉ) β (π β© π) β (πΉ βΎt π)) |
21 | | inss1 4227 |
. . . . . . . . . 10
β’ (π β© π) β π |
22 | | ss2ralv 4051 |
. . . . . . . . . 10
β’ ((π β© π) β π β (βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ’ β (π β© π)βπ£ β (π β© π)(π’π·π£) < π₯)) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . 9
β’
(βπ’ β
π βπ£ β π (π’π·π£) < π₯ β βπ’ β (π β© π)βπ£ β (π β© π)(π’π·π£) < π₯) |
24 | | elinel2 4195 |
. . . . . . . . . . . 12
β’ (π’ β (π β© π) β π’ β π) |
25 | | elinel2 4195 |
. . . . . . . . . . . 12
β’ (π£ β (π β© π) β π£ β π) |
26 | | ovres 7575 |
. . . . . . . . . . . . 13
β’ ((π’ β π β§ π£ β π) β (π’(π· βΎ (π Γ π))π£) = (π’π·π£)) |
27 | 26 | breq1d 5157 |
. . . . . . . . . . . 12
β’ ((π’ β π β§ π£ β π) β ((π’(π· βΎ (π Γ π))π£) < π₯ β (π’π·π£) < π₯)) |
28 | 24, 25, 27 | syl2an 594 |
. . . . . . . . . . 11
β’ ((π’ β (π β© π) β§ π£ β (π β© π)) β ((π’(π· βΎ (π Γ π))π£) < π₯ β (π’π·π£) < π₯)) |
29 | 28 | ralbidva 3173 |
. . . . . . . . . 10
β’ (π’ β (π β© π) β (βπ£ β (π β© π)(π’(π· βΎ (π Γ π))π£) < π₯ β βπ£ β (π β© π)(π’π·π£) < π₯)) |
30 | 29 | ralbiia 3089 |
. . . . . . . . 9
β’
(βπ’ β
(π β© π)βπ£ β (π β© π)(π’(π· βΎ (π Γ π))π£) < π₯ β βπ’ β (π β© π)βπ£ β (π β© π)(π’π·π£) < π₯) |
31 | 23, 30 | sylibr 233 |
. . . . . . . 8
β’
(βπ’ β
π βπ£ β π (π’π·π£) < π₯ β βπ’ β (π β© π)βπ£ β (π β© π)(π’(π· βΎ (π Γ π))π£) < π₯) |
32 | | raleq 3320 |
. . . . . . . . . . 11
β’ (π¦ = (π β© π) β (βπ£ β π¦ (π’(π· βΎ (π Γ π))π£) < π₯ β βπ£ β (π β© π)(π’(π· βΎ (π Γ π))π£) < π₯)) |
33 | 32 | raleqbi1dv 3331 |
. . . . . . . . . 10
β’ (π¦ = (π β© π) β (βπ’ β π¦ βπ£ β π¦ (π’(π· βΎ (π Γ π))π£) < π₯ β βπ’ β (π β© π)βπ£ β (π β© π)(π’(π· βΎ (π Γ π))π£) < π₯)) |
34 | 33 | rspcev 3611 |
. . . . . . . . 9
β’ (((π β© π) β (πΉ βΎt π) β§ βπ’ β (π β© π)βπ£ β (π β© π)(π’(π· βΎ (π Γ π))π£) < π₯) β βπ¦ β (πΉ βΎt π)βπ’ β π¦ βπ£ β π¦ (π’(π· βΎ (π Γ π))π£) < π₯) |
35 | 34 | ex 411 |
. . . . . . . 8
β’ ((π β© π) β (πΉ βΎt π) β (βπ’ β (π β© π)βπ£ β (π β© π)(π’(π· βΎ (π Γ π))π£) < π₯ β βπ¦ β (πΉ βΎt π)βπ’ β π¦ βπ£ β π¦ (π’(π· βΎ (π Γ π))π£) < π₯)) |
36 | 20, 31, 35 | syl2im 40 |
. . . . . . 7
β’
(((((π· β
(βMetβπ) β§
πΉ β (Filβπ) β§ π β πΉ) β§ πΉ β (CauFilβπ·)) β§ π₯ β β+) β§ π β πΉ) β (βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ¦ β (πΉ βΎt π)βπ’ β π¦ βπ£ β π¦ (π’(π· βΎ (π Γ π))π£) < π₯)) |
37 | 36 | rexlimdva 3153 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ πΉ β (CauFilβπ·)) β§ π₯ β β+) β
(βπ β πΉ βπ’ β π βπ£ β π (π’π·π£) < π₯ β βπ¦ β (πΉ βΎt π)βπ’ β π¦ βπ£ β π¦ (π’(π· βΎ (π Γ π))π£) < π₯)) |
38 | 14, 37 | mpd 15 |
. . . . 5
β’ ((((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ πΉ β (CauFilβπ·)) β§ π₯ β β+) β
βπ¦ β (πΉ βΎt π)βπ’ β π¦ βπ£ β π¦ (π’(π· βΎ (π Γ π))π£) < π₯) |
39 | 38 | ralrimiva 3144 |
. . . 4
β’ (((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ πΉ β (CauFilβπ·)) β βπ₯ β β+ βπ¦ β (πΉ βΎt π)βπ’ β π¦ βπ£ β π¦ (π’(π· βΎ (π Γ π))π£) < π₯) |
40 | | simp1 1134 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β π· β (βMetβπ)) |
41 | | xmetres2 24087 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π β π) β (π· βΎ (π Γ π)) β (βMetβπ)) |
42 | 40, 8, 41 | syl2anc 582 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (π· βΎ (π Γ π)) β (βMetβπ)) |
43 | 42 | adantr 479 |
. . . . 5
β’ (((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ πΉ β (CauFilβπ·)) β (π· βΎ (π Γ π)) β (βMetβπ)) |
44 | | iscfil2 25014 |
. . . . 5
β’ ((π· βΎ (π Γ π)) β (βMetβπ) β ((πΉ βΎt π) β (CauFilβ(π· βΎ (π Γ π))) β ((πΉ βΎt π) β (Filβπ) β§ βπ₯ β β+ βπ¦ β (πΉ βΎt π)βπ’ β π¦ βπ£ β π¦ (π’(π· βΎ (π Γ π))π£) < π₯))) |
45 | 43, 44 | syl 17 |
. . . 4
β’ (((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ πΉ β (CauFilβπ·)) β ((πΉ βΎt π) β (CauFilβ(π· βΎ (π Γ π))) β ((πΉ βΎt π) β (Filβπ) β§ βπ₯ β β+ βπ¦ β (πΉ βΎt π)βπ’ β π¦ βπ£ β π¦ (π’(π· βΎ (π Γ π))π£) < π₯))) |
46 | 12, 39, 45 | mpbir2and 709 |
. . 3
β’ (((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β§ πΉ β (CauFilβπ·)) β (πΉ βΎt π) β (CauFilβ(π· βΎ (π Γ π)))) |
47 | 46 | ex 411 |
. 2
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (πΉ β (CauFilβπ·) β (πΉ βΎt π) β (CauFilβ(π· βΎ (π Γ π))))) |
48 | | cfilresi 25043 |
. . . . 5
β’ ((π· β (βMetβπ) β§ (πΉ βΎt π) β (CauFilβ(π· βΎ (π Γ π)))) β (πfilGen(πΉ βΎt π)) β (CauFilβπ·)) |
49 | 48 | ex 411 |
. . . 4
β’ (π· β (βMetβπ) β ((πΉ βΎt π) β (CauFilβ(π· βΎ (π Γ π))) β (πfilGen(πΉ βΎt π)) β (CauFilβπ·))) |
50 | 49 | 3ad2ant1 1131 |
. . 3
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β ((πΉ βΎt π) β (CauFilβ(π· βΎ (π Γ π))) β (πfilGen(πΉ βΎt π)) β (CauFilβπ·))) |
51 | | fgtr 23614 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ π β πΉ) β (πfilGen(πΉ βΎt π)) = πΉ) |
52 | 51 | 3adant1 1128 |
. . . 4
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (πfilGen(πΉ βΎt π)) = πΉ) |
53 | 52 | eleq1d 2816 |
. . 3
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β ((πfilGen(πΉ βΎt π)) β (CauFilβπ·) β πΉ β (CauFilβπ·))) |
54 | 50, 53 | sylibd 238 |
. 2
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β ((πΉ βΎt π) β (CauFilβ(π· βΎ (π Γ π))) β πΉ β (CauFilβπ·))) |
55 | 47, 54 | impbid 211 |
1
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (πΉ β (CauFilβπ·) β (πΉ βΎt π) β (CauFilβ(π· βΎ (π Γ π))))) |