Step | Hyp | Ref
| Expression |
1 | | xmetxp.1 |
. . . 4
β’ (π β π β (βMetβπ)) |
2 | | eqid 2177 |
. . . . 5
β’
(MetOpenβπ) =
(MetOpenβπ) |
3 | 2 | mopnm 13918 |
. . . 4
β’ (π β (βMetβπ) β π β (MetOpenβπ)) |
4 | 1, 3 | syl 14 |
. . 3
β’ (π β π β (MetOpenβπ)) |
5 | | xmetxp.2 |
. . . 4
β’ (π β π β (βMetβπ)) |
6 | | eqid 2177 |
. . . . 5
β’
(MetOpenβπ) =
(MetOpenβπ) |
7 | 6 | mopnm 13918 |
. . . 4
β’ (π β (βMetβπ) β π β (MetOpenβπ)) |
8 | 5, 7 | syl 14 |
. . 3
β’ (π β π β (MetOpenβπ)) |
9 | | xpexg 4740 |
. . 3
β’ ((π β (MetOpenβπ) β§ π β (MetOpenβπ)) β (π Γ π) β V) |
10 | 4, 8, 9 | syl2anc 411 |
. 2
β’ (π β (π Γ π) β V) |
11 | 1 | adantr 276 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β π β (βMetβπ)) |
12 | | xp1st 6165 |
. . . . . . 7
β’ (π β (π Γ π) β (1st βπ) β π) |
13 | 12 | ad2antrl 490 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β (1st βπ) β π) |
14 | | xp1st 6165 |
. . . . . . 7
β’ (π β (π Γ π) β (1st βπ ) β π) |
15 | 14 | ad2antll 491 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β (1st βπ ) β π) |
16 | | xmetcl 13822 |
. . . . . 6
β’ ((π β (βMetβπ) β§ (1st
βπ) β π β§ (1st
βπ ) β π) β ((1st
βπ)π(1st βπ )) β
β*) |
17 | 11, 13, 15, 16 | syl3anc 1238 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β ((1st βπ)π(1st βπ )) β
β*) |
18 | 5 | adantr 276 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β π β (βMetβπ)) |
19 | | xp2nd 6166 |
. . . . . . 7
β’ (π β (π Γ π) β (2nd βπ) β π) |
20 | 19 | ad2antrl 490 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β (2nd βπ) β π) |
21 | | xp2nd 6166 |
. . . . . . 7
β’ (π β (π Γ π) β (2nd βπ ) β π) |
22 | 21 | ad2antll 491 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β (2nd βπ ) β π) |
23 | | xmetcl 13822 |
. . . . . 6
β’ ((π β (βMetβπ) β§ (2nd
βπ) β π β§ (2nd
βπ ) β π) β ((2nd
βπ)π(2nd βπ )) β
β*) |
24 | 18, 20, 22, 23 | syl3anc 1238 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β ((2nd βπ)π(2nd βπ )) β
β*) |
25 | | xrmaxcl 11259 |
. . . . 5
β’
((((1st βπ)π(1st βπ )) β β* β§
((2nd βπ)π(2nd βπ )) β β*) β
sup({((1st βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, < ) β
β*) |
26 | 17, 24, 25 | syl2anc 411 |
. . . 4
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β sup({((1st
βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, < ) β
β*) |
27 | 26 | ralrimivva 2559 |
. . 3
β’ (π β βπ β (π Γ π)βπ β (π Γ π)sup({((1st βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, < ) β
β*) |
28 | | xmetxp.p |
. . . . 5
β’ π = (π’ β (π Γ π), π£ β (π Γ π) β¦ sup({((1st βπ’)π(1st βπ£)), ((2nd βπ’)π(2nd βπ£))}, β*, <
)) |
29 | | fveq2 5515 |
. . . . . . . . 9
β’ (π’ = π β (1st βπ’) = (1st βπ)) |
30 | 29 | oveq1d 5889 |
. . . . . . . 8
β’ (π’ = π β ((1st βπ’)π(1st βπ£)) = ((1st βπ)π(1st βπ£))) |
31 | | fveq2 5515 |
. . . . . . . . 9
β’ (π’ = π β (2nd βπ’) = (2nd βπ)) |
32 | 31 | oveq1d 5889 |
. . . . . . . 8
β’ (π’ = π β ((2nd βπ’)π(2nd βπ£)) = ((2nd βπ)π(2nd βπ£))) |
33 | 30, 32 | preq12d 3677 |
. . . . . . 7
β’ (π’ = π β {((1st βπ’)π(1st βπ£)), ((2nd βπ’)π(2nd βπ£))} = {((1st βπ)π(1st βπ£)), ((2nd βπ)π(2nd βπ£))}) |
34 | 33 | supeq1d 6985 |
. . . . . 6
β’ (π’ = π β sup({((1st βπ’)π(1st βπ£)), ((2nd βπ’)π(2nd βπ£))}, β*, < ) =
sup({((1st βπ)π(1st βπ£)), ((2nd βπ)π(2nd βπ£))}, β*, <
)) |
35 | | fveq2 5515 |
. . . . . . . . 9
β’ (π£ = π β (1st βπ£) = (1st βπ )) |
36 | 35 | oveq2d 5890 |
. . . . . . . 8
β’ (π£ = π β ((1st βπ)π(1st βπ£)) = ((1st βπ)π(1st βπ ))) |
37 | | fveq2 5515 |
. . . . . . . . 9
β’ (π£ = π β (2nd βπ£) = (2nd βπ )) |
38 | 37 | oveq2d 5890 |
. . . . . . . 8
β’ (π£ = π β ((2nd βπ)π(2nd βπ£)) = ((2nd βπ)π(2nd βπ ))) |
39 | 36, 38 | preq12d 3677 |
. . . . . . 7
β’ (π£ = π β {((1st βπ)π(1st βπ£)), ((2nd βπ)π(2nd βπ£))} = {((1st βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}) |
40 | 39 | supeq1d 6985 |
. . . . . 6
β’ (π£ = π β sup({((1st βπ)π(1st βπ£)), ((2nd βπ)π(2nd βπ£))}, β*, < ) =
sup({((1st βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, <
)) |
41 | 34, 40 | cbvmpov 5954 |
. . . . 5
β’ (π’ β (π Γ π), π£ β (π Γ π) β¦ sup({((1st βπ’)π(1st βπ£)), ((2nd βπ’)π(2nd βπ£))}, β*, < )) = (π β (π Γ π), π β (π Γ π) β¦ sup({((1st βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, <
)) |
42 | 28, 41 | eqtri 2198 |
. . . 4
β’ π = (π β (π Γ π), π β (π Γ π) β¦ sup({((1st βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, <
)) |
43 | 42 | fmpo 6201 |
. . 3
β’
(βπ β
(π Γ π)βπ β (π Γ π)sup({((1st βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, < ) β
β* β π:((π Γ π) Γ (π Γ π))βΆβ*) |
44 | 27, 43 | sylib 122 |
. 2
β’ (π β π:((π Γ π) Γ (π Γ π))βΆβ*) |
45 | | simprl 529 |
. . . . . . . 8
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β π β (π Γ π)) |
46 | | simprr 531 |
. . . . . . . 8
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β π β (π Γ π)) |
47 | 34, 40, 28 | ovmpog 6008 |
. . . . . . . 8
β’ ((π β (π Γ π) β§ π β (π Γ π) β§ sup({((1st βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, < ) β
β*) β (πππ ) = sup({((1st βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, <
)) |
48 | 45, 46, 26, 47 | syl3anc 1238 |
. . . . . . 7
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β (πππ ) = sup({((1st βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, <
)) |
49 | 48, 26 | eqeltrd 2254 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β (πππ ) β
β*) |
50 | | 0xr 8003 |
. . . . . . 7
β’ 0 β
β* |
51 | 50 | a1i 9 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β 0 β
β*) |
52 | | xrletri3 9803 |
. . . . . 6
β’ (((πππ ) β β* β§ 0 β
β*) β ((πππ ) = 0 β ((πππ ) β€ 0 β§ 0 β€ (πππ )))) |
53 | 49, 51, 52 | syl2anc 411 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β ((πππ ) = 0 β ((πππ ) β€ 0 β§ 0 β€ (πππ )))) |
54 | | xmetge0 13835 |
. . . . . . . . 9
β’ ((π β (βMetβπ) β§ (1st
βπ) β π β§ (1st
βπ ) β π) β 0 β€ ((1st
βπ)π(1st βπ ))) |
55 | 11, 13, 15, 54 | syl3anc 1238 |
. . . . . . . 8
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β 0 β€ ((1st
βπ)π(1st βπ ))) |
56 | | xrmax1sup 11260 |
. . . . . . . . 9
β’
((((1st βπ)π(1st βπ )) β β* β§
((2nd βπ)π(2nd βπ )) β β*) β
((1st βπ)π(1st βπ )) β€ sup({((1st βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, <
)) |
57 | 17, 24, 56 | syl2anc 411 |
. . . . . . . 8
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β ((1st βπ)π(1st βπ )) β€ sup({((1st βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, <
)) |
58 | 51, 17, 26, 55, 57 | xrletrd 9811 |
. . . . . . 7
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β 0 β€ sup({((1st
βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, <
)) |
59 | 58, 48 | breqtrrd 4031 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β 0 β€ (πππ )) |
60 | 59 | biantrud 304 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β ((πππ ) β€ 0 β ((πππ ) β€ 0 β§ 0 β€ (πππ )))) |
61 | 53, 60 | bitr4d 191 |
. . . 4
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β ((πππ ) = 0 β (πππ ) β€ 0)) |
62 | 48 | breq1d 4013 |
. . . 4
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β ((πππ ) β€ 0 β sup({((1st
βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, < ) β€
0)) |
63 | | xrmaxlesup 11266 |
. . . . 5
β’
((((1st βπ)π(1st βπ )) β β* β§
((2nd βπ)π(2nd βπ )) β β* β§ 0 β
β*) β (sup({((1st βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, < ) β€ 0
β (((1st βπ)π(1st βπ )) β€ 0 β§ ((2nd βπ)π(2nd βπ )) β€ 0))) |
64 | 17, 24, 51, 63 | syl3anc 1238 |
. . . 4
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β (sup({((1st
βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, < ) β€ 0
β (((1st βπ)π(1st βπ )) β€ 0 β§ ((2nd βπ)π(2nd βπ )) β€ 0))) |
65 | 61, 62, 64 | 3bitrd 214 |
. . 3
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β ((πππ ) = 0 β (((1st βπ)π(1st βπ )) β€ 0 β§ ((2nd βπ)π(2nd βπ )) β€ 0))) |
66 | 55 | biantrud 304 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β (((1st βπ)π(1st βπ )) β€ 0 β (((1st
βπ)π(1st βπ )) β€ 0 β§ 0 β€ ((1st
βπ)π(1st βπ ))))) |
67 | | xrletri3 9803 |
. . . . . 6
β’
((((1st βπ)π(1st βπ )) β β* β§ 0 β
β*) β (((1st βπ)π(1st βπ )) = 0 β (((1st βπ)π(1st βπ )) β€ 0 β§ 0 β€ ((1st
βπ)π(1st βπ ))))) |
68 | 17, 51, 67 | syl2anc 411 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β (((1st βπ)π(1st βπ )) = 0 β (((1st βπ)π(1st βπ )) β€ 0 β§ 0 β€ ((1st
βπ)π(1st βπ ))))) |
69 | 66, 68 | bitr4d 191 |
. . . 4
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β (((1st βπ)π(1st βπ )) β€ 0 β ((1st
βπ)π(1st βπ )) = 0)) |
70 | | xmetge0 13835 |
. . . . . . 7
β’ ((π β (βMetβπ) β§ (2nd
βπ) β π β§ (2nd
βπ ) β π) β 0 β€ ((2nd
βπ)π(2nd βπ ))) |
71 | 18, 20, 22, 70 | syl3anc 1238 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β 0 β€ ((2nd
βπ)π(2nd βπ ))) |
72 | 71 | biantrud 304 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β (((2nd βπ)π(2nd βπ )) β€ 0 β (((2nd
βπ)π(2nd βπ )) β€ 0 β§ 0 β€ ((2nd
βπ)π(2nd βπ ))))) |
73 | | xrletri3 9803 |
. . . . . 6
β’
((((2nd βπ)π(2nd βπ )) β β* β§ 0 β
β*) β (((2nd βπ)π(2nd βπ )) = 0 β (((2nd βπ)π(2nd βπ )) β€ 0 β§ 0 β€ ((2nd
βπ)π(2nd βπ ))))) |
74 | 24, 51, 73 | syl2anc 411 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β (((2nd βπ)π(2nd βπ )) = 0 β (((2nd βπ)π(2nd βπ )) β€ 0 β§ 0 β€ ((2nd
βπ)π(2nd βπ ))))) |
75 | 72, 74 | bitr4d 191 |
. . . 4
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β (((2nd βπ)π(2nd βπ )) β€ 0 β ((2nd
βπ)π(2nd βπ )) = 0)) |
76 | 69, 75 | anbi12d 473 |
. . 3
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β ((((1st βπ)π(1st βπ )) β€ 0 β§ ((2nd βπ)π(2nd βπ )) β€ 0) β (((1st
βπ)π(1st βπ )) = 0 β§ ((2nd βπ)π(2nd βπ )) = 0))) |
77 | | xmeteq0 13829 |
. . . . . 6
β’ ((π β (βMetβπ) β§ (1st
βπ) β π β§ (1st
βπ ) β π) β (((1st
βπ)π(1st βπ )) = 0 β (1st βπ) = (1st βπ ))) |
78 | 11, 13, 15, 77 | syl3anc 1238 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β (((1st βπ)π(1st βπ )) = 0 β (1st βπ) = (1st βπ ))) |
79 | | xmeteq0 13829 |
. . . . . 6
β’ ((π β (βMetβπ) β§ (2nd
βπ) β π β§ (2nd
βπ ) β π) β (((2nd
βπ)π(2nd βπ )) = 0 β (2nd βπ) = (2nd βπ ))) |
80 | 18, 20, 22, 79 | syl3anc 1238 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β (((2nd βπ)π(2nd βπ )) = 0 β (2nd βπ) = (2nd βπ ))) |
81 | 78, 80 | anbi12d 473 |
. . . 4
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β ((((1st βπ)π(1st βπ )) = 0 β§ ((2nd βπ)π(2nd βπ )) = 0) β ((1st βπ) = (1st βπ ) β§ (2nd
βπ) = (2nd
βπ )))) |
82 | | xpopth 6176 |
. . . . 5
β’ ((π β (π Γ π) β§ π β (π Γ π)) β (((1st βπ) = (1st βπ ) β§ (2nd
βπ) = (2nd
βπ )) β π = π )) |
83 | 82 | adantl 277 |
. . . 4
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β (((1st βπ) = (1st βπ ) β§ (2nd
βπ) = (2nd
βπ )) β π = π )) |
84 | 81, 83 | bitrd 188 |
. . 3
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β ((((1st βπ)π(1st βπ )) = 0 β§ ((2nd βπ)π(2nd βπ )) = 0) β π = π )) |
85 | 65, 76, 84 | 3bitrd 214 |
. 2
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π))) β ((πππ ) = 0 β π = π )) |
86 | 48 | 3adantr3 1158 |
. . 3
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (πππ ) = sup({((1st βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, <
)) |
87 | 17 | 3adantr3 1158 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((1st βπ)π(1st βπ )) β
β*) |
88 | 1 | adantr 276 |
. . . . . . 7
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β π β (βMetβπ)) |
89 | | simpr3 1005 |
. . . . . . . 8
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β π‘ β (π Γ π)) |
90 | | xp1st 6165 |
. . . . . . . 8
β’ (π‘ β (π Γ π) β (1st βπ‘) β π) |
91 | 89, 90 | syl 14 |
. . . . . . 7
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (1st βπ‘) β π) |
92 | | simpr1 1003 |
. . . . . . . 8
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β π β (π Γ π)) |
93 | 92, 12 | syl 14 |
. . . . . . 7
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (1st βπ) β π) |
94 | | xmetcl 13822 |
. . . . . . 7
β’ ((π β (βMetβπ) β§ (1st
βπ‘) β π β§ (1st
βπ) β π) β ((1st
βπ‘)π(1st βπ)) β
β*) |
95 | 88, 91, 93, 94 | syl3anc 1238 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((1st βπ‘)π(1st βπ)) β
β*) |
96 | 15 | 3adantr3 1158 |
. . . . . . 7
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (1st βπ ) β π) |
97 | | xmetcl 13822 |
. . . . . . 7
β’ ((π β (βMetβπ) β§ (1st
βπ‘) β π β§ (1st
βπ ) β π) β ((1st
βπ‘)π(1st βπ )) β
β*) |
98 | 88, 91, 96, 97 | syl3anc 1238 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((1st βπ‘)π(1st βπ )) β
β*) |
99 | 95, 98 | xaddcld 9883 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (((1st βπ‘)π(1st βπ)) +π ((1st
βπ‘)π(1st βπ ))) β
β*) |
100 | 5 | adantr 276 |
. . . . . . . . . 10
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β π β (βMetβπ)) |
101 | | xp2nd 6166 |
. . . . . . . . . . 11
β’ (π‘ β (π Γ π) β (2nd βπ‘) β π) |
102 | 89, 101 | syl 14 |
. . . . . . . . . 10
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (2nd βπ‘) β π) |
103 | 92, 19 | syl 14 |
. . . . . . . . . 10
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (2nd βπ) β π) |
104 | | xmetcl 13822 |
. . . . . . . . . 10
β’ ((π β (βMetβπ) β§ (2nd
βπ‘) β π β§ (2nd
βπ) β π) β ((2nd
βπ‘)π(2nd βπ)) β
β*) |
105 | 100, 102,
103, 104 | syl3anc 1238 |
. . . . . . . . 9
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((2nd βπ‘)π(2nd βπ)) β
β*) |
106 | | xrmaxcl 11259 |
. . . . . . . . 9
β’
((((1st βπ‘)π(1st βπ)) β β* β§
((2nd βπ‘)π(2nd βπ)) β β*) β
sup({((1st βπ‘)π(1st βπ)), ((2nd βπ‘)π(2nd βπ))}, β*, < ) β
β*) |
107 | 95, 105, 106 | syl2anc 411 |
. . . . . . . 8
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β sup({((1st
βπ‘)π(1st βπ)), ((2nd βπ‘)π(2nd βπ))}, β*, < ) β
β*) |
108 | | fveq2 5515 |
. . . . . . . . . . . 12
β’ (π’ = π‘ β (1st βπ’) = (1st βπ‘)) |
109 | | fveq2 5515 |
. . . . . . . . . . . 12
β’ (π£ = π β (1st βπ£) = (1st βπ)) |
110 | 108, 109 | oveqan12d 5893 |
. . . . . . . . . . 11
β’ ((π’ = π‘ β§ π£ = π) β ((1st βπ’)π(1st βπ£)) = ((1st βπ‘)π(1st βπ))) |
111 | | fveq2 5515 |
. . . . . . . . . . . 12
β’ (π’ = π‘ β (2nd βπ’) = (2nd βπ‘)) |
112 | | fveq2 5515 |
. . . . . . . . . . . 12
β’ (π£ = π β (2nd βπ£) = (2nd βπ)) |
113 | 111, 112 | oveqan12d 5893 |
. . . . . . . . . . 11
β’ ((π’ = π‘ β§ π£ = π) β ((2nd βπ’)π(2nd βπ£)) = ((2nd βπ‘)π(2nd βπ))) |
114 | 110, 113 | preq12d 3677 |
. . . . . . . . . 10
β’ ((π’ = π‘ β§ π£ = π) β {((1st βπ’)π(1st βπ£)), ((2nd βπ’)π(2nd βπ£))} = {((1st βπ‘)π(1st βπ)), ((2nd βπ‘)π(2nd βπ))}) |
115 | 114 | supeq1d 6985 |
. . . . . . . . 9
β’ ((π’ = π‘ β§ π£ = π) β sup({((1st βπ’)π(1st βπ£)), ((2nd βπ’)π(2nd βπ£))}, β*, < ) =
sup({((1st βπ‘)π(1st βπ)), ((2nd βπ‘)π(2nd βπ))}, β*, <
)) |
116 | 115, 28 | ovmpoga 6003 |
. . . . . . . 8
β’ ((π‘ β (π Γ π) β§ π β (π Γ π) β§ sup({((1st βπ‘)π(1st βπ)), ((2nd βπ‘)π(2nd βπ))}, β*, < ) β
β*) β (π‘ππ) = sup({((1st βπ‘)π(1st βπ)), ((2nd βπ‘)π(2nd βπ))}, β*, <
)) |
117 | 89, 92, 107, 116 | syl3anc 1238 |
. . . . . . 7
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (π‘ππ) = sup({((1st βπ‘)π(1st βπ)), ((2nd βπ‘)π(2nd βπ))}, β*, <
)) |
118 | 117, 107 | eqeltrd 2254 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (π‘ππ) β
β*) |
119 | | simpr2 1004 |
. . . . . . . 8
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β π β (π Γ π)) |
120 | 22 | 3adantr3 1158 |
. . . . . . . . . 10
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (2nd βπ ) β π) |
121 | | xmetcl 13822 |
. . . . . . . . . 10
β’ ((π β (βMetβπ) β§ (2nd
βπ‘) β π β§ (2nd
βπ ) β π) β ((2nd
βπ‘)π(2nd βπ )) β
β*) |
122 | 100, 102,
120, 121 | syl3anc 1238 |
. . . . . . . . 9
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((2nd βπ‘)π(2nd βπ )) β
β*) |
123 | | xrmaxcl 11259 |
. . . . . . . . 9
β’
((((1st βπ‘)π(1st βπ )) β β* β§
((2nd βπ‘)π(2nd βπ )) β β*) β
sup({((1st βπ‘)π(1st βπ )), ((2nd βπ‘)π(2nd βπ ))}, β*, < ) β
β*) |
124 | 98, 122, 123 | syl2anc 411 |
. . . . . . . 8
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β sup({((1st
βπ‘)π(1st βπ )), ((2nd βπ‘)π(2nd βπ ))}, β*, < ) β
β*) |
125 | 108, 35 | oveqan12d 5893 |
. . . . . . . . . . 11
β’ ((π’ = π‘ β§ π£ = π ) β ((1st βπ’)π(1st βπ£)) = ((1st βπ‘)π(1st βπ ))) |
126 | 111, 37 | oveqan12d 5893 |
. . . . . . . . . . 11
β’ ((π’ = π‘ β§ π£ = π ) β ((2nd βπ’)π(2nd βπ£)) = ((2nd βπ‘)π(2nd βπ ))) |
127 | 125, 126 | preq12d 3677 |
. . . . . . . . . 10
β’ ((π’ = π‘ β§ π£ = π ) β {((1st βπ’)π(1st βπ£)), ((2nd βπ’)π(2nd βπ£))} = {((1st βπ‘)π(1st βπ )), ((2nd βπ‘)π(2nd βπ ))}) |
128 | 127 | supeq1d 6985 |
. . . . . . . . 9
β’ ((π’ = π‘ β§ π£ = π ) β sup({((1st βπ’)π(1st βπ£)), ((2nd βπ’)π(2nd βπ£))}, β*, < ) =
sup({((1st βπ‘)π(1st βπ )), ((2nd βπ‘)π(2nd βπ ))}, β*, <
)) |
129 | 128, 28 | ovmpoga 6003 |
. . . . . . . 8
β’ ((π‘ β (π Γ π) β§ π β (π Γ π) β§ sup({((1st βπ‘)π(1st βπ )), ((2nd βπ‘)π(2nd βπ ))}, β*, < ) β
β*) β (π‘ππ ) = sup({((1st βπ‘)π(1st βπ )), ((2nd βπ‘)π(2nd βπ ))}, β*, <
)) |
130 | 89, 119, 124, 129 | syl3anc 1238 |
. . . . . . 7
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (π‘ππ ) = sup({((1st βπ‘)π(1st βπ )), ((2nd βπ‘)π(2nd βπ ))}, β*, <
)) |
131 | 130, 124 | eqeltrd 2254 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (π‘ππ ) β
β*) |
132 | 118, 131 | xaddcld 9883 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((π‘ππ) +π (π‘ππ )) β
β*) |
133 | | xmettri2 13831 |
. . . . . 6
β’ ((π β (βMetβπ) β§ ((1st
βπ‘) β π β§ (1st
βπ) β π β§ (1st
βπ ) β π)) β ((1st
βπ)π(1st βπ )) β€ (((1st βπ‘)π(1st βπ)) +π ((1st
βπ‘)π(1st βπ )))) |
134 | 88, 91, 93, 96, 133 | syl13anc 1240 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((1st βπ)π(1st βπ )) β€ (((1st βπ‘)π(1st βπ)) +π ((1st
βπ‘)π(1st βπ )))) |
135 | | xrmax1sup 11260 |
. . . . . . . 8
β’
((((1st βπ‘)π(1st βπ)) β β* β§
((2nd βπ‘)π(2nd βπ)) β β*) β
((1st βπ‘)π(1st βπ)) β€ sup({((1st βπ‘)π(1st βπ)), ((2nd βπ‘)π(2nd βπ))}, β*, <
)) |
136 | 95, 105, 135 | syl2anc 411 |
. . . . . . 7
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((1st βπ‘)π(1st βπ)) β€ sup({((1st βπ‘)π(1st βπ)), ((2nd βπ‘)π(2nd βπ))}, β*, <
)) |
137 | 136, 117 | breqtrrd 4031 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((1st βπ‘)π(1st βπ)) β€ (π‘ππ)) |
138 | | xrmax1sup 11260 |
. . . . . . . 8
β’
((((1st βπ‘)π(1st βπ )) β β* β§
((2nd βπ‘)π(2nd βπ )) β β*) β
((1st βπ‘)π(1st βπ )) β€ sup({((1st βπ‘)π(1st βπ )), ((2nd βπ‘)π(2nd βπ ))}, β*, <
)) |
139 | 98, 122, 138 | syl2anc 411 |
. . . . . . 7
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((1st βπ‘)π(1st βπ )) β€ sup({((1st βπ‘)π(1st βπ )), ((2nd βπ‘)π(2nd βπ ))}, β*, <
)) |
140 | 139, 130 | breqtrrd 4031 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((1st βπ‘)π(1st βπ )) β€ (π‘ππ )) |
141 | | xle2add 9878 |
. . . . . . 7
β’
(((((1st βπ‘)π(1st βπ)) β β* β§
((1st βπ‘)π(1st βπ )) β β*) β§ ((π‘ππ) β β* β§ (π‘ππ ) β β*)) β
((((1st βπ‘)π(1st βπ)) β€ (π‘ππ) β§ ((1st βπ‘)π(1st βπ )) β€ (π‘ππ )) β (((1st βπ‘)π(1st βπ)) +π ((1st
βπ‘)π(1st βπ ))) β€ ((π‘ππ) +π (π‘ππ )))) |
142 | 95, 98, 118, 131, 141 | syl22anc 1239 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((((1st βπ‘)π(1st βπ)) β€ (π‘ππ) β§ ((1st βπ‘)π(1st βπ )) β€ (π‘ππ )) β (((1st βπ‘)π(1st βπ)) +π ((1st
βπ‘)π(1st βπ ))) β€ ((π‘ππ) +π (π‘ππ )))) |
143 | 137, 140,
142 | mp2and 433 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (((1st βπ‘)π(1st βπ)) +π ((1st
βπ‘)π(1st βπ ))) β€ ((π‘ππ) +π (π‘ππ ))) |
144 | 87, 99, 132, 134, 143 | xrletrd 9811 |
. . . 4
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((1st βπ)π(1st βπ )) β€ ((π‘ππ) +π (π‘ππ ))) |
145 | 24 | 3adantr3 1158 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((2nd βπ)π(2nd βπ )) β
β*) |
146 | 105, 122 | xaddcld 9883 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (((2nd βπ‘)π(2nd βπ)) +π ((2nd
βπ‘)π(2nd βπ ))) β
β*) |
147 | | xmettri2 13831 |
. . . . . 6
β’ ((π β (βMetβπ) β§ ((2nd
βπ‘) β π β§ (2nd
βπ) β π β§ (2nd
βπ ) β π)) β ((2nd
βπ)π(2nd βπ )) β€ (((2nd βπ‘)π(2nd βπ)) +π ((2nd
βπ‘)π(2nd βπ )))) |
148 | 100, 102,
103, 120, 147 | syl13anc 1240 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((2nd βπ)π(2nd βπ )) β€ (((2nd βπ‘)π(2nd βπ)) +π ((2nd
βπ‘)π(2nd βπ )))) |
149 | | xrmax2sup 11261 |
. . . . . . . 8
β’
((((1st βπ‘)π(1st βπ)) β β* β§
((2nd βπ‘)π(2nd βπ)) β β*) β
((2nd βπ‘)π(2nd βπ)) β€ sup({((1st βπ‘)π(1st βπ)), ((2nd βπ‘)π(2nd βπ))}, β*, <
)) |
150 | 95, 105, 149 | syl2anc 411 |
. . . . . . 7
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((2nd βπ‘)π(2nd βπ)) β€ sup({((1st βπ‘)π(1st βπ)), ((2nd βπ‘)π(2nd βπ))}, β*, <
)) |
151 | 150, 117 | breqtrrd 4031 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((2nd βπ‘)π(2nd βπ)) β€ (π‘ππ)) |
152 | | xrmax2sup 11261 |
. . . . . . . 8
β’
((((1st βπ‘)π(1st βπ )) β β* β§
((2nd βπ‘)π(2nd βπ )) β β*) β
((2nd βπ‘)π(2nd βπ )) β€ sup({((1st βπ‘)π(1st βπ )), ((2nd βπ‘)π(2nd βπ ))}, β*, <
)) |
153 | 98, 122, 152 | syl2anc 411 |
. . . . . . 7
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((2nd βπ‘)π(2nd βπ )) β€ sup({((1st βπ‘)π(1st βπ )), ((2nd βπ‘)π(2nd βπ ))}, β*, <
)) |
154 | 153, 130 | breqtrrd 4031 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((2nd βπ‘)π(2nd βπ )) β€ (π‘ππ )) |
155 | | xle2add 9878 |
. . . . . . 7
β’
(((((2nd βπ‘)π(2nd βπ)) β β* β§
((2nd βπ‘)π(2nd βπ )) β β*) β§ ((π‘ππ) β β* β§ (π‘ππ ) β β*)) β
((((2nd βπ‘)π(2nd βπ)) β€ (π‘ππ) β§ ((2nd βπ‘)π(2nd βπ )) β€ (π‘ππ )) β (((2nd βπ‘)π(2nd βπ)) +π ((2nd
βπ‘)π(2nd βπ ))) β€ ((π‘ππ) +π (π‘ππ )))) |
156 | 105, 122,
118, 131, 155 | syl22anc 1239 |
. . . . . 6
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((((2nd βπ‘)π(2nd βπ)) β€ (π‘ππ) β§ ((2nd βπ‘)π(2nd βπ )) β€ (π‘ππ )) β (((2nd βπ‘)π(2nd βπ)) +π ((2nd
βπ‘)π(2nd βπ ))) β€ ((π‘ππ) +π (π‘ππ )))) |
157 | 151, 154,
156 | mp2and 433 |
. . . . 5
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (((2nd βπ‘)π(2nd βπ)) +π ((2nd
βπ‘)π(2nd βπ ))) β€ ((π‘ππ) +π (π‘ππ ))) |
158 | 145, 146,
132, 148, 157 | xrletrd 9811 |
. . . 4
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β ((2nd βπ)π(2nd βπ )) β€ ((π‘ππ) +π (π‘ππ ))) |
159 | | xrmaxlesup 11266 |
. . . . 5
β’
((((1st βπ)π(1st βπ )) β β* β§
((2nd βπ)π(2nd βπ )) β β* β§ ((π‘ππ) +π (π‘ππ )) β β*) β
(sup({((1st βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, < ) β€ ((π‘ππ) +π (π‘ππ )) β (((1st βπ)π(1st βπ )) β€ ((π‘ππ) +π (π‘ππ )) β§ ((2nd βπ)π(2nd βπ )) β€ ((π‘ππ) +π (π‘ππ ))))) |
160 | 87, 145, 132, 159 | syl3anc 1238 |
. . . 4
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (sup({((1st
βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, < ) β€ ((π‘ππ) +π (π‘ππ )) β (((1st βπ)π(1st βπ )) β€ ((π‘ππ) +π (π‘ππ )) β§ ((2nd βπ)π(2nd βπ )) β€ ((π‘ππ) +π (π‘ππ ))))) |
161 | 144, 158,
160 | mpbir2and 944 |
. . 3
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β sup({((1st
βπ)π(1st βπ )), ((2nd βπ)π(2nd βπ ))}, β*, < ) β€ ((π‘ππ) +π (π‘ππ ))) |
162 | 86, 161 | eqbrtrd 4025 |
. 2
β’ ((π β§ (π β (π Γ π) β§ π β (π Γ π) β§ π‘ β (π Γ π))) β (πππ ) β€ ((π‘ππ) +π (π‘ππ ))) |
163 | 10, 44, 85, 162 | isxmetd 13817 |
1
β’ (π β π β (βMetβ(π Γ π))) |