Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β πΉ β ((π½ CnP πΎ)βπ)) |
2 | | simpll 765 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β πΆ β (βMetβπ)) |
3 | | simplr 767 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β π· β (βMetβπ)) |
4 | | eqid 2736 |
. . . . . . . 8
β’ βͺ π½ =
βͺ π½ |
5 | 4 | cnprcl 22445 |
. . . . . . 7
β’ (πΉ β ((π½ CnP πΎ)βπ) β π β βͺ π½) |
6 | 5 | adantl 483 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β π β βͺ π½) |
7 | | metcn.2 |
. . . . . . . 8
β’ π½ = (MetOpenβπΆ) |
8 | 7 | mopnuni 23643 |
. . . . . . 7
β’ (πΆ β (βMetβπ) β π = βͺ π½) |
9 | 8 | ad2antrr 724 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β π = βͺ π½) |
10 | 6, 9 | eleqtrrd 2840 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β π β π) |
11 | | metcn.4 |
. . . . . 6
β’ πΎ = (MetOpenβπ·) |
12 | 7, 11 | metcnp 23746 |
. . . . 5
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ§ β β+ βπ₯ β β+
βπ¦ β π ((ππΆπ¦) < π₯ β ((πΉβπ)π·(πΉβπ¦)) < π§)))) |
13 | 2, 3, 10, 12 | syl3anc 1371 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ§ β β+ βπ₯ β β+
βπ¦ β π ((ππΆπ¦) < π₯ β ((πΉβπ)π·(πΉβπ¦)) < π§)))) |
14 | 1, 13 | mpbid 231 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β (πΉ:πβΆπ β§ βπ§ β β+ βπ₯ β β+
βπ¦ β π ((ππΆπ¦) < π₯ β ((πΉβπ)π·(πΉβπ¦)) < π§))) |
15 | | breq2 5085 |
. . . . . 6
β’ (π§ = π΄ β (((πΉβπ)π·(πΉβπ¦)) < π§ β ((πΉβπ)π·(πΉβπ¦)) < π΄)) |
16 | 15 | imbi2d 341 |
. . . . 5
β’ (π§ = π΄ β (((ππΆπ¦) < π₯ β ((πΉβπ)π·(πΉβπ¦)) < π§) β ((ππΆπ¦) < π₯ β ((πΉβπ)π·(πΉβπ¦)) < π΄))) |
17 | 16 | rexralbidv 3211 |
. . . 4
β’ (π§ = π΄ β (βπ₯ β β+ βπ¦ β π ((ππΆπ¦) < π₯ β ((πΉβπ)π·(πΉβπ¦)) < π§) β βπ₯ β β+ βπ¦ β π ((ππΆπ¦) < π₯ β ((πΉβπ)π·(πΉβπ¦)) < π΄))) |
18 | 17 | rspccv 3563 |
. . 3
β’
(βπ§ β
β+ βπ₯ β β+ βπ¦ β π ((ππΆπ¦) < π₯ β ((πΉβπ)π·(πΉβπ¦)) < π§) β (π΄ β β+ β
βπ₯ β
β+ βπ¦ β π ((ππΆπ¦) < π₯ β ((πΉβπ)π·(πΉβπ¦)) < π΄))) |
19 | 14, 18 | simpl2im 505 |
. 2
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β (π΄ β β+ β
βπ₯ β
β+ βπ¦ β π ((ππΆπ¦) < π₯ β ((πΉβπ)π·(πΉβπ¦)) < π΄))) |
20 | 19 | impr 456 |
1
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β
βπ₯ β
β+ βπ¦ β π ((ππΆπ¦) < π₯ β ((πΉβπ)π·(πΉβπ¦)) < π΄)) |