Step | Hyp | Ref
| Expression |
1 | | metcn.2 |
. . . . . 6
β’ π½ = (MetOpenβπΆ) |
2 | 1 | mopntopon 23815 |
. . . . 5
β’ (πΆ β (βMetβπ) β π½ β (TopOnβπ)) |
3 | | metcn.4 |
. . . . . 6
β’ πΎ = (MetOpenβπ·) |
4 | 3 | mopntopon 23815 |
. . . . 5
β’ (π· β (βMetβπ) β πΎ β (TopOnβπ)) |
5 | | txtopon 22965 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
6 | 2, 4, 5 | syl2an 597 |
. . . 4
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
7 | 6 | 3adant3 1133 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
8 | | txmetcnp.4 |
. . . . 5
β’ πΏ = (MetOpenβπΈ) |
9 | 8 | mopntopon 23815 |
. . . 4
β’ (πΈ β (βMetβπ) β πΏ β (TopOnβπ)) |
10 | 9 | 3ad2ant3 1136 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β πΏ β (TopOnβπ)) |
11 | | cncnp 22654 |
. . 3
β’ (((π½ Γt πΎ) β (TopOnβ(π Γ π)) β§ πΏ β (TopOnβπ)) β (πΉ β ((π½ Γt πΎ) Cn πΏ) β (πΉ:(π Γ π)βΆπ β§ βπ‘ β (π Γ π)πΉ β (((π½ Γt πΎ) CnP πΏ)βπ‘)))) |
12 | 7, 10, 11 | syl2anc 585 |
. 2
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β (πΉ β ((π½ Γt πΎ) Cn πΏ) β (πΉ:(π Γ π)βΆπ β§ βπ‘ β (π Γ π)πΉ β (((π½ Γt πΎ) CnP πΏ)βπ‘)))) |
13 | | fveq2 6846 |
. . . . . 6
β’ (π‘ = β¨π₯, π¦β© β (((π½ Γt πΎ) CnP πΏ)βπ‘) = (((π½ Γt πΎ) CnP πΏ)ββ¨π₯, π¦β©)) |
14 | 13 | eleq2d 2820 |
. . . . 5
β’ (π‘ = β¨π₯, π¦β© β (πΉ β (((π½ Γt πΎ) CnP πΏ)βπ‘) β πΉ β (((π½ Γt πΎ) CnP πΏ)ββ¨π₯, π¦β©))) |
15 | 14 | ralxp 5801 |
. . . 4
β’
(βπ‘ β
(π Γ π)πΉ β (((π½ Γt πΎ) CnP πΏ)βπ‘) β βπ₯ β π βπ¦ β π πΉ β (((π½ Γt πΎ) CnP πΏ)ββ¨π₯, π¦β©)) |
16 | | simplr 768 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ πΉ:(π Γ π)βΆπ) β§ (π₯ β π β§ π¦ β π)) β πΉ:(π Γ π)βΆπ) |
17 | 1, 3, 8 | txmetcnp 23926 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π₯ β π β§ π¦ β π)) β (πΉ β (((π½ Γt πΎ) CnP πΏ)ββ¨π₯, π¦β©) β (πΉ:(π Γ π)βΆπ β§ βπ§ β β+ βπ€ β β+
βπ’ β π βπ£ β π (((π₯πΆπ’) < π€ β§ (π¦π·π£) < π€) β ((π₯πΉπ¦)πΈ(π’πΉπ£)) < π§)))) |
18 | 17 | adantlr 714 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ πΉ:(π Γ π)βΆπ) β§ (π₯ β π β§ π¦ β π)) β (πΉ β (((π½ Γt πΎ) CnP πΏ)ββ¨π₯, π¦β©) β (πΉ:(π Γ π)βΆπ β§ βπ§ β β+ βπ€ β β+
βπ’ β π βπ£ β π (((π₯πΆπ’) < π€ β§ (π¦π·π£) < π€) β ((π₯πΉπ¦)πΈ(π’πΉπ£)) < π§)))) |
19 | 16, 18 | mpbirand 706 |
. . . . 5
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ πΉ:(π Γ π)βΆπ) β§ (π₯ β π β§ π¦ β π)) β (πΉ β (((π½ Γt πΎ) CnP πΏ)ββ¨π₯, π¦β©) β βπ§ β β+ βπ€ β β+
βπ’ β π βπ£ β π (((π₯πΆπ’) < π€ β§ (π¦π·π£) < π€) β ((π₯πΉπ¦)πΈ(π’πΉπ£)) < π§))) |
20 | 19 | 2ralbidva 3207 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ πΉ:(π Γ π)βΆπ) β (βπ₯ β π βπ¦ β π πΉ β (((π½ Γt πΎ) CnP πΏ)ββ¨π₯, π¦β©) β βπ₯ β π βπ¦ β π βπ§ β β+ βπ€ β β+
βπ’ β π βπ£ β π (((π₯πΆπ’) < π€ β§ (π¦π·π£) < π€) β ((π₯πΉπ¦)πΈ(π’πΉπ£)) < π§))) |
21 | 15, 20 | bitrid 283 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ πΉ:(π Γ π)βΆπ) β (βπ‘ β (π Γ π)πΉ β (((π½ Γt πΎ) CnP πΏ)βπ‘) β βπ₯ β π βπ¦ β π βπ§ β β+ βπ€ β β+
βπ’ β π βπ£ β π (((π₯πΆπ’) < π€ β§ (π¦π·π£) < π€) β ((π₯πΉπ¦)πΈ(π’πΉπ£)) < π§))) |
22 | 21 | pm5.32da 580 |
. 2
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β ((πΉ:(π Γ π)βΆπ β§ βπ‘ β (π Γ π)πΉ β (((π½ Γt πΎ) CnP πΏ)βπ‘)) β (πΉ:(π Γ π)βΆπ β§ βπ₯ β π βπ¦ β π βπ§ β β+ βπ€ β β+
βπ’ β π βπ£ β π (((π₯πΆπ’) < π€ β§ (π¦π·π£) < π€) β ((π₯πΉπ¦)πΈ(π’πΉπ£)) < π§)))) |
23 | 12, 22 | bitrd 279 |
1
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β (πΉ β ((π½ Γt πΎ) Cn πΏ) β (πΉ:(π Γ π)βΆπ β§ βπ₯ β π βπ¦ β π βπ§ β β+ βπ€ β β+
βπ’ β π βπ£ β π (((π₯πΆπ’) < π€ β§ (π¦π·π£) < π€) β ((π₯πΉπ¦)πΈ(π’πΉπ£)) < π§)))) |