Step | Hyp | Ref
| Expression |
1 | | xmetxp.p |
. . 3
β’ π = (π’ β (π Γ π), π£ β (π Γ π) β¦ sup({((1st βπ’)π(1st βπ£)), ((2nd βπ’)π(2nd βπ£))}, β*, <
)) |
2 | | xmetxp.1 |
. . 3
β’ (π β π β (βMetβπ)) |
3 | | xmetxp.2 |
. . 3
β’ (π β π β (βMetβπ)) |
4 | | xmettx.j |
. . 3
β’ π½ = (MetOpenβπ) |
5 | | xmettx.k |
. . 3
β’ πΎ = (MetOpenβπ) |
6 | | xmettx.l |
. . 3
β’ πΏ = (MetOpenβπ) |
7 | 1, 2, 3, 4, 5, 6 | xmettxlem 13945 |
. 2
β’ (π β πΏ β (π½ Γt πΎ)) |
8 | | eqid 2177 |
. . . . . . . . . . . 12
β’ (π β π½, π β πΎ β¦ (π Γ π )) = (π β π½, π β πΎ β¦ (π Γ π )) |
9 | 8 | elrnmpog 5986 |
. . . . . . . . . . 11
β’ (π€ β V β (π€ β ran (π β π½, π β πΎ β¦ (π Γ π )) β βπ β π½ βπ β πΎ π€ = (π Γ π ))) |
10 | 9 | elv 2741 |
. . . . . . . . . 10
β’ (π€ β ran (π β π½, π β πΎ β¦ (π Γ π )) β βπ β π½ βπ β πΎ π€ = (π Γ π )) |
11 | 10 | biimpi 120 |
. . . . . . . . 9
β’ (π€ β ran (π β π½, π β πΎ β¦ (π Γ π )) β βπ β π½ βπ β πΎ π€ = (π Γ π )) |
12 | 11 | adantl 277 |
. . . . . . . 8
β’ ((π β§ π€ β ran (π β π½, π β πΎ β¦ (π Γ π ))) β βπ β π½ βπ β πΎ π€ = (π Γ π )) |
13 | | xpeq1 4640 |
. . . . . . . . . 10
β’ (π = π₯ β (π Γ π ) = (π₯ Γ π )) |
14 | 13 | eqeq2d 2189 |
. . . . . . . . 9
β’ (π = π₯ β (π€ = (π Γ π ) β π€ = (π₯ Γ π ))) |
15 | | xpeq2 4641 |
. . . . . . . . . 10
β’ (π = π¦ β (π₯ Γ π ) = (π₯ Γ π¦)) |
16 | 15 | eqeq2d 2189 |
. . . . . . . . 9
β’ (π = π¦ β (π€ = (π₯ Γ π ) β π€ = (π₯ Γ π¦))) |
17 | 14, 16 | cbvrex2v 2717 |
. . . . . . . 8
β’
(βπ β
π½ βπ β πΎ π€ = (π Γ π ) β βπ₯ β π½ βπ¦ β πΎ π€ = (π₯ Γ π¦)) |
18 | 12, 17 | sylib 122 |
. . . . . . 7
β’ ((π β§ π€ β ran (π β π½, π β πΎ β¦ (π Γ π ))) β βπ₯ β π½ βπ¦ β πΎ π€ = (π₯ Γ π¦)) |
19 | | simpr 110 |
. . . . . . . . . 10
β’ ((((π β§ π€ β ran (π β π½, π β πΎ β¦ (π Γ π ))) β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π€ = (π₯ Γ π¦)) β π€ = (π₯ Γ π¦)) |
20 | | simplll 533 |
. . . . . . . . . . 11
β’ ((((π β§ π€ β ran (π β π½, π β πΎ β¦ (π Γ π ))) β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π€ = (π₯ Γ π¦)) β π) |
21 | | simplrl 535 |
. . . . . . . . . . 11
β’ ((((π β§ π€ β ran (π β π½, π β πΎ β¦ (π Γ π ))) β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π€ = (π₯ Γ π¦)) β π₯ β π½) |
22 | | simplrr 536 |
. . . . . . . . . . 11
β’ ((((π β§ π€ β ran (π β π½, π β πΎ β¦ (π Γ π ))) β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π€ = (π₯ Γ π¦)) β π¦ β πΎ) |
23 | 4 | mopntopon 13879 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (βMetβπ) β π½ β (TopOnβπ)) |
24 | 2, 23 | syl 14 |
. . . . . . . . . . . . . . . . 17
β’ (π β π½ β (TopOnβπ)) |
25 | 24 | adantr 276 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β π½ β§ π¦ β πΎ)) β π½ β (TopOnβπ)) |
26 | | simprl 529 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β π½ β§ π¦ β πΎ)) β π₯ β π½) |
27 | | toponss 13462 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β (TopOnβπ) β§ π₯ β π½) β π₯ β π) |
28 | 25, 26, 27 | syl2anc 411 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β π½ β§ π¦ β πΎ)) β π₯ β π) |
29 | 5 | mopntopon 13879 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (βMetβπ) β πΎ β (TopOnβπ)) |
30 | 3, 29 | syl 14 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΎ β (TopOnβπ)) |
31 | 30 | adantr 276 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β π½ β§ π¦ β πΎ)) β πΎ β (TopOnβπ)) |
32 | | simprr 531 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β π½ β§ π¦ β πΎ)) β π¦ β πΎ) |
33 | | toponss 13462 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β (TopOnβπ) β§ π¦ β πΎ) β π¦ β π) |
34 | 31, 32, 33 | syl2anc 411 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β π½ β§ π¦ β πΎ)) β π¦ β π) |
35 | | xpss12 4733 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β π β§ π¦ β π) β (π₯ Γ π¦) β (π Γ π)) |
36 | 28, 34, 35 | syl2anc 411 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β π½ β§ π¦ β πΎ)) β (π₯ Γ π¦) β (π Γ π)) |
37 | 1, 2, 3 | xmetxp 13943 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (βMetβ(π Γ π))) |
38 | | unirnbl 13859 |
. . . . . . . . . . . . . . . 16
β’ (π β (βMetβ(π Γ π)) β βͺ ran
(ballβπ) = (π Γ π)) |
39 | 37, 38 | syl 14 |
. . . . . . . . . . . . . . 15
β’ (π β βͺ ran (ballβπ) = (π Γ π)) |
40 | 39 | adantr 276 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β π½ β§ π¦ β πΎ)) β βͺ ran
(ballβπ) = (π Γ π)) |
41 | 36, 40 | sseqtrrd 3194 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π½ β§ π¦ β πΎ)) β (π₯ Γ π¦) β βͺ ran
(ballβπ)) |
42 | 2 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β π β (βMetβπ)) |
43 | | simplrl 535 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β π₯ β π½) |
44 | | xp1st 6165 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π₯ Γ π¦) β (1st βπ) β π₯) |
45 | 44 | adantl 277 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β (1st βπ) β π₯) |
46 | 4 | mopni2 13919 |
. . . . . . . . . . . . . . . 16
β’ ((π β (βMetβπ) β§ π₯ β π½ β§ (1st βπ) β π₯) β βπ β β+ ((1st
βπ)(ballβπ)π) β π₯) |
47 | 42, 43, 45, 46 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β βπ β β+ ((1st
βπ)(ballβπ)π) β π₯) |
48 | 3 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β π β (βMetβπ)) |
49 | | simplrr 536 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β π¦ β πΎ) |
50 | | xp2nd 6166 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π₯ Γ π¦) β (2nd βπ) β π¦) |
51 | 50 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β (2nd βπ) β π¦) |
52 | 5 | mopni2 13919 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (βMetβπ) β§ π¦ β πΎ β§ (2nd βπ) β π¦) β βπ β β+ ((2nd
βπ)(ballβπ)π) β π¦) |
53 | 48, 49, 51, 52 | syl3anc 1238 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β βπ β β+ ((2nd
βπ)(ballβπ)π) β π¦) |
54 | 53 | adantr 276 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β βπ β β+ ((2nd
βπ)(ballβπ)π) β π¦) |
55 | | blf 13846 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (βMetβ(π Γ π)) β (ballβπ):((π Γ π) Γ
β*)βΆπ« (π Γ π)) |
56 | 37, 55 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (ballβπ):((π Γ π) Γ
β*)βΆπ« (π Γ π)) |
57 | 56 | ffnd 5366 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (ballβπ) Fn ((π Γ π) Γ
β*)) |
58 | 57 | ad4antr 494 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β (ballβπ) Fn ((π Γ π) Γ
β*)) |
59 | 36 | sselda 3155 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β π β (π Γ π)) |
60 | 59 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β π β (π Γ π)) |
61 | | rpxr 9660 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β+
β π β
β*) |
62 | 61 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β π β β*) |
63 | 62 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β π β β*) |
64 | | rpxr 9660 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β+
β π β
β*) |
65 | 64 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β π β β*) |
66 | | xrmincl 11273 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β*
β§ π β
β*) β inf({π, π}, β*, < ) β
β*) |
67 | 63, 65, 66 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β inf({π, π}, β*, < ) β
β*) |
68 | | fnovrn 6021 |
. . . . . . . . . . . . . . . . . 18
β’
(((ballβπ) Fn
((π Γ π) Γ β*)
β§ π β (π Γ π) β§ inf({π, π}, β*, < ) β
β*) β (π(ballβπ)inf({π, π}, β*, < )) β ran
(ballβπ)) |
69 | 58, 60, 67, 68 | syl3anc 1238 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β (π(ballβπ)inf({π, π}, β*, < )) β ran
(ballβπ)) |
70 | | eleq2 2241 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π(ballβπ)inf({π, π}, β*, < )) β (π β π β π β (π(ballβπ)inf({π, π}, β*, <
)))) |
71 | | sseq1 3178 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π(ballβπ)inf({π, π}, β*, < )) β (π β (π₯ Γ π¦) β (π(ballβπ)inf({π, π}, β*, < )) β
(π₯ Γ π¦))) |
72 | 70, 71 | anbi12d 473 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π(ballβπ)inf({π, π}, β*, < )) β
((π β π β§ π β (π₯ Γ π¦)) β (π β (π(ballβπ)inf({π, π}, β*, < )) β§ (π(ballβπ)inf({π, π}, β*, < )) β
(π₯ Γ π¦)))) |
73 | 72 | adantl 277 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β§ π = (π(ballβπ)inf({π, π}, β*, < ))) β
((π β π β§ π β (π₯ Γ π¦)) β (π β (π(ballβπ)inf({π, π}, β*, < )) β§ (π(ballβπ)inf({π, π}, β*, < )) β
(π₯ Γ π¦)))) |
74 | 37 | ad4antr 494 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β π β (βMetβ(π Γ π))) |
75 | | simplrl 535 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β π β β+) |
76 | | simprl 529 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β π β β+) |
77 | | xrminrpcl 11281 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β+
β§ π β
β+) β inf({π, π}, β*, < ) β
β+) |
78 | 75, 76, 77 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β inf({π, π}, β*, < ) β
β+) |
79 | | blcntr 13852 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (βMetβ(π Γ π)) β§ π β (π Γ π) β§ inf({π, π}, β*, < ) β
β+) β π β (π(ballβπ)inf({π, π}, β*, <
))) |
80 | 74, 60, 78, 79 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β π β (π(ballβπ)inf({π, π}, β*, <
))) |
81 | 42 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β π β (βMetβπ)) |
82 | 48 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β π β (βMetβπ)) |
83 | 1, 81, 82, 67, 60 | xmetxpbl 13944 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β (π(ballβπ)inf({π, π}, β*, < )) =
(((1st βπ)(ballβπ)inf({π, π}, β*, < )) Γ
((2nd βπ)(ballβπ)inf({π, π}, β*, <
)))) |
84 | 28 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β π₯ β π) |
85 | 84, 45 | sseldd 3156 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β (1st βπ) β π) |
86 | 85 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β (1st βπ) β π) |
87 | | xrmin1inf 11274 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β*
β§ π β
β*) β inf({π, π}, β*, < ) β€ π) |
88 | 63, 65, 87 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β inf({π, π}, β*, < ) β€ π) |
89 | | ssbl 13862 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β (βMetβπ) β§ (1st
βπ) β π) β§ (inf({π, π}, β*, < ) β
β* β§ π
β β*) β§ inf({π, π}, β*, < ) β€ π) β ((1st
βπ)(ballβπ)inf({π, π}, β*, < )) β
((1st βπ)(ballβπ)π)) |
90 | 81, 86, 67, 63, 88, 89 | syl221anc 1249 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β ((1st βπ)(ballβπ)inf({π, π}, β*, < )) β
((1st βπ)(ballβπ)π)) |
91 | | simplrr 536 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β ((1st βπ)(ballβπ)π) β π₯) |
92 | 90, 91 | sstrd 3165 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β ((1st βπ)(ballβπ)inf({π, π}, β*, < )) β π₯) |
93 | 34 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β π¦ β π) |
94 | 93, 51 | sseldd 3156 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β (2nd βπ) β π) |
95 | 94 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β (2nd βπ) β π) |
96 | | xrmin2inf 11275 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β*
β§ π β
β*) β inf({π, π}, β*, < ) β€ π) |
97 | 63, 65, 96 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β inf({π, π}, β*, < ) β€ π) |
98 | | ssbl 13862 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β (βMetβπ) β§ (2nd
βπ) β π) β§ (inf({π, π}, β*, < ) β
β* β§ π
β β*) β§ inf({π, π}, β*, < ) β€ π) β ((2nd
βπ)(ballβπ)inf({π, π}, β*, < )) β
((2nd βπ)(ballβπ)π)) |
99 | 82, 95, 67, 65, 97, 98 | syl221anc 1249 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β ((2nd βπ)(ballβπ)inf({π, π}, β*, < )) β
((2nd βπ)(ballβπ)π)) |
100 | | simprr 531 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β ((2nd βπ)(ballβπ)π) β π¦) |
101 | 99, 100 | sstrd 3165 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β ((2nd βπ)(ballβπ)inf({π, π}, β*, < )) β π¦) |
102 | | xpss12 4733 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((1st βπ)(ballβπ)inf({π, π}, β*, < )) β π₯ β§ ((2nd
βπ)(ballβπ)inf({π, π}, β*, < )) β π¦) β (((1st
βπ)(ballβπ)inf({π, π}, β*, < )) Γ
((2nd βπ)(ballβπ)inf({π, π}, β*, < ))) β
(π₯ Γ π¦)) |
103 | 92, 101, 102 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β (((1st βπ)(ballβπ)inf({π, π}, β*, < )) Γ
((2nd βπ)(ballβπ)inf({π, π}, β*, < ))) β
(π₯ Γ π¦)) |
104 | 83, 103 | eqsstrd 3191 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β (π(ballβπ)inf({π, π}, β*, < )) β
(π₯ Γ π¦)) |
105 | 80, 104 | jca 306 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β (π β (π(ballβπ)inf({π, π}, β*, < )) β§ (π(ballβπ)inf({π, π}, β*, < )) β
(π₯ Γ π¦))) |
106 | 69, 73, 105 | rspcedvd 2847 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β§ (π β β+ β§
((2nd βπ)(ballβπ)π) β π¦)) β βπ β ran (ballβπ)(π β π β§ π β (π₯ Γ π¦))) |
107 | 54, 106 | rexlimddv 2599 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β§ (π β β+ β§
((1st βπ)(ballβπ)π) β π₯)) β βπ β ran (ballβπ)(π β π β§ π β (π₯ Γ π¦))) |
108 | 47, 107 | rexlimddv 2599 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π β (π₯ Γ π¦)) β βπ β ran (ballβπ)(π β π β§ π β (π₯ Γ π¦))) |
109 | 108 | ralrimiva 2550 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π½ β§ π¦ β πΎ)) β βπ β (π₯ Γ π¦)βπ β ran (ballβπ)(π β π β§ π β (π₯ Γ π¦))) |
110 | 41, 109 | jca 306 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π½ β§ π¦ β πΎ)) β ((π₯ Γ π¦) β βͺ ran
(ballβπ) β§
βπ β (π₯ Γ π¦)βπ β ran (ballβπ)(π β π β§ π β (π₯ Γ π¦)))) |
111 | | blex 13823 |
. . . . . . . . . . . . . . 15
β’ (π β (βMetβ(π Γ π)) β (ballβπ) β V) |
112 | 37, 111 | syl 14 |
. . . . . . . . . . . . . 14
β’ (π β (ballβπ) β V) |
113 | 112 | adantr 276 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π½ β§ π¦ β πΎ)) β (ballβπ) β V) |
114 | | rnexg 4892 |
. . . . . . . . . . . . 13
β’
((ballβπ)
β V β ran (ballβπ) β V) |
115 | | eltg2 13489 |
. . . . . . . . . . . . 13
β’ (ran
(ballβπ) β V
β ((π₯ Γ π¦) β (topGenβran
(ballβπ)) β
((π₯ Γ π¦) β βͺ ran (ballβπ) β§ βπ β (π₯ Γ π¦)βπ β ran (ballβπ)(π β π β§ π β (π₯ Γ π¦))))) |
116 | 113, 114,
115 | 3syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π½ β§ π¦ β πΎ)) β ((π₯ Γ π¦) β (topGenβran (ballβπ)) β ((π₯ Γ π¦) β βͺ ran
(ballβπ) β§
βπ β (π₯ Γ π¦)βπ β ran (ballβπ)(π β π β§ π β (π₯ Γ π¦))))) |
117 | 110, 116 | mpbird 167 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π½ β§ π¦ β πΎ)) β (π₯ Γ π¦) β (topGenβran (ballβπ))) |
118 | 20, 21, 22, 117 | syl12anc 1236 |
. . . . . . . . . 10
β’ ((((π β§ π€ β ran (π β π½, π β πΎ β¦ (π Γ π ))) β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π€ = (π₯ Γ π¦)) β (π₯ Γ π¦) β (topGenβran (ballβπ))) |
119 | 19, 118 | eqeltrd 2254 |
. . . . . . . . 9
β’ ((((π β§ π€ β ran (π β π½, π β πΎ β¦ (π Γ π ))) β§ (π₯ β π½ β§ π¦ β πΎ)) β§ π€ = (π₯ Γ π¦)) β π€ β (topGenβran (ballβπ))) |
120 | 119 | ex 115 |
. . . . . . . 8
β’ (((π β§ π€ β ran (π β π½, π β πΎ β¦ (π Γ π ))) β§ (π₯ β π½ β§ π¦ β πΎ)) β (π€ = (π₯ Γ π¦) β π€ β (topGenβran (ballβπ)))) |
121 | 120 | rexlimdvva 2602 |
. . . . . . 7
β’ ((π β§ π€ β ran (π β π½, π β πΎ β¦ (π Γ π ))) β (βπ₯ β π½ βπ¦ β πΎ π€ = (π₯ Γ π¦) β π€ β (topGenβran (ballβπ)))) |
122 | 18, 121 | mpd 13 |
. . . . . 6
β’ ((π β§ π€ β ran (π β π½, π β πΎ β¦ (π Γ π ))) β π€ β (topGenβran (ballβπ))) |
123 | 122 | ex 115 |
. . . . 5
β’ (π β (π€ β ran (π β π½, π β πΎ β¦ (π Γ π )) β π€ β (topGenβran (ballβπ)))) |
124 | 123 | ssrdv 3161 |
. . . 4
β’ (π β ran (π β π½, π β πΎ β¦ (π Γ π )) β (topGenβran
(ballβπ))) |
125 | 4 | mopntop 13880 |
. . . . . . . 8
β’ (π β (βMetβπ) β π½ β Top) |
126 | 2, 125 | syl 14 |
. . . . . . 7
β’ (π β π½ β Top) |
127 | 5 | mopntop 13880 |
. . . . . . . 8
β’ (π β (βMetβπ) β πΎ β Top) |
128 | 3, 127 | syl 14 |
. . . . . . 7
β’ (π β πΎ β Top) |
129 | | mpoexga 6212 |
. . . . . . 7
β’ ((π½ β Top β§ πΎ β Top) β (π β π½, π β πΎ β¦ (π Γ π )) β V) |
130 | 126, 128,
129 | syl2anc 411 |
. . . . . 6
β’ (π β (π β π½, π β πΎ β¦ (π Γ π )) β V) |
131 | | rnexg 4892 |
. . . . . 6
β’ ((π β π½, π β πΎ β¦ (π Γ π )) β V β ran (π β π½, π β πΎ β¦ (π Γ π )) β V) |
132 | 130, 131 | syl 14 |
. . . . 5
β’ (π β ran (π β π½, π β πΎ β¦ (π Γ π )) β V) |
133 | 37, 111, 114 | 3syl 17 |
. . . . 5
β’ (π β ran (ballβπ) β V) |
134 | | tgss3 13514 |
. . . . 5
β’ ((ran
(π β π½, π β πΎ β¦ (π Γ π )) β V β§ ran (ballβπ) β V) β
((topGenβran (π
β π½, π β πΎ β¦ (π Γ π ))) β (topGenβran
(ballβπ)) β ran
(π β π½, π β πΎ β¦ (π Γ π )) β (topGenβran
(ballβπ)))) |
135 | 132, 133,
134 | syl2anc 411 |
. . . 4
β’ (π β ((topGenβran (π β π½, π β πΎ β¦ (π Γ π ))) β (topGenβran
(ballβπ)) β ran
(π β π½, π β πΎ β¦ (π Γ π )) β (topGenβran
(ballβπ)))) |
136 | 124, 135 | mpbird 167 |
. . 3
β’ (π β (topGenβran (π β π½, π β πΎ β¦ (π Γ π ))) β (topGenβran
(ballβπ))) |
137 | | eqid 2177 |
. . . . 5
β’ ran
(π β π½, π β πΎ β¦ (π Γ π )) = ran (π β π½, π β πΎ β¦ (π Γ π )) |
138 | 137 | txval 13691 |
. . . 4
β’ ((π½ β Top β§ πΎ β Top) β (π½ Γt πΎ) = (topGenβran (π β π½, π β πΎ β¦ (π Γ π )))) |
139 | 126, 128,
138 | syl2anc 411 |
. . 3
β’ (π β (π½ Γt πΎ) = (topGenβran (π β π½, π β πΎ β¦ (π Γ π )))) |
140 | 6 | mopnval 13878 |
. . . 4
β’ (π β (βMetβ(π Γ π)) β πΏ = (topGenβran (ballβπ))) |
141 | 37, 140 | syl 14 |
. . 3
β’ (π β πΏ = (topGenβran (ballβπ))) |
142 | 136, 139,
141 | 3sstr4d 3200 |
. 2
β’ (π β (π½ Γt πΎ) β πΏ) |
143 | 7, 142 | eqssd 3172 |
1
β’ (π β πΏ = (π½ Γt πΎ)) |