Step | Hyp | Ref
| Expression |
1 | | xmetxp.p |
. . . 4
⊢ 𝑃 = (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ sup({((1^{st} ‘𝑢)𝑀(1^{st} ‘𝑣)), ((2^{nd} ‘𝑢)𝑁(2^{nd} ‘𝑣))}, ℝ^{*}, <
)) |
2 | | xmetxp.1 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) |
3 | | xmetxp.2 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) |
4 | 1, 2, 3 | xmetxp 12571 |
. . 3
⊢ (𝜑 → 𝑃 ∈ (∞Met‘(𝑋 × 𝑌))) |
5 | | xmetxpbl.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ (𝑋 × 𝑌)) |
6 | | xmetxpbl.r |
. . 3
⊢ (𝜑 → 𝑅 ∈
ℝ^{*}) |
7 | | blval 12453 |
. . 3
⊢ ((𝑃 ∈ (∞Met‘(𝑋 × 𝑌)) ∧ 𝐶 ∈ (𝑋 × 𝑌) ∧ 𝑅 ∈ ℝ^{*}) → (𝐶(ball‘𝑃)𝑅) = {𝑡 ∈ (𝑋 × 𝑌) ∣ (𝐶𝑃𝑡) < 𝑅}) |
8 | 4, 5, 6, 7 | syl3anc 1199 |
. 2
⊢ (𝜑 → (𝐶(ball‘𝑃)𝑅) = {𝑡 ∈ (𝑋 × 𝑌) ∣ (𝐶𝑃𝑡) < 𝑅}) |
9 | 5 | adantr 272 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝐶 ∈ (𝑋 × 𝑌)) |
10 | | simpr 109 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝑡 ∈ (𝑋 × 𝑌)) |
11 | 2 | adantr 272 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝑀 ∈ (∞Met‘𝑋)) |
12 | | xp1st 6029 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑋 × 𝑌) → (1^{st} ‘𝐶) ∈ 𝑋) |
13 | 9, 12 | syl 14 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (1^{st} ‘𝐶) ∈ 𝑋) |
14 | | xp1st 6029 |
. . . . . . . . 9
⊢ (𝑡 ∈ (𝑋 × 𝑌) → (1^{st} ‘𝑡) ∈ 𝑋) |
15 | 14 | adantl 273 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (1^{st} ‘𝑡) ∈ 𝑋) |
16 | | xmetcl 12416 |
. . . . . . . 8
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ (1^{st}
‘𝐶) ∈ 𝑋 ∧ (1^{st}
‘𝑡) ∈ 𝑋) → ((1^{st}
‘𝐶)𝑀(1^{st} ‘𝑡)) ∈
ℝ^{*}) |
17 | 11, 13, 15, 16 | syl3anc 1199 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → ((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)) ∈
ℝ^{*}) |
18 | 3 | adantr 272 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝑁 ∈ (∞Met‘𝑌)) |
19 | | xp2nd 6030 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑋 × 𝑌) → (2^{nd} ‘𝐶) ∈ 𝑌) |
20 | 9, 19 | syl 14 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (2^{nd} ‘𝐶) ∈ 𝑌) |
21 | | xp2nd 6030 |
. . . . . . . . 9
⊢ (𝑡 ∈ (𝑋 × 𝑌) → (2^{nd} ‘𝑡) ∈ 𝑌) |
22 | 21 | adantl 273 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (2^{nd} ‘𝑡) ∈ 𝑌) |
23 | | xmetcl 12416 |
. . . . . . . 8
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ (2^{nd}
‘𝐶) ∈ 𝑌 ∧ (2^{nd}
‘𝑡) ∈ 𝑌) → ((2^{nd}
‘𝐶)𝑁(2^{nd} ‘𝑡)) ∈
ℝ^{*}) |
24 | 18, 20, 22, 23 | syl3anc 1199 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡)) ∈
ℝ^{*}) |
25 | | xrmaxcl 10961 |
. . . . . . 7
⊢
((((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)) ∈ ℝ^{*} ∧
((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡)) ∈ ℝ^{*}) →
sup({((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)), ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡))}, ℝ^{*}, < ) ∈
ℝ^{*}) |
26 | 17, 24, 25 | syl2anc 406 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → sup({((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)), ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡))}, ℝ^{*}, < ) ∈
ℝ^{*}) |
27 | | fveq2 5387 |
. . . . . . . . . 10
⊢ (𝑢 = 𝐶 → (1^{st} ‘𝑢) = (1^{st} ‘𝐶)) |
28 | | fveq2 5387 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑡 → (1^{st} ‘𝑣) = (1^{st} ‘𝑡)) |
29 | 27, 28 | oveqan12d 5759 |
. . . . . . . . 9
⊢ ((𝑢 = 𝐶 ∧ 𝑣 = 𝑡) → ((1^{st} ‘𝑢)𝑀(1^{st} ‘𝑣)) = ((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡))) |
30 | | fveq2 5387 |
. . . . . . . . . 10
⊢ (𝑢 = 𝐶 → (2^{nd} ‘𝑢) = (2^{nd} ‘𝐶)) |
31 | | fveq2 5387 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑡 → (2^{nd} ‘𝑣) = (2^{nd} ‘𝑡)) |
32 | 30, 31 | oveqan12d 5759 |
. . . . . . . . 9
⊢ ((𝑢 = 𝐶 ∧ 𝑣 = 𝑡) → ((2^{nd} ‘𝑢)𝑁(2^{nd} ‘𝑣)) = ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡))) |
33 | 29, 32 | preq12d 3576 |
. . . . . . . 8
⊢ ((𝑢 = 𝐶 ∧ 𝑣 = 𝑡) → {((1^{st} ‘𝑢)𝑀(1^{st} ‘𝑣)), ((2^{nd} ‘𝑢)𝑁(2^{nd} ‘𝑣))} = {((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)), ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡))}) |
34 | 33 | supeq1d 6840 |
. . . . . . 7
⊢ ((𝑢 = 𝐶 ∧ 𝑣 = 𝑡) → sup({((1^{st} ‘𝑢)𝑀(1^{st} ‘𝑣)), ((2^{nd} ‘𝑢)𝑁(2^{nd} ‘𝑣))}, ℝ^{*}, < ) =
sup({((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)), ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡))}, ℝ^{*}, <
)) |
35 | 34, 1 | ovmpoga 5866 |
. . . . . 6
⊢ ((𝐶 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌) ∧ sup({((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)), ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡))}, ℝ^{*}, < ) ∈
ℝ^{*}) → (𝐶𝑃𝑡) = sup({((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)), ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡))}, ℝ^{*}, <
)) |
36 | 9, 10, 26, 35 | syl3anc 1199 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (𝐶𝑃𝑡) = sup({((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)), ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡))}, ℝ^{*}, <
)) |
37 | 36 | breq1d 3907 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → ((𝐶𝑃𝑡) < 𝑅 ↔ sup({((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)), ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡))}, ℝ^{*}, < ) < 𝑅)) |
38 | 6 | adantr 272 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝑅 ∈
ℝ^{*}) |
39 | | xrmaxltsup 10967 |
. . . . 5
⊢
((((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)) ∈ ℝ^{*} ∧
((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡)) ∈ ℝ^{*} ∧ 𝑅 ∈ ℝ^{*})
→ (sup({((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)), ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡))}, ℝ^{*}, < ) < 𝑅 ↔ (((1^{st}
‘𝐶)𝑀(1^{st} ‘𝑡)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡)) < 𝑅))) |
40 | 17, 24, 38, 39 | syl3anc 1199 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (sup({((1^{st}
‘𝐶)𝑀(1^{st} ‘𝑡)), ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡))}, ℝ^{*}, < ) < 𝑅 ↔ (((1^{st}
‘𝐶)𝑀(1^{st} ‘𝑡)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡)) < 𝑅))) |
41 | 37, 40 | bitrd 187 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → ((𝐶𝑃𝑡) < 𝑅 ↔ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡)) < 𝑅))) |
42 | 41 | rabbidva 2646 |
. 2
⊢ (𝜑 → {𝑡 ∈ (𝑋 × 𝑌) ∣ (𝐶𝑃𝑡) < 𝑅} = {𝑡 ∈ (𝑋 × 𝑌) ∣ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡)) < 𝑅)}) |
43 | | 1st2nd2 6039 |
. . . . . . 7
⊢ (𝑛 ∈ (𝑋 × 𝑌) → 𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩) |
44 | 43 | ad2antrl 479 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) → 𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩) |
45 | | xp1st 6029 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝑋 × 𝑌) → (1^{st} ‘𝑛) ∈ 𝑋) |
46 | 45 | ad2antrl 479 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) → (1^{st} ‘𝑛) ∈ 𝑋) |
47 | | simprrl 511 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) → ((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅) |
48 | 5, 12 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → (1^{st}
‘𝐶) ∈ 𝑋) |
49 | | elbl 12455 |
. . . . . . . . 9
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ (1^{st}
‘𝐶) ∈ 𝑋 ∧ 𝑅 ∈ ℝ^{*}) →
((1^{st} ‘𝑛)
∈ ((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ↔ ((1^{st} ‘𝑛) ∈ 𝑋 ∧ ((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅))) |
50 | 2, 48, 6, 49 | syl3anc 1199 |
. . . . . . . 8
⊢ (𝜑 → ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ↔ ((1^{st} ‘𝑛) ∈ 𝑋 ∧ ((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅))) |
51 | 50 | adantr 272 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) → ((1^{st} ‘𝑛) ∈ ((1^{st}
‘𝐶)(ball‘𝑀)𝑅) ↔ ((1^{st} ‘𝑛) ∈ 𝑋 ∧ ((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅))) |
52 | 46, 47, 51 | mpbir2and 911 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) → (1^{st} ‘𝑛) ∈ ((1^{st}
‘𝐶)(ball‘𝑀)𝑅)) |
53 | | xp2nd 6030 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝑋 × 𝑌) → (2^{nd} ‘𝑛) ∈ 𝑌) |
54 | 53 | ad2antrl 479 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) → (2^{nd} ‘𝑛) ∈ 𝑌) |
55 | | simprrr 512 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) → ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅) |
56 | 5, 19 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → (2^{nd}
‘𝐶) ∈ 𝑌) |
57 | | elbl 12455 |
. . . . . . . . 9
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ (2^{nd}
‘𝐶) ∈ 𝑌 ∧ 𝑅 ∈ ℝ^{*}) →
((2^{nd} ‘𝑛)
∈ ((2^{nd} ‘𝐶)(ball‘𝑁)𝑅) ↔ ((2^{nd} ‘𝑛) ∈ 𝑌 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) |
58 | 3, 56, 6, 57 | syl3anc 1199 |
. . . . . . . 8
⊢ (𝜑 → ((2^{nd}
‘𝑛) ∈
((2^{nd} ‘𝐶)(ball‘𝑁)𝑅) ↔ ((2^{nd} ‘𝑛) ∈ 𝑌 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) |
59 | 58 | adantr 272 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) → ((2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅) ↔ ((2^{nd} ‘𝑛) ∈ 𝑌 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) |
60 | 54, 55, 59 | mpbir2and 911 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) → (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)) |
61 | 44, 52, 60 | jca32 306 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) → (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)))) |
62 | | simprl 503 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)))) → 𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩) |
63 | | simprrl 511 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)))) → (1^{st} ‘𝑛) ∈ ((1^{st}
‘𝐶)(ball‘𝑀)𝑅)) |
64 | 50 | adantr 272 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)))) → ((1^{st} ‘𝑛) ∈ ((1^{st}
‘𝐶)(ball‘𝑀)𝑅) ↔ ((1^{st} ‘𝑛) ∈ 𝑋 ∧ ((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅))) |
65 | 63, 64 | mpbid 146 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)))) → ((1^{st} ‘𝑛) ∈ 𝑋 ∧ ((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅)) |
66 | 65 | simpld 111 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)))) → (1^{st} ‘𝑛) ∈ 𝑋) |
67 | | simprrr 512 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)))) → (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)) |
68 | 58 | adantr 272 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)))) → ((2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅) ↔ ((2^{nd} ‘𝑛) ∈ 𝑌 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) |
69 | 67, 68 | mpbid 146 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)))) → ((2^{nd} ‘𝑛) ∈ 𝑌 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅)) |
70 | 69 | simpld 111 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)))) → (2^{nd} ‘𝑛) ∈ 𝑌) |
71 | 62, 66, 70 | jca32 306 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)))) → (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈ 𝑋 ∧ (2^{nd}
‘𝑛) ∈ 𝑌))) |
72 | | elxp6 6033 |
. . . . . . 7
⊢ (𝑛 ∈ (𝑋 × 𝑌) ↔ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈ 𝑋 ∧ (2^{nd}
‘𝑛) ∈ 𝑌))) |
73 | 71, 72 | sylibr 133 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)))) → 𝑛 ∈ (𝑋 × 𝑌)) |
74 | 65 | simprd 113 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)))) → ((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅) |
75 | 69 | simprd 113 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)))) → ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅) |
76 | 73, 74, 75 | jca32 306 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)))) → (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) |
77 | 61, 76 | impbida 568 |
. . . 4
⊢ (𝜑 → ((𝑛 ∈ (𝑋 × 𝑌) ∧ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅)) ↔ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅))))) |
78 | | fveq2 5387 |
. . . . . . . 8
⊢ (𝑡 = 𝑛 → (1^{st} ‘𝑡) = (1^{st} ‘𝑛)) |
79 | 78 | oveq2d 5756 |
. . . . . . 7
⊢ (𝑡 = 𝑛 → ((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)) = ((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛))) |
80 | 79 | breq1d 3907 |
. . . . . 6
⊢ (𝑡 = 𝑛 → (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)) < 𝑅 ↔ ((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅)) |
81 | | fveq2 5387 |
. . . . . . . 8
⊢ (𝑡 = 𝑛 → (2^{nd} ‘𝑡) = (2^{nd} ‘𝑛)) |
82 | 81 | oveq2d 5756 |
. . . . . . 7
⊢ (𝑡 = 𝑛 → ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡)) = ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛))) |
83 | 82 | breq1d 3907 |
. . . . . 6
⊢ (𝑡 = 𝑛 → (((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡)) < 𝑅 ↔ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅)) |
84 | 80, 83 | anbi12d 462 |
. . . . 5
⊢ (𝑡 = 𝑛 → ((((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡)) < 𝑅) ↔ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) |
85 | 84 | elrab 2811 |
. . . 4
⊢ (𝑛 ∈ {𝑡 ∈ (𝑋 × 𝑌) ∣ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡)) < 𝑅)} ↔ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑛)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑛)) < 𝑅))) |
86 | | elxp6 6033 |
. . . 4
⊢ (𝑛 ∈ (((1^{st}
‘𝐶)(ball‘𝑀)𝑅) × ((2^{nd} ‘𝐶)(ball‘𝑁)𝑅)) ↔ (𝑛 = ⟨(1^{st} ‘𝑛), (2^{nd} ‘𝑛)⟩ ∧ ((1^{st}
‘𝑛) ∈
((1^{st} ‘𝐶)(ball‘𝑀)𝑅) ∧ (2^{nd} ‘𝑛) ∈ ((2^{nd}
‘𝐶)(ball‘𝑁)𝑅)))) |
87 | 77, 85, 86 | 3bitr4g 222 |
. . 3
⊢ (𝜑 → (𝑛 ∈ {𝑡 ∈ (𝑋 × 𝑌) ∣ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡)) < 𝑅)} ↔ 𝑛 ∈ (((1^{st} ‘𝐶)(ball‘𝑀)𝑅) × ((2^{nd} ‘𝐶)(ball‘𝑁)𝑅)))) |
88 | 87 | eqrdv 2113 |
. 2
⊢ (𝜑 → {𝑡 ∈ (𝑋 × 𝑌) ∣ (((1^{st} ‘𝐶)𝑀(1^{st} ‘𝑡)) < 𝑅 ∧ ((2^{nd} ‘𝐶)𝑁(2^{nd} ‘𝑡)) < 𝑅)} = (((1^{st} ‘𝐶)(ball‘𝑀)𝑅) × ((2^{nd} ‘𝐶)(ball‘𝑁)𝑅))) |
89 | 8, 42, 88 | 3eqtrd 2152 |
1
⊢ (𝜑 → (𝐶(ball‘𝑃)𝑅) = (((1^{st} ‘𝐶)(ball‘𝑀)𝑅) × ((2^{nd} ‘𝐶)(ball‘𝑁)𝑅))) |