Step |
Hyp |
Ref |
Expression |
1 |
|
xmetres |
β’ ( π· β ( βMet β π ) β ( π· βΎ ( π Γ π ) ) β ( βMet β ( π β© π ) ) ) |
2 |
|
iscfil2 |
β’ ( ( π· βΎ ( π Γ π ) ) β ( βMet β ( π β© π ) ) β ( πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) β ( πΉ β ( Fil β ( π β© π ) ) β§ β π₯ β β+ β π¦ β πΉ β π’ β π¦ β π£ β π¦ ( π’ ( π· βΎ ( π Γ π ) ) π£ ) < π₯ ) ) ) |
3 |
2
|
simplbda |
β’ ( ( ( π· βΎ ( π Γ π ) ) β ( βMet β ( π β© π ) ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β β π₯ β β+ β π¦ β πΉ β π’ β π¦ β π£ β π¦ ( π’ ( π· βΎ ( π Γ π ) ) π£ ) < π₯ ) |
4 |
1 3
|
sylan |
β’ ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β β π₯ β β+ β π¦ β πΉ β π’ β π¦ β π£ β π¦ ( π’ ( π· βΎ ( π Γ π ) ) π£ ) < π₯ ) |
5 |
|
cfilfil |
β’ ( ( ( π· βΎ ( π Γ π ) ) β ( βMet β ( π β© π ) ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β πΉ β ( Fil β ( π β© π ) ) ) |
6 |
1 5
|
sylan |
β’ ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β πΉ β ( Fil β ( π β© π ) ) ) |
7 |
|
filelss |
β’ ( ( πΉ β ( Fil β ( π β© π ) ) β§ π¦ β πΉ ) β π¦ β ( π β© π ) ) |
8 |
6 7
|
sylan |
β’ ( ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β§ π¦ β πΉ ) β π¦ β ( π β© π ) ) |
9 |
|
inss2 |
β’ ( π β© π ) β π |
10 |
8 9
|
sstrdi |
β’ ( ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β§ π¦ β πΉ ) β π¦ β π ) |
11 |
10
|
sselda |
β’ ( ( ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β§ π¦ β πΉ ) β§ π’ β π¦ ) β π’ β π ) |
12 |
10
|
sselda |
β’ ( ( ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β§ π¦ β πΉ ) β§ π£ β π¦ ) β π£ β π ) |
13 |
11 12
|
anim12dan |
β’ ( ( ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β§ π¦ β πΉ ) β§ ( π’ β π¦ β§ π£ β π¦ ) ) β ( π’ β π β§ π£ β π ) ) |
14 |
|
ovres |
β’ ( ( π’ β π β§ π£ β π ) β ( π’ ( π· βΎ ( π Γ π ) ) π£ ) = ( π’ π· π£ ) ) |
15 |
13 14
|
syl |
β’ ( ( ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β§ π¦ β πΉ ) β§ ( π’ β π¦ β§ π£ β π¦ ) ) β ( π’ ( π· βΎ ( π Γ π ) ) π£ ) = ( π’ π· π£ ) ) |
16 |
15
|
breq1d |
β’ ( ( ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β§ π¦ β πΉ ) β§ ( π’ β π¦ β§ π£ β π¦ ) ) β ( ( π’ ( π· βΎ ( π Γ π ) ) π£ ) < π₯ β ( π’ π· π£ ) < π₯ ) ) |
17 |
16
|
2ralbidva |
β’ ( ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β§ π¦ β πΉ ) β ( β π’ β π¦ β π£ β π¦ ( π’ ( π· βΎ ( π Γ π ) ) π£ ) < π₯ β β π’ β π¦ β π£ β π¦ ( π’ π· π£ ) < π₯ ) ) |
18 |
17
|
rexbidva |
β’ ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β ( β π¦ β πΉ β π’ β π¦ β π£ β π¦ ( π’ ( π· βΎ ( π Γ π ) ) π£ ) < π₯ β β π¦ β πΉ β π’ β π¦ β π£ β π¦ ( π’ π· π£ ) < π₯ ) ) |
19 |
18
|
ralbidv |
β’ ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β ( β π₯ β β+ β π¦ β πΉ β π’ β π¦ β π£ β π¦ ( π’ ( π· βΎ ( π Γ π ) ) π£ ) < π₯ β β π₯ β β+ β π¦ β πΉ β π’ β π¦ β π£ β π¦ ( π’ π· π£ ) < π₯ ) ) |
20 |
4 19
|
mpbid |
β’ ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β β π₯ β β+ β π¦ β πΉ β π’ β π¦ β π£ β π¦ ( π’ π· π£ ) < π₯ ) |
21 |
|
filfbas |
β’ ( πΉ β ( Fil β ( π β© π ) ) β πΉ β ( fBas β ( π β© π ) ) ) |
22 |
6 21
|
syl |
β’ ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β πΉ β ( fBas β ( π β© π ) ) ) |
23 |
|
filsspw |
β’ ( πΉ β ( Fil β ( π β© π ) ) β πΉ β π« ( π β© π ) ) |
24 |
6 23
|
syl |
β’ ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β πΉ β π« ( π β© π ) ) |
25 |
|
inss1 |
β’ ( π β© π ) β π |
26 |
25
|
sspwi |
β’ π« ( π β© π ) β π« π |
27 |
24 26
|
sstrdi |
β’ ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β πΉ β π« π ) |
28 |
|
elfvdm |
β’ ( π· β ( βMet β π ) β π β dom βMet ) |
29 |
28
|
adantr |
β’ ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β π β dom βMet ) |
30 |
|
fbasweak |
β’ ( ( πΉ β ( fBas β ( π β© π ) ) β§ πΉ β π« π β§ π β dom βMet ) β πΉ β ( fBas β π ) ) |
31 |
22 27 29 30
|
syl3anc |
β’ ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β πΉ β ( fBas β π ) ) |
32 |
|
fgcfil |
β’ ( ( π· β ( βMet β π ) β§ πΉ β ( fBas β π ) ) β ( ( π filGen πΉ ) β ( CauFil β π· ) β β π₯ β β+ β π¦ β πΉ β π’ β π¦ β π£ β π¦ ( π’ π· π£ ) < π₯ ) ) |
33 |
31 32
|
syldan |
β’ ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β ( ( π filGen πΉ ) β ( CauFil β π· ) β β π₯ β β+ β π¦ β πΉ β π’ β π¦ β π£ β π¦ ( π’ π· π£ ) < π₯ ) ) |
34 |
20 33
|
mpbird |
β’ ( ( π· β ( βMet β π ) β§ πΉ β ( CauFil β ( π· βΎ ( π Γ π ) ) ) ) β ( π filGen πΉ ) β ( CauFil β π· ) ) |