Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’
(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·))) =
(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·))) |
2 | | simpl1 1192 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β πΆ β (βMetβπ)) |
3 | | simpl2 1193 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β π· β (βMetβπ)) |
4 | 1, 2, 3 | tmsxps 23908 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β (distβ((toMetSpβπΆ) Γs
(toMetSpβπ·))) β
(βMetβ(π
Γ π))) |
5 | | simpl3 1194 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β πΈ β (βMetβπ)) |
6 | | opelxpi 5671 |
. . . 4
β’ ((π΄ β π β§ π΅ β π) β β¨π΄, π΅β© β (π Γ π)) |
7 | 6 | adantl 483 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β β¨π΄, π΅β© β (π Γ π)) |
8 | | eqid 2733 |
. . . 4
β’
(MetOpenβ(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))) =
(MetOpenβ(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))) |
9 | | txmetcnp.4 |
. . . 4
β’ πΏ = (MetOpenβπΈ) |
10 | 8, 9 | metcnp 23913 |
. . 3
β’
(((distβ((toMetSpβπΆ) Γs
(toMetSpβπ·))) β
(βMetβ(π
Γ π)) β§ πΈ β (βMetβπ) β§ β¨π΄, π΅β© β (π Γ π)) β (πΉ β
(((MetOpenβ(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))) CnP
πΏ)ββ¨π΄, π΅β©) β (πΉ:(π Γ π)βΆπ β§ βπ§ β β+ βπ€ β β+
βπ₯ β (π Γ π)((β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))π₯) < π€ β ((πΉββ¨π΄, π΅β©)πΈ(πΉβπ₯)) < π§)))) |
11 | 4, 5, 7, 10 | syl3anc 1372 |
. 2
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β (πΉ β
(((MetOpenβ(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))) CnP
πΏ)ββ¨π΄, π΅β©) β (πΉ:(π Γ π)βΆπ β§ βπ§ β β+ βπ€ β β+
βπ₯ β (π Γ π)((β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))π₯) < π€ β ((πΉββ¨π΄, π΅β©)πΈ(πΉβπ₯)) < π§)))) |
12 | | metcn.2 |
. . . . . 6
β’ π½ = (MetOpenβπΆ) |
13 | | metcn.4 |
. . . . . 6
β’ πΎ = (MetOpenβπ·) |
14 | 1, 2, 3, 12, 13, 8 | tmsxpsmopn 23909 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β
(MetOpenβ(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))) =
(π½ Γt
πΎ)) |
15 | 14 | oveq1d 7373 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β
((MetOpenβ(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))) CnP
πΏ) = ((π½ Γt πΎ) CnP πΏ)) |
16 | 15 | fveq1d 6845 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β
(((MetOpenβ(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))) CnP
πΏ)ββ¨π΄, π΅β©) = (((π½ Γt πΎ) CnP πΏ)ββ¨π΄, π΅β©)) |
17 | 16 | eleq2d 2820 |
. 2
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β (πΉ β
(((MetOpenβ(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))) CnP
πΏ)ββ¨π΄, π΅β©) β πΉ β (((π½ Γt πΎ) CnP πΏ)ββ¨π΄, π΅β©))) |
18 | | oveq2 7366 |
. . . . . . . . 9
β’ (π₯ = β¨π’, π£β© β (β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))π₯) = (β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))β¨π’, π£β©)) |
19 | 18 | breq1d 5116 |
. . . . . . . 8
β’ (π₯ = β¨π’, π£β© β ((β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))π₯) < π€ β (β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))β¨π’, π£β©) < π€)) |
20 | | df-ov 7361 |
. . . . . . . . . . 11
β’ (π΄πΉπ΅) = (πΉββ¨π΄, π΅β©) |
21 | 20 | oveq1i 7368 |
. . . . . . . . . 10
β’ ((π΄πΉπ΅)πΈ(πΉβπ₯)) = ((πΉββ¨π΄, π΅β©)πΈ(πΉβπ₯)) |
22 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π₯ = β¨π’, π£β© β (πΉβπ₯) = (πΉββ¨π’, π£β©)) |
23 | | df-ov 7361 |
. . . . . . . . . . . 12
β’ (π’πΉπ£) = (πΉββ¨π’, π£β©) |
24 | 22, 23 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π₯ = β¨π’, π£β© β (πΉβπ₯) = (π’πΉπ£)) |
25 | 24 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π₯ = β¨π’, π£β© β ((π΄πΉπ΅)πΈ(πΉβπ₯)) = ((π΄πΉπ΅)πΈ(π’πΉπ£))) |
26 | 21, 25 | eqtr3id 2787 |
. . . . . . . . 9
β’ (π₯ = β¨π’, π£β© β ((πΉββ¨π΄, π΅β©)πΈ(πΉβπ₯)) = ((π΄πΉπ΅)πΈ(π’πΉπ£))) |
27 | 26 | breq1d 5116 |
. . . . . . . 8
β’ (π₯ = β¨π’, π£β© β (((πΉββ¨π΄, π΅β©)πΈ(πΉβπ₯)) < π§ β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§)) |
28 | 19, 27 | imbi12d 345 |
. . . . . . 7
β’ (π₯ = β¨π’, π£β© β (((β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))π₯) < π€ β ((πΉββ¨π΄, π΅β©)πΈ(πΉβπ₯)) < π§) β ((β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))β¨π’, π£β©) < π€ β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§))) |
29 | 28 | ralxp 5798 |
. . . . . 6
β’
(βπ₯ β
(π Γ π)((β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))π₯) < π€ β ((πΉββ¨π΄, π΅β©)πΈ(πΉβπ₯)) < π§) β βπ’ β π βπ£ β π ((β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))β¨π’, π£β©) < π€ β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§)) |
30 | 2 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ (π€ β β+ β§ (π’ β π β§ π£ β π))) β πΆ β (βMetβπ)) |
31 | 3 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ (π€ β β+ β§ (π’ β π β§ π£ β π))) β π· β (βMetβπ)) |
32 | | simpllr 775 |
. . . . . . . . . . . . 13
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ (π€ β β+ β§ (π’ β π β§ π£ β π))) β (π΄ β π β§ π΅ β π)) |
33 | 32 | simpld 496 |
. . . . . . . . . . . 12
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ (π€ β β+ β§ (π’ β π β§ π£ β π))) β π΄ β π) |
34 | 32 | simprd 497 |
. . . . . . . . . . . 12
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ (π€ β β+ β§ (π’ β π β§ π£ β π))) β π΅ β π) |
35 | | simprrl 780 |
. . . . . . . . . . . 12
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ (π€ β β+ β§ (π’ β π β§ π£ β π))) β π’ β π) |
36 | | simprrr 781 |
. . . . . . . . . . . 12
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ (π€ β β+ β§ (π’ β π β§ π£ β π))) β π£ β π) |
37 | 1, 30, 31, 33, 34, 35, 36 | tmsxpsval2 23911 |
. . . . . . . . . . 11
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ (π€ β β+ β§ (π’ β π β§ π£ β π))) β (β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))β¨π’, π£β©) = if((π΄πΆπ’) β€ (π΅π·π£), (π΅π·π£), (π΄πΆπ’))) |
38 | 37 | breq1d 5116 |
. . . . . . . . . 10
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ (π€ β β+ β§ (π’ β π β§ π£ β π))) β ((β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))β¨π’, π£β©) < π€ β if((π΄πΆπ’) β€ (π΅π·π£), (π΅π·π£), (π΄πΆπ’)) < π€)) |
39 | | xmetcl 23700 |
. . . . . . . . . . . 12
β’ ((πΆ β (βMetβπ) β§ π΄ β π β§ π’ β π) β (π΄πΆπ’) β
β*) |
40 | 30, 33, 35, 39 | syl3anc 1372 |
. . . . . . . . . . 11
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ (π€ β β+ β§ (π’ β π β§ π£ β π))) β (π΄πΆπ’) β
β*) |
41 | | xmetcl 23700 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ π΅ β π β§ π£ β π) β (π΅π·π£) β
β*) |
42 | 31, 34, 36, 41 | syl3anc 1372 |
. . . . . . . . . . 11
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ (π€ β β+ β§ (π’ β π β§ π£ β π))) β (π΅π·π£) β
β*) |
43 | | rpxr 12929 |
. . . . . . . . . . . 12
β’ (π€ β β+
β π€ β
β*) |
44 | 43 | ad2antrl 727 |
. . . . . . . . . . 11
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ (π€ β β+ β§ (π’ β π β§ π£ β π))) β π€ β β*) |
45 | | xrmaxlt 13106 |
. . . . . . . . . . 11
β’ (((π΄πΆπ’) β β* β§ (π΅π·π£) β β* β§ π€ β β*)
β (if((π΄πΆπ’) β€ (π΅π·π£), (π΅π·π£), (π΄πΆπ’)) < π€ β ((π΄πΆπ’) < π€ β§ (π΅π·π£) < π€))) |
46 | 40, 42, 44, 45 | syl3anc 1372 |
. . . . . . . . . 10
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ (π€ β β+ β§ (π’ β π β§ π£ β π))) β (if((π΄πΆπ’) β€ (π΅π·π£), (π΅π·π£), (π΄πΆπ’)) < π€ β ((π΄πΆπ’) < π€ β§ (π΅π·π£) < π€))) |
47 | 38, 46 | bitrd 279 |
. . . . . . . . 9
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ (π€ β β+ β§ (π’ β π β§ π£ β π))) β ((β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))β¨π’, π£β©) < π€ β ((π΄πΆπ’) < π€ β§ (π΅π·π£) < π€))) |
48 | 47 | imbi1d 342 |
. . . . . . . 8
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ (π€ β β+ β§ (π’ β π β§ π£ β π))) β (((β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))β¨π’, π£β©) < π€ β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§) β (((π΄πΆπ’) < π€ β§ (π΅π·π£) < π€) β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§))) |
49 | 48 | anassrs 469 |
. . . . . . 7
β’
((((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ π€ β β+) β§ (π’ β π β§ π£ β π)) β (((β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))β¨π’, π£β©) < π€ β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§) β (((π΄πΆπ’) < π€ β§ (π΅π·π£) < π€) β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§))) |
50 | 49 | 2ralbidva 3207 |
. . . . . 6
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ π€ β β+) β
(βπ’ β π βπ£ β π ((β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))β¨π’, π£β©) < π€ β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§) β βπ’ β π βπ£ β π (((π΄πΆπ’) < π€ β§ (π΅π·π£) < π€) β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§))) |
51 | 29, 50 | bitrid 283 |
. . . . 5
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
πΈ β
(βMetβπ)) β§
(π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β§ π€ β β+) β
(βπ₯ β (π Γ π)((β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))π₯) < π€ β ((πΉββ¨π΄, π΅β©)πΈ(πΉβπ₯)) < π§) β βπ’ β π βπ£ β π (((π΄πΆπ’) < π€ β§ (π΅π·π£) < π€) β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§))) |
52 | 51 | rexbidva 3170 |
. . . 4
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β (βπ€ β β+ βπ₯ β (π Γ π)((β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))π₯) < π€ β ((πΉββ¨π΄, π΅β©)πΈ(πΉβπ₯)) < π§) β βπ€ β β+ βπ’ β π βπ£ β π (((π΄πΆπ’) < π€ β§ (π΅π·π£) < π€) β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§))) |
53 | 52 | ralbidv 3171 |
. . 3
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β§ πΉ:(π Γ π)βΆπ) β (βπ§ β β+ βπ€ β β+
βπ₯ β (π Γ π)((β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))π₯) < π€ β ((πΉββ¨π΄, π΅β©)πΈ(πΉβπ₯)) < π§) β βπ§ β β+ βπ€ β β+
βπ’ β π βπ£ β π (((π΄πΆπ’) < π€ β§ (π΅π·π£) < π€) β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§))) |
54 | 53 | pm5.32da 580 |
. 2
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β ((πΉ:(π Γ π)βΆπ β§ βπ§ β β+ βπ€ β β+
βπ₯ β (π Γ π)((β¨π΄, π΅β©(distβ((toMetSpβπΆ) Γs
(toMetSpβπ·)))π₯) < π€ β ((πΉββ¨π΄, π΅β©)πΈ(πΉβπ₯)) < π§)) β (πΉ:(π Γ π)βΆπ β§ βπ§ β β+ βπ€ β β+
βπ’ β π βπ£ β π (((π΄πΆπ’) < π€ β§ (π΅π·π£) < π€) β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§)))) |
55 | 11, 17, 54 | 3bitr3d 309 |
1
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β (πΉ β (((π½ Γt πΎ) CnP πΏ)ββ¨π΄, π΅β©) β (πΉ:(π Γ π)βΆπ β§ βπ§ β β+ βπ€ β β+
βπ’ β π βπ£ β π (((π΄πΆπ’) < π€ β§ (π΅π·π£) < π€) β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§)))) |