Step | Hyp | Ref
| Expression |
1 | | xmetxp.1 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) |
2 | | eqid 2157 |
. . . . 5
⊢
(MetOpen‘𝑀) =
(MetOpen‘𝑀) |
3 | 2 | mopnm 12918 |
. . . 4
⊢ (𝑀 ∈ (∞Met‘𝑋) → 𝑋 ∈ (MetOpen‘𝑀)) |
4 | 1, 3 | syl 14 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (MetOpen‘𝑀)) |
5 | | xmetxp.2 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) |
6 | | eqid 2157 |
. . . . 5
⊢
(MetOpen‘𝑁) =
(MetOpen‘𝑁) |
7 | 6 | mopnm 12918 |
. . . 4
⊢ (𝑁 ∈ (∞Met‘𝑌) → 𝑌 ∈ (MetOpen‘𝑁)) |
8 | 5, 7 | syl 14 |
. . 3
⊢ (𝜑 → 𝑌 ∈ (MetOpen‘𝑁)) |
9 | | xpexg 4702 |
. . 3
⊢ ((𝑋 ∈ (MetOpen‘𝑀) ∧ 𝑌 ∈ (MetOpen‘𝑁)) → (𝑋 × 𝑌) ∈ V) |
10 | 4, 8, 9 | syl2anc 409 |
. 2
⊢ (𝜑 → (𝑋 × 𝑌) ∈ V) |
11 | 1 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → 𝑀 ∈ (∞Met‘𝑋)) |
12 | | xp1st 6115 |
. . . . . . 7
⊢ (𝑟 ∈ (𝑋 × 𝑌) → (1st ‘𝑟) ∈ 𝑋) |
13 | 12 | ad2antrl 482 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → (1st ‘𝑟) ∈ 𝑋) |
14 | | xp1st 6115 |
. . . . . . 7
⊢ (𝑠 ∈ (𝑋 × 𝑌) → (1st ‘𝑠) ∈ 𝑋) |
15 | 14 | ad2antll 483 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → (1st ‘𝑠) ∈ 𝑋) |
16 | | xmetcl 12822 |
. . . . . 6
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ (1st
‘𝑟) ∈ 𝑋 ∧ (1st
‘𝑠) ∈ 𝑋) → ((1st
‘𝑟)𝑀(1st ‘𝑠)) ∈
ℝ*) |
17 | 11, 13, 15, 16 | syl3anc 1220 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → ((1st ‘𝑟)𝑀(1st ‘𝑠)) ∈
ℝ*) |
18 | 5 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → 𝑁 ∈ (∞Met‘𝑌)) |
19 | | xp2nd 6116 |
. . . . . . 7
⊢ (𝑟 ∈ (𝑋 × 𝑌) → (2nd ‘𝑟) ∈ 𝑌) |
20 | 19 | ad2antrl 482 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → (2nd ‘𝑟) ∈ 𝑌) |
21 | | xp2nd 6116 |
. . . . . . 7
⊢ (𝑠 ∈ (𝑋 × 𝑌) → (2nd ‘𝑠) ∈ 𝑌) |
22 | 21 | ad2antll 483 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → (2nd ‘𝑠) ∈ 𝑌) |
23 | | xmetcl 12822 |
. . . . . 6
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ (2nd
‘𝑟) ∈ 𝑌 ∧ (2nd
‘𝑠) ∈ 𝑌) → ((2nd
‘𝑟)𝑁(2nd ‘𝑠)) ∈
ℝ*) |
24 | 18, 20, 22, 23 | syl3anc 1220 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → ((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ∈
ℝ*) |
25 | | xrmaxcl 11160 |
. . . . 5
⊢
((((1st ‘𝑟)𝑀(1st ‘𝑠)) ∈ ℝ* ∧
((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ∈ ℝ*) →
sup({((1st ‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, < ) ∈
ℝ*) |
26 | 17, 24, 25 | syl2anc 409 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → sup({((1st
‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, < ) ∈
ℝ*) |
27 | 26 | ralrimivva 2539 |
. . 3
⊢ (𝜑 → ∀𝑟 ∈ (𝑋 × 𝑌)∀𝑠 ∈ (𝑋 × 𝑌)sup({((1st ‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, < ) ∈
ℝ*) |
28 | | xmetxp.p |
. . . . 5
⊢ 𝑃 = (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ sup({((1st ‘𝑢)𝑀(1st ‘𝑣)), ((2nd ‘𝑢)𝑁(2nd ‘𝑣))}, ℝ*, <
)) |
29 | | fveq2 5470 |
. . . . . . . . 9
⊢ (𝑢 = 𝑟 → (1st ‘𝑢) = (1st ‘𝑟)) |
30 | 29 | oveq1d 5841 |
. . . . . . . 8
⊢ (𝑢 = 𝑟 → ((1st ‘𝑢)𝑀(1st ‘𝑣)) = ((1st ‘𝑟)𝑀(1st ‘𝑣))) |
31 | | fveq2 5470 |
. . . . . . . . 9
⊢ (𝑢 = 𝑟 → (2nd ‘𝑢) = (2nd ‘𝑟)) |
32 | 31 | oveq1d 5841 |
. . . . . . . 8
⊢ (𝑢 = 𝑟 → ((2nd ‘𝑢)𝑁(2nd ‘𝑣)) = ((2nd ‘𝑟)𝑁(2nd ‘𝑣))) |
33 | 30, 32 | preq12d 3646 |
. . . . . . 7
⊢ (𝑢 = 𝑟 → {((1st ‘𝑢)𝑀(1st ‘𝑣)), ((2nd ‘𝑢)𝑁(2nd ‘𝑣))} = {((1st ‘𝑟)𝑀(1st ‘𝑣)), ((2nd ‘𝑟)𝑁(2nd ‘𝑣))}) |
34 | 33 | supeq1d 6933 |
. . . . . 6
⊢ (𝑢 = 𝑟 → sup({((1st ‘𝑢)𝑀(1st ‘𝑣)), ((2nd ‘𝑢)𝑁(2nd ‘𝑣))}, ℝ*, < ) =
sup({((1st ‘𝑟)𝑀(1st ‘𝑣)), ((2nd ‘𝑟)𝑁(2nd ‘𝑣))}, ℝ*, <
)) |
35 | | fveq2 5470 |
. . . . . . . . 9
⊢ (𝑣 = 𝑠 → (1st ‘𝑣) = (1st ‘𝑠)) |
36 | 35 | oveq2d 5842 |
. . . . . . . 8
⊢ (𝑣 = 𝑠 → ((1st ‘𝑟)𝑀(1st ‘𝑣)) = ((1st ‘𝑟)𝑀(1st ‘𝑠))) |
37 | | fveq2 5470 |
. . . . . . . . 9
⊢ (𝑣 = 𝑠 → (2nd ‘𝑣) = (2nd ‘𝑠)) |
38 | 37 | oveq2d 5842 |
. . . . . . . 8
⊢ (𝑣 = 𝑠 → ((2nd ‘𝑟)𝑁(2nd ‘𝑣)) = ((2nd ‘𝑟)𝑁(2nd ‘𝑠))) |
39 | 36, 38 | preq12d 3646 |
. . . . . . 7
⊢ (𝑣 = 𝑠 → {((1st ‘𝑟)𝑀(1st ‘𝑣)), ((2nd ‘𝑟)𝑁(2nd ‘𝑣))} = {((1st ‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}) |
40 | 39 | supeq1d 6933 |
. . . . . 6
⊢ (𝑣 = 𝑠 → sup({((1st ‘𝑟)𝑀(1st ‘𝑣)), ((2nd ‘𝑟)𝑁(2nd ‘𝑣))}, ℝ*, < ) =
sup({((1st ‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, <
)) |
41 | 34, 40 | cbvmpov 5903 |
. . . . 5
⊢ (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ sup({((1st ‘𝑢)𝑀(1st ‘𝑣)), ((2nd ‘𝑢)𝑁(2nd ‘𝑣))}, ℝ*, < )) = (𝑟 ∈ (𝑋 × 𝑌), 𝑠 ∈ (𝑋 × 𝑌) ↦ sup({((1st ‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, <
)) |
42 | 28, 41 | eqtri 2178 |
. . . 4
⊢ 𝑃 = (𝑟 ∈ (𝑋 × 𝑌), 𝑠 ∈ (𝑋 × 𝑌) ↦ sup({((1st ‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, <
)) |
43 | 42 | fmpo 6151 |
. . 3
⊢
(∀𝑟 ∈
(𝑋 × 𝑌)∀𝑠 ∈ (𝑋 × 𝑌)sup({((1st ‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, < ) ∈
ℝ* ↔ 𝑃:((𝑋 × 𝑌) × (𝑋 × 𝑌))⟶ℝ*) |
44 | 27, 43 | sylib 121 |
. 2
⊢ (𝜑 → 𝑃:((𝑋 × 𝑌) × (𝑋 × 𝑌))⟶ℝ*) |
45 | | simprl 521 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → 𝑟 ∈ (𝑋 × 𝑌)) |
46 | | simprr 522 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → 𝑠 ∈ (𝑋 × 𝑌)) |
47 | 34, 40, 28 | ovmpog 5957 |
. . . . . . . 8
⊢ ((𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ sup({((1st ‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, < ) ∈
ℝ*) → (𝑟𝑃𝑠) = sup({((1st ‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, <
)) |
48 | 45, 46, 26, 47 | syl3anc 1220 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → (𝑟𝑃𝑠) = sup({((1st ‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, <
)) |
49 | 48, 26 | eqeltrd 2234 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → (𝑟𝑃𝑠) ∈
ℝ*) |
50 | | 0xr 7926 |
. . . . . . 7
⊢ 0 ∈
ℝ* |
51 | 50 | a1i 9 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → 0 ∈
ℝ*) |
52 | | xrletri3 9715 |
. . . . . 6
⊢ (((𝑟𝑃𝑠) ∈ ℝ* ∧ 0 ∈
ℝ*) → ((𝑟𝑃𝑠) = 0 ↔ ((𝑟𝑃𝑠) ≤ 0 ∧ 0 ≤ (𝑟𝑃𝑠)))) |
53 | 49, 51, 52 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → ((𝑟𝑃𝑠) = 0 ↔ ((𝑟𝑃𝑠) ≤ 0 ∧ 0 ≤ (𝑟𝑃𝑠)))) |
54 | | xmetge0 12835 |
. . . . . . . . 9
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ (1st
‘𝑟) ∈ 𝑋 ∧ (1st
‘𝑠) ∈ 𝑋) → 0 ≤ ((1st
‘𝑟)𝑀(1st ‘𝑠))) |
55 | 11, 13, 15, 54 | syl3anc 1220 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → 0 ≤ ((1st
‘𝑟)𝑀(1st ‘𝑠))) |
56 | | xrmax1sup 11161 |
. . . . . . . . 9
⊢
((((1st ‘𝑟)𝑀(1st ‘𝑠)) ∈ ℝ* ∧
((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ∈ ℝ*) →
((1st ‘𝑟)𝑀(1st ‘𝑠)) ≤ sup({((1st ‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, <
)) |
57 | 17, 24, 56 | syl2anc 409 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → ((1st ‘𝑟)𝑀(1st ‘𝑠)) ≤ sup({((1st ‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, <
)) |
58 | 51, 17, 26, 55, 57 | xrletrd 9722 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → 0 ≤ sup({((1st
‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, <
)) |
59 | 58, 48 | breqtrrd 3994 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → 0 ≤ (𝑟𝑃𝑠)) |
60 | 59 | biantrud 302 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → ((𝑟𝑃𝑠) ≤ 0 ↔ ((𝑟𝑃𝑠) ≤ 0 ∧ 0 ≤ (𝑟𝑃𝑠)))) |
61 | 53, 60 | bitr4d 190 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → ((𝑟𝑃𝑠) = 0 ↔ (𝑟𝑃𝑠) ≤ 0)) |
62 | 48 | breq1d 3977 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → ((𝑟𝑃𝑠) ≤ 0 ↔ sup({((1st
‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, < ) ≤
0)) |
63 | | xrmaxlesup 11167 |
. . . . 5
⊢
((((1st ‘𝑟)𝑀(1st ‘𝑠)) ∈ ℝ* ∧
((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ∈ ℝ* ∧ 0 ∈
ℝ*) → (sup({((1st ‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, < ) ≤ 0
↔ (((1st ‘𝑟)𝑀(1st ‘𝑠)) ≤ 0 ∧ ((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ≤ 0))) |
64 | 17, 24, 51, 63 | syl3anc 1220 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → (sup({((1st
‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, < ) ≤ 0
↔ (((1st ‘𝑟)𝑀(1st ‘𝑠)) ≤ 0 ∧ ((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ≤ 0))) |
65 | 61, 62, 64 | 3bitrd 213 |
. . 3
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → ((𝑟𝑃𝑠) = 0 ↔ (((1st ‘𝑟)𝑀(1st ‘𝑠)) ≤ 0 ∧ ((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ≤ 0))) |
66 | 55 | biantrud 302 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → (((1st ‘𝑟)𝑀(1st ‘𝑠)) ≤ 0 ↔ (((1st
‘𝑟)𝑀(1st ‘𝑠)) ≤ 0 ∧ 0 ≤ ((1st
‘𝑟)𝑀(1st ‘𝑠))))) |
67 | | xrletri3 9715 |
. . . . . 6
⊢
((((1st ‘𝑟)𝑀(1st ‘𝑠)) ∈ ℝ* ∧ 0 ∈
ℝ*) → (((1st ‘𝑟)𝑀(1st ‘𝑠)) = 0 ↔ (((1st ‘𝑟)𝑀(1st ‘𝑠)) ≤ 0 ∧ 0 ≤ ((1st
‘𝑟)𝑀(1st ‘𝑠))))) |
68 | 17, 51, 67 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → (((1st ‘𝑟)𝑀(1st ‘𝑠)) = 0 ↔ (((1st ‘𝑟)𝑀(1st ‘𝑠)) ≤ 0 ∧ 0 ≤ ((1st
‘𝑟)𝑀(1st ‘𝑠))))) |
69 | 66, 68 | bitr4d 190 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → (((1st ‘𝑟)𝑀(1st ‘𝑠)) ≤ 0 ↔ ((1st
‘𝑟)𝑀(1st ‘𝑠)) = 0)) |
70 | | xmetge0 12835 |
. . . . . . 7
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ (2nd
‘𝑟) ∈ 𝑌 ∧ (2nd
‘𝑠) ∈ 𝑌) → 0 ≤ ((2nd
‘𝑟)𝑁(2nd ‘𝑠))) |
71 | 18, 20, 22, 70 | syl3anc 1220 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → 0 ≤ ((2nd
‘𝑟)𝑁(2nd ‘𝑠))) |
72 | 71 | biantrud 302 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → (((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ≤ 0 ↔ (((2nd
‘𝑟)𝑁(2nd ‘𝑠)) ≤ 0 ∧ 0 ≤ ((2nd
‘𝑟)𝑁(2nd ‘𝑠))))) |
73 | | xrletri3 9715 |
. . . . . 6
⊢
((((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ∈ ℝ* ∧ 0 ∈
ℝ*) → (((2nd ‘𝑟)𝑁(2nd ‘𝑠)) = 0 ↔ (((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ≤ 0 ∧ 0 ≤ ((2nd
‘𝑟)𝑁(2nd ‘𝑠))))) |
74 | 24, 51, 73 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → (((2nd ‘𝑟)𝑁(2nd ‘𝑠)) = 0 ↔ (((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ≤ 0 ∧ 0 ≤ ((2nd
‘𝑟)𝑁(2nd ‘𝑠))))) |
75 | 72, 74 | bitr4d 190 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → (((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ≤ 0 ↔ ((2nd
‘𝑟)𝑁(2nd ‘𝑠)) = 0)) |
76 | 69, 75 | anbi12d 465 |
. . 3
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → ((((1st ‘𝑟)𝑀(1st ‘𝑠)) ≤ 0 ∧ ((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ≤ 0) ↔ (((1st
‘𝑟)𝑀(1st ‘𝑠)) = 0 ∧ ((2nd ‘𝑟)𝑁(2nd ‘𝑠)) = 0))) |
77 | | xmeteq0 12829 |
. . . . . 6
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ (1st
‘𝑟) ∈ 𝑋 ∧ (1st
‘𝑠) ∈ 𝑋) → (((1st
‘𝑟)𝑀(1st ‘𝑠)) = 0 ↔ (1st ‘𝑟) = (1st ‘𝑠))) |
78 | 11, 13, 15, 77 | syl3anc 1220 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → (((1st ‘𝑟)𝑀(1st ‘𝑠)) = 0 ↔ (1st ‘𝑟) = (1st ‘𝑠))) |
79 | | xmeteq0 12829 |
. . . . . 6
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ (2nd
‘𝑟) ∈ 𝑌 ∧ (2nd
‘𝑠) ∈ 𝑌) → (((2nd
‘𝑟)𝑁(2nd ‘𝑠)) = 0 ↔ (2nd ‘𝑟) = (2nd ‘𝑠))) |
80 | 18, 20, 22, 79 | syl3anc 1220 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → (((2nd ‘𝑟)𝑁(2nd ‘𝑠)) = 0 ↔ (2nd ‘𝑟) = (2nd ‘𝑠))) |
81 | 78, 80 | anbi12d 465 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → ((((1st ‘𝑟)𝑀(1st ‘𝑠)) = 0 ∧ ((2nd ‘𝑟)𝑁(2nd ‘𝑠)) = 0) ↔ ((1st ‘𝑟) = (1st ‘𝑠) ∧ (2nd
‘𝑟) = (2nd
‘𝑠)))) |
82 | | xpopth 6126 |
. . . . 5
⊢ ((𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌)) → (((1st ‘𝑟) = (1st ‘𝑠) ∧ (2nd
‘𝑟) = (2nd
‘𝑠)) ↔ 𝑟 = 𝑠)) |
83 | 82 | adantl 275 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → (((1st ‘𝑟) = (1st ‘𝑠) ∧ (2nd
‘𝑟) = (2nd
‘𝑠)) ↔ 𝑟 = 𝑠)) |
84 | 81, 83 | bitrd 187 |
. . 3
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → ((((1st ‘𝑟)𝑀(1st ‘𝑠)) = 0 ∧ ((2nd ‘𝑟)𝑁(2nd ‘𝑠)) = 0) ↔ 𝑟 = 𝑠)) |
85 | 65, 76, 84 | 3bitrd 213 |
. 2
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌))) → ((𝑟𝑃𝑠) = 0 ↔ 𝑟 = 𝑠)) |
86 | 48 | 3adantr3 1143 |
. . 3
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (𝑟𝑃𝑠) = sup({((1st ‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, <
)) |
87 | 17 | 3adantr3 1143 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((1st ‘𝑟)𝑀(1st ‘𝑠)) ∈
ℝ*) |
88 | 1 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → 𝑀 ∈ (∞Met‘𝑋)) |
89 | | simpr3 990 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → 𝑡 ∈ (𝑋 × 𝑌)) |
90 | | xp1st 6115 |
. . . . . . . 8
⊢ (𝑡 ∈ (𝑋 × 𝑌) → (1st ‘𝑡) ∈ 𝑋) |
91 | 89, 90 | syl 14 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (1st ‘𝑡) ∈ 𝑋) |
92 | | simpr1 988 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → 𝑟 ∈ (𝑋 × 𝑌)) |
93 | 92, 12 | syl 14 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (1st ‘𝑟) ∈ 𝑋) |
94 | | xmetcl 12822 |
. . . . . . 7
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ (1st
‘𝑡) ∈ 𝑋 ∧ (1st
‘𝑟) ∈ 𝑋) → ((1st
‘𝑡)𝑀(1st ‘𝑟)) ∈
ℝ*) |
95 | 88, 91, 93, 94 | syl3anc 1220 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((1st ‘𝑡)𝑀(1st ‘𝑟)) ∈
ℝ*) |
96 | 15 | 3adantr3 1143 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (1st ‘𝑠) ∈ 𝑋) |
97 | | xmetcl 12822 |
. . . . . . 7
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ (1st
‘𝑡) ∈ 𝑋 ∧ (1st
‘𝑠) ∈ 𝑋) → ((1st
‘𝑡)𝑀(1st ‘𝑠)) ∈
ℝ*) |
98 | 88, 91, 96, 97 | syl3anc 1220 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((1st ‘𝑡)𝑀(1st ‘𝑠)) ∈
ℝ*) |
99 | 95, 98 | xaddcld 9794 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (((1st ‘𝑡)𝑀(1st ‘𝑟)) +𝑒 ((1st
‘𝑡)𝑀(1st ‘𝑠))) ∈
ℝ*) |
100 | 5 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → 𝑁 ∈ (∞Met‘𝑌)) |
101 | | xp2nd 6116 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ (𝑋 × 𝑌) → (2nd ‘𝑡) ∈ 𝑌) |
102 | 89, 101 | syl 14 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (2nd ‘𝑡) ∈ 𝑌) |
103 | 92, 19 | syl 14 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (2nd ‘𝑟) ∈ 𝑌) |
104 | | xmetcl 12822 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ (2nd
‘𝑡) ∈ 𝑌 ∧ (2nd
‘𝑟) ∈ 𝑌) → ((2nd
‘𝑡)𝑁(2nd ‘𝑟)) ∈
ℝ*) |
105 | 100, 102,
103, 104 | syl3anc 1220 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((2nd ‘𝑡)𝑁(2nd ‘𝑟)) ∈
ℝ*) |
106 | | xrmaxcl 11160 |
. . . . . . . . 9
⊢
((((1st ‘𝑡)𝑀(1st ‘𝑟)) ∈ ℝ* ∧
((2nd ‘𝑡)𝑁(2nd ‘𝑟)) ∈ ℝ*) →
sup({((1st ‘𝑡)𝑀(1st ‘𝑟)), ((2nd ‘𝑡)𝑁(2nd ‘𝑟))}, ℝ*, < ) ∈
ℝ*) |
107 | 95, 105, 106 | syl2anc 409 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → sup({((1st
‘𝑡)𝑀(1st ‘𝑟)), ((2nd ‘𝑡)𝑁(2nd ‘𝑟))}, ℝ*, < ) ∈
ℝ*) |
108 | | fveq2 5470 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑡 → (1st ‘𝑢) = (1st ‘𝑡)) |
109 | | fveq2 5470 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑟 → (1st ‘𝑣) = (1st ‘𝑟)) |
110 | 108, 109 | oveqan12d 5845 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑡 ∧ 𝑣 = 𝑟) → ((1st ‘𝑢)𝑀(1st ‘𝑣)) = ((1st ‘𝑡)𝑀(1st ‘𝑟))) |
111 | | fveq2 5470 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑡 → (2nd ‘𝑢) = (2nd ‘𝑡)) |
112 | | fveq2 5470 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑟 → (2nd ‘𝑣) = (2nd ‘𝑟)) |
113 | 111, 112 | oveqan12d 5845 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑡 ∧ 𝑣 = 𝑟) → ((2nd ‘𝑢)𝑁(2nd ‘𝑣)) = ((2nd ‘𝑡)𝑁(2nd ‘𝑟))) |
114 | 110, 113 | preq12d 3646 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑡 ∧ 𝑣 = 𝑟) → {((1st ‘𝑢)𝑀(1st ‘𝑣)), ((2nd ‘𝑢)𝑁(2nd ‘𝑣))} = {((1st ‘𝑡)𝑀(1st ‘𝑟)), ((2nd ‘𝑡)𝑁(2nd ‘𝑟))}) |
115 | 114 | supeq1d 6933 |
. . . . . . . . 9
⊢ ((𝑢 = 𝑡 ∧ 𝑣 = 𝑟) → sup({((1st ‘𝑢)𝑀(1st ‘𝑣)), ((2nd ‘𝑢)𝑁(2nd ‘𝑣))}, ℝ*, < ) =
sup({((1st ‘𝑡)𝑀(1st ‘𝑟)), ((2nd ‘𝑡)𝑁(2nd ‘𝑟))}, ℝ*, <
)) |
116 | 115, 28 | ovmpoga 5952 |
. . . . . . . 8
⊢ ((𝑡 ∈ (𝑋 × 𝑌) ∧ 𝑟 ∈ (𝑋 × 𝑌) ∧ sup({((1st ‘𝑡)𝑀(1st ‘𝑟)), ((2nd ‘𝑡)𝑁(2nd ‘𝑟))}, ℝ*, < ) ∈
ℝ*) → (𝑡𝑃𝑟) = sup({((1st ‘𝑡)𝑀(1st ‘𝑟)), ((2nd ‘𝑡)𝑁(2nd ‘𝑟))}, ℝ*, <
)) |
117 | 89, 92, 107, 116 | syl3anc 1220 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (𝑡𝑃𝑟) = sup({((1st ‘𝑡)𝑀(1st ‘𝑟)), ((2nd ‘𝑡)𝑁(2nd ‘𝑟))}, ℝ*, <
)) |
118 | 117, 107 | eqeltrd 2234 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (𝑡𝑃𝑟) ∈
ℝ*) |
119 | | simpr2 989 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → 𝑠 ∈ (𝑋 × 𝑌)) |
120 | 22 | 3adantr3 1143 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (2nd ‘𝑠) ∈ 𝑌) |
121 | | xmetcl 12822 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ (2nd
‘𝑡) ∈ 𝑌 ∧ (2nd
‘𝑠) ∈ 𝑌) → ((2nd
‘𝑡)𝑁(2nd ‘𝑠)) ∈
ℝ*) |
122 | 100, 102,
120, 121 | syl3anc 1220 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((2nd ‘𝑡)𝑁(2nd ‘𝑠)) ∈
ℝ*) |
123 | | xrmaxcl 11160 |
. . . . . . . . 9
⊢
((((1st ‘𝑡)𝑀(1st ‘𝑠)) ∈ ℝ* ∧
((2nd ‘𝑡)𝑁(2nd ‘𝑠)) ∈ ℝ*) →
sup({((1st ‘𝑡)𝑀(1st ‘𝑠)), ((2nd ‘𝑡)𝑁(2nd ‘𝑠))}, ℝ*, < ) ∈
ℝ*) |
124 | 98, 122, 123 | syl2anc 409 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → sup({((1st
‘𝑡)𝑀(1st ‘𝑠)), ((2nd ‘𝑡)𝑁(2nd ‘𝑠))}, ℝ*, < ) ∈
ℝ*) |
125 | 108, 35 | oveqan12d 5845 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑡 ∧ 𝑣 = 𝑠) → ((1st ‘𝑢)𝑀(1st ‘𝑣)) = ((1st ‘𝑡)𝑀(1st ‘𝑠))) |
126 | 111, 37 | oveqan12d 5845 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑡 ∧ 𝑣 = 𝑠) → ((2nd ‘𝑢)𝑁(2nd ‘𝑣)) = ((2nd ‘𝑡)𝑁(2nd ‘𝑠))) |
127 | 125, 126 | preq12d 3646 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑡 ∧ 𝑣 = 𝑠) → {((1st ‘𝑢)𝑀(1st ‘𝑣)), ((2nd ‘𝑢)𝑁(2nd ‘𝑣))} = {((1st ‘𝑡)𝑀(1st ‘𝑠)), ((2nd ‘𝑡)𝑁(2nd ‘𝑠))}) |
128 | 127 | supeq1d 6933 |
. . . . . . . . 9
⊢ ((𝑢 = 𝑡 ∧ 𝑣 = 𝑠) → sup({((1st ‘𝑢)𝑀(1st ‘𝑣)), ((2nd ‘𝑢)𝑁(2nd ‘𝑣))}, ℝ*, < ) =
sup({((1st ‘𝑡)𝑀(1st ‘𝑠)), ((2nd ‘𝑡)𝑁(2nd ‘𝑠))}, ℝ*, <
)) |
129 | 128, 28 | ovmpoga 5952 |
. . . . . . . 8
⊢ ((𝑡 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ sup({((1st ‘𝑡)𝑀(1st ‘𝑠)), ((2nd ‘𝑡)𝑁(2nd ‘𝑠))}, ℝ*, < ) ∈
ℝ*) → (𝑡𝑃𝑠) = sup({((1st ‘𝑡)𝑀(1st ‘𝑠)), ((2nd ‘𝑡)𝑁(2nd ‘𝑠))}, ℝ*, <
)) |
130 | 89, 119, 124, 129 | syl3anc 1220 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (𝑡𝑃𝑠) = sup({((1st ‘𝑡)𝑀(1st ‘𝑠)), ((2nd ‘𝑡)𝑁(2nd ‘𝑠))}, ℝ*, <
)) |
131 | 130, 124 | eqeltrd 2234 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (𝑡𝑃𝑠) ∈
ℝ*) |
132 | 118, 131 | xaddcld 9794 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠)) ∈
ℝ*) |
133 | | xmettri2 12831 |
. . . . . 6
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ ((1st
‘𝑡) ∈ 𝑋 ∧ (1st
‘𝑟) ∈ 𝑋 ∧ (1st
‘𝑠) ∈ 𝑋)) → ((1st
‘𝑟)𝑀(1st ‘𝑠)) ≤ (((1st ‘𝑡)𝑀(1st ‘𝑟)) +𝑒 ((1st
‘𝑡)𝑀(1st ‘𝑠)))) |
134 | 88, 91, 93, 96, 133 | syl13anc 1222 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((1st ‘𝑟)𝑀(1st ‘𝑠)) ≤ (((1st ‘𝑡)𝑀(1st ‘𝑟)) +𝑒 ((1st
‘𝑡)𝑀(1st ‘𝑠)))) |
135 | | xrmax1sup 11161 |
. . . . . . . 8
⊢
((((1st ‘𝑡)𝑀(1st ‘𝑟)) ∈ ℝ* ∧
((2nd ‘𝑡)𝑁(2nd ‘𝑟)) ∈ ℝ*) →
((1st ‘𝑡)𝑀(1st ‘𝑟)) ≤ sup({((1st ‘𝑡)𝑀(1st ‘𝑟)), ((2nd ‘𝑡)𝑁(2nd ‘𝑟))}, ℝ*, <
)) |
136 | 95, 105, 135 | syl2anc 409 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((1st ‘𝑡)𝑀(1st ‘𝑟)) ≤ sup({((1st ‘𝑡)𝑀(1st ‘𝑟)), ((2nd ‘𝑡)𝑁(2nd ‘𝑟))}, ℝ*, <
)) |
137 | 136, 117 | breqtrrd 3994 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((1st ‘𝑡)𝑀(1st ‘𝑟)) ≤ (𝑡𝑃𝑟)) |
138 | | xrmax1sup 11161 |
. . . . . . . 8
⊢
((((1st ‘𝑡)𝑀(1st ‘𝑠)) ∈ ℝ* ∧
((2nd ‘𝑡)𝑁(2nd ‘𝑠)) ∈ ℝ*) →
((1st ‘𝑡)𝑀(1st ‘𝑠)) ≤ sup({((1st ‘𝑡)𝑀(1st ‘𝑠)), ((2nd ‘𝑡)𝑁(2nd ‘𝑠))}, ℝ*, <
)) |
139 | 98, 122, 138 | syl2anc 409 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((1st ‘𝑡)𝑀(1st ‘𝑠)) ≤ sup({((1st ‘𝑡)𝑀(1st ‘𝑠)), ((2nd ‘𝑡)𝑁(2nd ‘𝑠))}, ℝ*, <
)) |
140 | 139, 130 | breqtrrd 3994 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((1st ‘𝑡)𝑀(1st ‘𝑠)) ≤ (𝑡𝑃𝑠)) |
141 | | xle2add 9789 |
. . . . . . 7
⊢
(((((1st ‘𝑡)𝑀(1st ‘𝑟)) ∈ ℝ* ∧
((1st ‘𝑡)𝑀(1st ‘𝑠)) ∈ ℝ*) ∧ ((𝑡𝑃𝑟) ∈ ℝ* ∧ (𝑡𝑃𝑠) ∈ ℝ*)) →
((((1st ‘𝑡)𝑀(1st ‘𝑟)) ≤ (𝑡𝑃𝑟) ∧ ((1st ‘𝑡)𝑀(1st ‘𝑠)) ≤ (𝑡𝑃𝑠)) → (((1st ‘𝑡)𝑀(1st ‘𝑟)) +𝑒 ((1st
‘𝑡)𝑀(1st ‘𝑠))) ≤ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠)))) |
142 | 95, 98, 118, 131, 141 | syl22anc 1221 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((((1st ‘𝑡)𝑀(1st ‘𝑟)) ≤ (𝑡𝑃𝑟) ∧ ((1st ‘𝑡)𝑀(1st ‘𝑠)) ≤ (𝑡𝑃𝑠)) → (((1st ‘𝑡)𝑀(1st ‘𝑟)) +𝑒 ((1st
‘𝑡)𝑀(1st ‘𝑠))) ≤ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠)))) |
143 | 137, 140,
142 | mp2and 430 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (((1st ‘𝑡)𝑀(1st ‘𝑟)) +𝑒 ((1st
‘𝑡)𝑀(1st ‘𝑠))) ≤ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠))) |
144 | 87, 99, 132, 134, 143 | xrletrd 9722 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((1st ‘𝑟)𝑀(1st ‘𝑠)) ≤ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠))) |
145 | 24 | 3adantr3 1143 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ∈
ℝ*) |
146 | 105, 122 | xaddcld 9794 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (((2nd ‘𝑡)𝑁(2nd ‘𝑟)) +𝑒 ((2nd
‘𝑡)𝑁(2nd ‘𝑠))) ∈
ℝ*) |
147 | | xmettri2 12831 |
. . . . . 6
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ ((2nd
‘𝑡) ∈ 𝑌 ∧ (2nd
‘𝑟) ∈ 𝑌 ∧ (2nd
‘𝑠) ∈ 𝑌)) → ((2nd
‘𝑟)𝑁(2nd ‘𝑠)) ≤ (((2nd ‘𝑡)𝑁(2nd ‘𝑟)) +𝑒 ((2nd
‘𝑡)𝑁(2nd ‘𝑠)))) |
148 | 100, 102,
103, 120, 147 | syl13anc 1222 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ≤ (((2nd ‘𝑡)𝑁(2nd ‘𝑟)) +𝑒 ((2nd
‘𝑡)𝑁(2nd ‘𝑠)))) |
149 | | xrmax2sup 11162 |
. . . . . . . 8
⊢
((((1st ‘𝑡)𝑀(1st ‘𝑟)) ∈ ℝ* ∧
((2nd ‘𝑡)𝑁(2nd ‘𝑟)) ∈ ℝ*) →
((2nd ‘𝑡)𝑁(2nd ‘𝑟)) ≤ sup({((1st ‘𝑡)𝑀(1st ‘𝑟)), ((2nd ‘𝑡)𝑁(2nd ‘𝑟))}, ℝ*, <
)) |
150 | 95, 105, 149 | syl2anc 409 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((2nd ‘𝑡)𝑁(2nd ‘𝑟)) ≤ sup({((1st ‘𝑡)𝑀(1st ‘𝑟)), ((2nd ‘𝑡)𝑁(2nd ‘𝑟))}, ℝ*, <
)) |
151 | 150, 117 | breqtrrd 3994 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((2nd ‘𝑡)𝑁(2nd ‘𝑟)) ≤ (𝑡𝑃𝑟)) |
152 | | xrmax2sup 11162 |
. . . . . . . 8
⊢
((((1st ‘𝑡)𝑀(1st ‘𝑠)) ∈ ℝ* ∧
((2nd ‘𝑡)𝑁(2nd ‘𝑠)) ∈ ℝ*) →
((2nd ‘𝑡)𝑁(2nd ‘𝑠)) ≤ sup({((1st ‘𝑡)𝑀(1st ‘𝑠)), ((2nd ‘𝑡)𝑁(2nd ‘𝑠))}, ℝ*, <
)) |
153 | 98, 122, 152 | syl2anc 409 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((2nd ‘𝑡)𝑁(2nd ‘𝑠)) ≤ sup({((1st ‘𝑡)𝑀(1st ‘𝑠)), ((2nd ‘𝑡)𝑁(2nd ‘𝑠))}, ℝ*, <
)) |
154 | 153, 130 | breqtrrd 3994 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((2nd ‘𝑡)𝑁(2nd ‘𝑠)) ≤ (𝑡𝑃𝑠)) |
155 | | xle2add 9789 |
. . . . . . 7
⊢
(((((2nd ‘𝑡)𝑁(2nd ‘𝑟)) ∈ ℝ* ∧
((2nd ‘𝑡)𝑁(2nd ‘𝑠)) ∈ ℝ*) ∧ ((𝑡𝑃𝑟) ∈ ℝ* ∧ (𝑡𝑃𝑠) ∈ ℝ*)) →
((((2nd ‘𝑡)𝑁(2nd ‘𝑟)) ≤ (𝑡𝑃𝑟) ∧ ((2nd ‘𝑡)𝑁(2nd ‘𝑠)) ≤ (𝑡𝑃𝑠)) → (((2nd ‘𝑡)𝑁(2nd ‘𝑟)) +𝑒 ((2nd
‘𝑡)𝑁(2nd ‘𝑠))) ≤ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠)))) |
156 | 105, 122,
118, 131, 155 | syl22anc 1221 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((((2nd ‘𝑡)𝑁(2nd ‘𝑟)) ≤ (𝑡𝑃𝑟) ∧ ((2nd ‘𝑡)𝑁(2nd ‘𝑠)) ≤ (𝑡𝑃𝑠)) → (((2nd ‘𝑡)𝑁(2nd ‘𝑟)) +𝑒 ((2nd
‘𝑡)𝑁(2nd ‘𝑠))) ≤ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠)))) |
157 | 151, 154,
156 | mp2and 430 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (((2nd ‘𝑡)𝑁(2nd ‘𝑟)) +𝑒 ((2nd
‘𝑡)𝑁(2nd ‘𝑠))) ≤ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠))) |
158 | 145, 146,
132, 148, 157 | xrletrd 9722 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → ((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ≤ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠))) |
159 | | xrmaxlesup 11167 |
. . . . 5
⊢
((((1st ‘𝑟)𝑀(1st ‘𝑠)) ∈ ℝ* ∧
((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ∈ ℝ* ∧ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠)) ∈ ℝ*) →
(sup({((1st ‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, < ) ≤ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠)) ↔ (((1st ‘𝑟)𝑀(1st ‘𝑠)) ≤ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠)) ∧ ((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ≤ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠))))) |
160 | 87, 145, 132, 159 | syl3anc 1220 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (sup({((1st
‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, < ) ≤ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠)) ↔ (((1st ‘𝑟)𝑀(1st ‘𝑠)) ≤ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠)) ∧ ((2nd ‘𝑟)𝑁(2nd ‘𝑠)) ≤ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠))))) |
161 | 144, 158,
160 | mpbir2and 929 |
. . 3
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → sup({((1st
‘𝑟)𝑀(1st ‘𝑠)), ((2nd ‘𝑟)𝑁(2nd ‘𝑠))}, ℝ*, < ) ≤ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠))) |
162 | 86, 161 | eqbrtrd 3988 |
. 2
⊢ ((𝜑 ∧ (𝑟 ∈ (𝑋 × 𝑌) ∧ 𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌))) → (𝑟𝑃𝑠) ≤ ((𝑡𝑃𝑟) +𝑒 (𝑡𝑃𝑠))) |
163 | 10, 44, 85, 162 | isxmetd 12817 |
1
⊢ (𝜑 → 𝑃 ∈ (∞Met‘(𝑋 × 𝑌))) |