Step | Hyp | Ref
| Expression |
1 | | metcn.2 |
. . 3
β’ π½ = (MetOpenβπΆ) |
2 | | metcn.4 |
. . 3
β’ πΎ = (MetOpenβπ·) |
3 | 1, 2 | metcnp 23920 |
. 2
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+
βπ€ β π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦)))) |
4 | | simpl1 1192 |
. . . . . . . . . . 11
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β πΆ β (βMetβπ)) |
5 | 4 | ad2antrr 725 |
. . . . . . . . . 10
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β πΆ β (βMetβπ)) |
6 | | simpl3 1194 |
. . . . . . . . . . 11
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β π β π) |
7 | 6 | ad2antrr 725 |
. . . . . . . . . 10
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β π β π) |
8 | | simpr 486 |
. . . . . . . . . 10
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β π€ β π) |
9 | | xmetsym 23723 |
. . . . . . . . . 10
β’ ((πΆ β (βMetβπ) β§ π β π β§ π€ β π) β (ππΆπ€) = (π€πΆπ)) |
10 | 5, 7, 8, 9 | syl3anc 1372 |
. . . . . . . . 9
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β (ππΆπ€) = (π€πΆπ)) |
11 | 10 | breq1d 5119 |
. . . . . . . 8
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β ((ππΆπ€) < π§ β (π€πΆπ) < π§)) |
12 | | simpl2 1193 |
. . . . . . . . . . 11
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β π· β (βMetβπ)) |
13 | 12 | ad2antrr 725 |
. . . . . . . . . 10
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β π· β (βMetβπ)) |
14 | | simpllr 775 |
. . . . . . . . . . 11
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β πΉ:πβΆπ) |
15 | 14, 7 | ffvelcdmd 7040 |
. . . . . . . . . 10
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β (πΉβπ) β π) |
16 | 14, 8 | ffvelcdmd 7040 |
. . . . . . . . . 10
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β (πΉβπ€) β π) |
17 | | xmetsym 23723 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ (πΉβπ€) β π) β ((πΉβπ)π·(πΉβπ€)) = ((πΉβπ€)π·(πΉβπ))) |
18 | 13, 15, 16, 17 | syl3anc 1372 |
. . . . . . . . 9
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β ((πΉβπ)π·(πΉβπ€)) = ((πΉβπ€)π·(πΉβπ))) |
19 | 18 | breq1d 5119 |
. . . . . . . 8
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β (((πΉβπ)π·(πΉβπ€)) < π¦ β ((πΉβπ€)π·(πΉβπ)) < π¦)) |
20 | 11, 19 | imbi12d 345 |
. . . . . . 7
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β§ π€ β π) β (((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦) β ((π€πΆπ) < π§ β ((πΉβπ€)π·(πΉβπ)) < π¦))) |
21 | 20 | ralbidva 3169 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π§ β β+))
β (βπ€ β
π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦) β βπ€ β π ((π€πΆπ) < π§ β ((πΉβπ€)π·(πΉβπ)) < π¦))) |
22 | 21 | anassrs 469 |
. . . . 5
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β§ π§ β β+)
β (βπ€ β
π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦) β βπ€ β π ((π€πΆπ) < π§ β ((πΉβπ€)π·(πΉβπ)) < π¦))) |
23 | 22 | rexbidva 3170 |
. . . 4
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β
(βπ§ β
β+ βπ€ β π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦) β βπ§ β β+ βπ€ β π ((π€πΆπ) < π§ β ((πΉβπ€)π·(πΉβπ)) < π¦))) |
24 | 23 | ralbidva 3169 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β (βπ¦ β β+ βπ§ β β+
βπ€ β π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦) β βπ¦ β β+ βπ§ β β+
βπ€ β π ((π€πΆπ) < π§ β ((πΉβπ€)π·(πΉβπ)) < π¦))) |
25 | 24 | pm5.32da 580 |
. 2
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β ((πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+
βπ€ β π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦)) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+
βπ€ β π ((π€πΆπ) < π§ β ((πΉβπ€)π·(πΉβπ)) < π¦)))) |
26 | 3, 25 | bitrd 279 |
1
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+
βπ€ β π ((π€πΆπ) < π§ β ((πΉβπ€)π·(πΉβπ)) < π¦)))) |