Step | Hyp | Ref
| Expression |
1 | | simprl 770 |
. 2
β’ (((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β§ (πΊ β (Filβπ) β§ πΉ β πΊ)) β πΊ β (Filβπ)) |
2 | | simprr 772 |
. . 3
β’ (((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β§ (πΊ β (Filβπ) β§ πΉ β πΊ)) β πΉ β πΊ) |
3 | | iscfil 24645 |
. . . . 5
β’ (π· β (βMetβπ) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ₯ β β+ βπ¦ β πΉ (π· β (π¦ Γ π¦)) β (0[,)π₯)))) |
4 | 3 | simplbda 501 |
. . . 4
β’ ((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β βπ₯ β β+ βπ¦ β πΉ (π· β (π¦ Γ π¦)) β (0[,)π₯)) |
5 | 4 | adantr 482 |
. . 3
β’ (((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β§ (πΊ β (Filβπ) β§ πΉ β πΊ)) β βπ₯ β β+ βπ¦ β πΉ (π· β (π¦ Γ π¦)) β (0[,)π₯)) |
6 | | ssrexv 4016 |
. . . 4
β’ (πΉ β πΊ β (βπ¦ β πΉ (π· β (π¦ Γ π¦)) β (0[,)π₯) β βπ¦ β πΊ (π· β (π¦ Γ π¦)) β (0[,)π₯))) |
7 | 6 | ralimdv 3167 |
. . 3
β’ (πΉ β πΊ β (βπ₯ β β+ βπ¦ β πΉ (π· β (π¦ Γ π¦)) β (0[,)π₯) β βπ₯ β β+ βπ¦ β πΊ (π· β (π¦ Γ π¦)) β (0[,)π₯))) |
8 | 2, 5, 7 | sylc 65 |
. 2
β’ (((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β§ (πΊ β (Filβπ) β§ πΉ β πΊ)) β βπ₯ β β+ βπ¦ β πΊ (π· β (π¦ Γ π¦)) β (0[,)π₯)) |
9 | | iscfil 24645 |
. . 3
β’ (π· β (βMetβπ) β (πΊ β (CauFilβπ·) β (πΊ β (Filβπ) β§ βπ₯ β β+ βπ¦ β πΊ (π· β (π¦ Γ π¦)) β (0[,)π₯)))) |
10 | 9 | ad2antrr 725 |
. 2
β’ (((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β§ (πΊ β (Filβπ) β§ πΉ β πΊ)) β (πΊ β (CauFilβπ·) β (πΊ β (Filβπ) β§ βπ₯ β β+ βπ¦ β πΊ (π· β (π¦ Γ π¦)) β (0[,)π₯)))) |
11 | 1, 8, 10 | mpbir2and 712 |
1
β’ (((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β§ (πΊ β (Filβπ) β§ πΉ β πΊ)) β πΊ β (CauFilβπ·)) |