Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β πΉ β ((π½ CnP πΎ)βπ)) |
2 | | simpll 766 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β πΆ β (βMetβπ)) |
3 | | simplr 768 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β π· β (βMetβπ)) |
4 | | eqid 2733 |
. . . . . . . 8
β’ βͺ π½ =
βͺ π½ |
5 | 4 | cnprcl 22619 |
. . . . . . 7
β’ (πΉ β ((π½ CnP πΎ)βπ) β π β βͺ π½) |
6 | 5 | adantl 483 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β π β βͺ π½) |
7 | | metcn.2 |
. . . . . . . 8
β’ π½ = (MetOpenβπΆ) |
8 | 7 | mopnuni 23817 |
. . . . . . 7
β’ (πΆ β (βMetβπ) β π = βͺ π½) |
9 | 8 | ad2antrr 725 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β π = βͺ π½) |
10 | 6, 9 | eleqtrrd 2837 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β π β π) |
11 | | metcn.4 |
. . . . . 6
β’ πΎ = (MetOpenβπ·) |
12 | 7, 11 | metcnp2 23921 |
. . . . 5
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ§ β β+ βπ₯ β β+
βπ¦ β π ((π¦πΆπ) < π₯ β ((πΉβπ¦)π·(πΉβπ)) < π§)))) |
13 | 2, 3, 10, 12 | syl3anc 1372 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ§ β β+ βπ₯ β β+
βπ¦ β π ((π¦πΆπ) < π₯ β ((πΉβπ¦)π·(πΉβπ)) < π§)))) |
14 | 1, 13 | mpbid 231 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β (πΉ:πβΆπ β§ βπ§ β β+ βπ₯ β β+
βπ¦ β π ((π¦πΆπ) < π₯ β ((πΉβπ¦)π·(πΉβπ)) < π§))) |
15 | | breq2 5113 |
. . . . . 6
β’ (π§ = π΄ β (((πΉβπ¦)π·(πΉβπ)) < π§ β ((πΉβπ¦)π·(πΉβπ)) < π΄)) |
16 | 15 | imbi2d 341 |
. . . . 5
β’ (π§ = π΄ β (((π¦πΆπ) < π₯ β ((πΉβπ¦)π·(πΉβπ)) < π§) β ((π¦πΆπ) < π₯ β ((πΉβπ¦)π·(πΉβπ)) < π΄))) |
17 | 16 | rexralbidv 3211 |
. . . 4
β’ (π§ = π΄ β (βπ₯ β β+ βπ¦ β π ((π¦πΆπ) < π₯ β ((πΉβπ¦)π·(πΉβπ)) < π§) β βπ₯ β β+ βπ¦ β π ((π¦πΆπ) < π₯ β ((πΉβπ¦)π·(πΉβπ)) < π΄))) |
18 | 17 | rspccv 3580 |
. . 3
β’
(βπ§ β
β+ βπ₯ β β+ βπ¦ β π ((π¦πΆπ) < π₯ β ((πΉβπ¦)π·(πΉβπ)) < π§) β (π΄ β β+ β
βπ₯ β
β+ βπ¦ β π ((π¦πΆπ) < π₯ β ((πΉβπ¦)π·(πΉβπ)) < π΄))) |
19 | 14, 18 | simpl2im 505 |
. 2
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β (π΄ β β+ β
βπ₯ β
β+ βπ¦ β π ((π¦πΆπ) < π₯ β ((πΉβπ¦)π·(πΉβπ)) < π΄))) |
20 | 19 | impr 456 |
1
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β
βπ₯ β
β+ βπ¦ β π ((π¦πΆπ) < π₯ β ((πΉβπ¦)π·(πΉβπ)) < π΄)) |