Step | Hyp | Ref
| Expression |
1 | | xmetxp.p |
. . . 4
⊢ 𝑃 = (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ sup({((1st ‘𝑢)𝑀(1st ‘𝑣)), ((2nd ‘𝑢)𝑁(2nd ‘𝑣))}, ℝ*, <
)) |
2 | | xmetxp.1 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) |
3 | | xmetxp.2 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) |
4 | 1, 2, 3 | xmetxp 13301 |
. . 3
⊢ (𝜑 → 𝑃 ∈ (∞Met‘(𝑋 × 𝑌))) |
5 | | xmetxpbl.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ (𝑋 × 𝑌)) |
6 | | xmetxpbl.r |
. . 3
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
7 | | blval 13183 |
. . 3
⊢ ((𝑃 ∈ (∞Met‘(𝑋 × 𝑌)) ∧ 𝐶 ∈ (𝑋 × 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝐶(ball‘𝑃)𝑅) = {𝑡 ∈ (𝑋 × 𝑌) ∣ (𝐶𝑃𝑡) < 𝑅}) |
8 | 4, 5, 6, 7 | syl3anc 1233 |
. 2
⊢ (𝜑 → (𝐶(ball‘𝑃)𝑅) = {𝑡 ∈ (𝑋 × 𝑌) ∣ (𝐶𝑃𝑡) < 𝑅}) |
9 | 5 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝐶 ∈ (𝑋 × 𝑌)) |
10 | | simpr 109 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝑡 ∈ (𝑋 × 𝑌)) |
11 | 2 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝑀 ∈ (∞Met‘𝑋)) |
12 | | xp1st 6144 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑋 × 𝑌) → (1st ‘𝐶) ∈ 𝑋) |
13 | 9, 12 | syl 14 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (1st ‘𝐶) ∈ 𝑋) |
14 | | xp1st 6144 |
. . . . . . . . 9
⊢ (𝑡 ∈ (𝑋 × 𝑌) → (1st ‘𝑡) ∈ 𝑋) |
15 | 14 | adantl 275 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (1st ‘𝑡) ∈ 𝑋) |
16 | | xmetcl 13146 |
. . . . . . . 8
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ (1st
‘𝐶) ∈ 𝑋 ∧ (1st
‘𝑡) ∈ 𝑋) → ((1st
‘𝐶)𝑀(1st ‘𝑡)) ∈
ℝ*) |
17 | 11, 13, 15, 16 | syl3anc 1233 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → ((1st ‘𝐶)𝑀(1st ‘𝑡)) ∈
ℝ*) |
18 | 3 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝑁 ∈ (∞Met‘𝑌)) |
19 | | xp2nd 6145 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑋 × 𝑌) → (2nd ‘𝐶) ∈ 𝑌) |
20 | 9, 19 | syl 14 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (2nd ‘𝐶) ∈ 𝑌) |
21 | | xp2nd 6145 |
. . . . . . . . 9
⊢ (𝑡 ∈ (𝑋 × 𝑌) → (2nd ‘𝑡) ∈ 𝑌) |
22 | 21 | adantl 275 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑡) ∈ 𝑌) |
23 | | xmetcl 13146 |
. . . . . . . 8
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ (2nd
‘𝐶) ∈ 𝑌 ∧ (2nd
‘𝑡) ∈ 𝑌) → ((2nd
‘𝐶)𝑁(2nd ‘𝑡)) ∈
ℝ*) |
24 | 18, 20, 22, 23 | syl3anc 1233 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → ((2nd ‘𝐶)𝑁(2nd ‘𝑡)) ∈
ℝ*) |
25 | | xrmaxcl 11215 |
. . . . . . 7
⊢
((((1st ‘𝐶)𝑀(1st ‘𝑡)) ∈ ℝ* ∧
((2nd ‘𝐶)𝑁(2nd ‘𝑡)) ∈ ℝ*) →
sup({((1st ‘𝐶)𝑀(1st ‘𝑡)), ((2nd ‘𝐶)𝑁(2nd ‘𝑡))}, ℝ*, < ) ∈
ℝ*) |
26 | 17, 24, 25 | syl2anc 409 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → sup({((1st ‘𝐶)𝑀(1st ‘𝑡)), ((2nd ‘𝐶)𝑁(2nd ‘𝑡))}, ℝ*, < ) ∈
ℝ*) |
27 | | fveq2 5496 |
. . . . . . . . . 10
⊢ (𝑢 = 𝐶 → (1st ‘𝑢) = (1st ‘𝐶)) |
28 | | fveq2 5496 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑡 → (1st ‘𝑣) = (1st ‘𝑡)) |
29 | 27, 28 | oveqan12d 5872 |
. . . . . . . . 9
⊢ ((𝑢 = 𝐶 ∧ 𝑣 = 𝑡) → ((1st ‘𝑢)𝑀(1st ‘𝑣)) = ((1st ‘𝐶)𝑀(1st ‘𝑡))) |
30 | | fveq2 5496 |
. . . . . . . . . 10
⊢ (𝑢 = 𝐶 → (2nd ‘𝑢) = (2nd ‘𝐶)) |
31 | | fveq2 5496 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑡 → (2nd ‘𝑣) = (2nd ‘𝑡)) |
32 | 30, 31 | oveqan12d 5872 |
. . . . . . . . 9
⊢ ((𝑢 = 𝐶 ∧ 𝑣 = 𝑡) → ((2nd ‘𝑢)𝑁(2nd ‘𝑣)) = ((2nd ‘𝐶)𝑁(2nd ‘𝑡))) |
33 | 29, 32 | preq12d 3668 |
. . . . . . . 8
⊢ ((𝑢 = 𝐶 ∧ 𝑣 = 𝑡) → {((1st ‘𝑢)𝑀(1st ‘𝑣)), ((2nd ‘𝑢)𝑁(2nd ‘𝑣))} = {((1st ‘𝐶)𝑀(1st ‘𝑡)), ((2nd ‘𝐶)𝑁(2nd ‘𝑡))}) |
34 | 33 | supeq1d 6964 |
. . . . . . 7
⊢ ((𝑢 = 𝐶 ∧ 𝑣 = 𝑡) → sup({((1st ‘𝑢)𝑀(1st ‘𝑣)), ((2nd ‘𝑢)𝑁(2nd ‘𝑣))}, ℝ*, < ) =
sup({((1st ‘𝐶)𝑀(1st ‘𝑡)), ((2nd ‘𝐶)𝑁(2nd ‘𝑡))}, ℝ*, <
)) |
35 | 34, 1 | ovmpoga 5982 |
. . . . . 6
⊢ ((𝐶 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌) ∧ sup({((1st ‘𝐶)𝑀(1st ‘𝑡)), ((2nd ‘𝐶)𝑁(2nd ‘𝑡))}, ℝ*, < ) ∈
ℝ*) → (𝐶𝑃𝑡) = sup({((1st ‘𝐶)𝑀(1st ‘𝑡)), ((2nd ‘𝐶)𝑁(2nd ‘𝑡))}, ℝ*, <
)) |
36 | 9, 10, 26, 35 | syl3anc 1233 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (𝐶𝑃𝑡) = sup({((1st ‘𝐶)𝑀(1st ‘𝑡)), ((2nd ‘𝐶)𝑁(2nd ‘𝑡))}, ℝ*, <
)) |
37 | 36 | breq1d 3999 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → ((𝐶𝑃𝑡) < 𝑅 ↔ sup({((1st ‘𝐶)𝑀(1st ‘𝑡)), ((2nd ‘𝐶)𝑁(2nd ‘𝑡))}, ℝ*, < ) < 𝑅)) |
38 | 6 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝑅 ∈
ℝ*) |
39 | | xrmaxltsup 11221 |
. . . . 5
⊢
((((1st ‘𝐶)𝑀(1st ‘𝑡)) ∈ ℝ* ∧
((2nd ‘𝐶)𝑁(2nd ‘𝑡)) ∈ ℝ* ∧ 𝑅 ∈ ℝ*)
→ (sup({((1st ‘𝐶)𝑀(1st ‘𝑡)), ((2nd ‘𝐶)𝑁(2nd ‘𝑡))}, ℝ*, < ) < 𝑅 ↔ (((1st
‘𝐶)𝑀(1st ‘𝑡)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑡)) < 𝑅))) |
40 | 17, 24, 38, 39 | syl3anc 1233 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (sup({((1st
‘𝐶)𝑀(1st ‘𝑡)), ((2nd ‘𝐶)𝑁(2nd ‘𝑡))}, ℝ*, < ) < 𝑅 ↔ (((1st
‘𝐶)𝑀(1st ‘𝑡)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑡)) < 𝑅))) |
41 | 37, 40 | bitrd 187 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → ((𝐶𝑃𝑡) < 𝑅 ↔ (((1st ‘𝐶)𝑀(1st ‘𝑡)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑡)) < 𝑅))) |
42 | 41 | rabbidva 2718 |
. 2
⊢ (𝜑 → {𝑡 ∈ (𝑋 × 𝑌) ∣ (𝐶𝑃𝑡) < 𝑅} = {𝑡 ∈ (𝑋 × 𝑌) ∣ (((1st ‘𝐶)𝑀(1st ‘𝑡)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑡)) < 𝑅)}) |
43 | | 1st2nd2 6154 |
. . . . . . 7
⊢ (𝑛 ∈ (𝑋 × 𝑌) → 𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉) |
44 | 43 | ad2antrl 487 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) → 𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉) |
45 | | xp1st 6144 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝑋 × 𝑌) → (1st ‘𝑛) ∈ 𝑋) |
46 | 45 | ad2antrl 487 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) → (1st ‘𝑛) ∈ 𝑋) |
47 | | simprrl 534 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) → ((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅) |
48 | 5, 12 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘𝐶) ∈ 𝑋) |
49 | | elbl 13185 |
. . . . . . . . 9
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ (1st
‘𝐶) ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) →
((1st ‘𝑛)
∈ ((1st ‘𝐶)(ball‘𝑀)𝑅) ↔ ((1st ‘𝑛) ∈ 𝑋 ∧ ((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅))) |
50 | 2, 48, 6, 49 | syl3anc 1233 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ↔ ((1st ‘𝑛) ∈ 𝑋 ∧ ((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅))) |
51 | 50 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) → ((1st ‘𝑛) ∈ ((1st
‘𝐶)(ball‘𝑀)𝑅) ↔ ((1st ‘𝑛) ∈ 𝑋 ∧ ((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅))) |
52 | 46, 47, 51 | mpbir2and 939 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) → (1st ‘𝑛) ∈ ((1st
‘𝐶)(ball‘𝑀)𝑅)) |
53 | | xp2nd 6145 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝑋 × 𝑌) → (2nd ‘𝑛) ∈ 𝑌) |
54 | 53 | ad2antrl 487 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) → (2nd ‘𝑛) ∈ 𝑌) |
55 | | simprrr 535 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) → ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅) |
56 | 5, 19 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘𝐶) ∈ 𝑌) |
57 | | elbl 13185 |
. . . . . . . . 9
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ (2nd
‘𝐶) ∈ 𝑌 ∧ 𝑅 ∈ ℝ*) →
((2nd ‘𝑛)
∈ ((2nd ‘𝐶)(ball‘𝑁)𝑅) ↔ ((2nd ‘𝑛) ∈ 𝑌 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) |
58 | 3, 56, 6, 57 | syl3anc 1233 |
. . . . . . . 8
⊢ (𝜑 → ((2nd
‘𝑛) ∈
((2nd ‘𝐶)(ball‘𝑁)𝑅) ↔ ((2nd ‘𝑛) ∈ 𝑌 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) |
59 | 58 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) → ((2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅) ↔ ((2nd ‘𝑛) ∈ 𝑌 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) |
60 | 54, 55, 59 | mpbir2and 939 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) → (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)) |
61 | 44, 52, 60 | jca32 308 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) → (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)))) |
62 | | simprl 526 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)))) → 𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉) |
63 | | simprrl 534 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)))) → (1st ‘𝑛) ∈ ((1st
‘𝐶)(ball‘𝑀)𝑅)) |
64 | 50 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)))) → ((1st ‘𝑛) ∈ ((1st
‘𝐶)(ball‘𝑀)𝑅) ↔ ((1st ‘𝑛) ∈ 𝑋 ∧ ((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅))) |
65 | 63, 64 | mpbid 146 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)))) → ((1st ‘𝑛) ∈ 𝑋 ∧ ((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅)) |
66 | 65 | simpld 111 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)))) → (1st ‘𝑛) ∈ 𝑋) |
67 | | simprrr 535 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)))) → (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)) |
68 | 58 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)))) → ((2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅) ↔ ((2nd ‘𝑛) ∈ 𝑌 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) |
69 | 67, 68 | mpbid 146 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)))) → ((2nd ‘𝑛) ∈ 𝑌 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅)) |
70 | 69 | simpld 111 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)))) → (2nd ‘𝑛) ∈ 𝑌) |
71 | 62, 66, 70 | jca32 308 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)))) → (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈ 𝑋 ∧ (2nd
‘𝑛) ∈ 𝑌))) |
72 | | elxp6 6148 |
. . . . . . 7
⊢ (𝑛 ∈ (𝑋 × 𝑌) ↔ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈ 𝑋 ∧ (2nd
‘𝑛) ∈ 𝑌))) |
73 | 71, 72 | sylibr 133 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)))) → 𝑛 ∈ (𝑋 × 𝑌)) |
74 | 65 | simprd 113 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)))) → ((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅) |
75 | 69 | simprd 113 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)))) → ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅) |
76 | 73, 74, 75 | jca32 308 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)))) → (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) |
77 | 61, 76 | impbida 591 |
. . . 4
⊢ (𝜑 → ((𝑛 ∈ (𝑋 × 𝑌) ∧ (((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅)) ↔ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅))))) |
78 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑡 = 𝑛 → (1st ‘𝑡) = (1st ‘𝑛)) |
79 | 78 | oveq2d 5869 |
. . . . . . 7
⊢ (𝑡 = 𝑛 → ((1st ‘𝐶)𝑀(1st ‘𝑡)) = ((1st ‘𝐶)𝑀(1st ‘𝑛))) |
80 | 79 | breq1d 3999 |
. . . . . 6
⊢ (𝑡 = 𝑛 → (((1st ‘𝐶)𝑀(1st ‘𝑡)) < 𝑅 ↔ ((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅)) |
81 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑡 = 𝑛 → (2nd ‘𝑡) = (2nd ‘𝑛)) |
82 | 81 | oveq2d 5869 |
. . . . . . 7
⊢ (𝑡 = 𝑛 → ((2nd ‘𝐶)𝑁(2nd ‘𝑡)) = ((2nd ‘𝐶)𝑁(2nd ‘𝑛))) |
83 | 82 | breq1d 3999 |
. . . . . 6
⊢ (𝑡 = 𝑛 → (((2nd ‘𝐶)𝑁(2nd ‘𝑡)) < 𝑅 ↔ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅)) |
84 | 80, 83 | anbi12d 470 |
. . . . 5
⊢ (𝑡 = 𝑛 → ((((1st ‘𝐶)𝑀(1st ‘𝑡)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑡)) < 𝑅) ↔ (((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) |
85 | 84 | elrab 2886 |
. . . 4
⊢ (𝑛 ∈ {𝑡 ∈ (𝑋 × 𝑌) ∣ (((1st ‘𝐶)𝑀(1st ‘𝑡)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑡)) < 𝑅)} ↔ (𝑛 ∈ (𝑋 × 𝑌) ∧ (((1st ‘𝐶)𝑀(1st ‘𝑛)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑛)) < 𝑅))) |
86 | | elxp6 6148 |
. . . 4
⊢ (𝑛 ∈ (((1st
‘𝐶)(ball‘𝑀)𝑅) × ((2nd ‘𝐶)(ball‘𝑁)𝑅)) ↔ (𝑛 = 〈(1st ‘𝑛), (2nd ‘𝑛)〉 ∧ ((1st
‘𝑛) ∈
((1st ‘𝐶)(ball‘𝑀)𝑅) ∧ (2nd ‘𝑛) ∈ ((2nd
‘𝐶)(ball‘𝑁)𝑅)))) |
87 | 77, 85, 86 | 3bitr4g 222 |
. . 3
⊢ (𝜑 → (𝑛 ∈ {𝑡 ∈ (𝑋 × 𝑌) ∣ (((1st ‘𝐶)𝑀(1st ‘𝑡)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑡)) < 𝑅)} ↔ 𝑛 ∈ (((1st ‘𝐶)(ball‘𝑀)𝑅) × ((2nd ‘𝐶)(ball‘𝑁)𝑅)))) |
88 | 87 | eqrdv 2168 |
. 2
⊢ (𝜑 → {𝑡 ∈ (𝑋 × 𝑌) ∣ (((1st ‘𝐶)𝑀(1st ‘𝑡)) < 𝑅 ∧ ((2nd ‘𝐶)𝑁(2nd ‘𝑡)) < 𝑅)} = (((1st ‘𝐶)(ball‘𝑀)𝑅) × ((2nd ‘𝐶)(ball‘𝑁)𝑅))) |
89 | 8, 42, 88 | 3eqtrd 2207 |
1
⊢ (𝜑 → (𝐶(ball‘𝑃)𝑅) = (((1st ‘𝐶)(ball‘𝑀)𝑅) × ((2nd ‘𝐶)(ball‘𝑁)𝑅))) |