Proof of Theorem bcthlem1
Step | Hyp | Ref
| Expression |
1 | | opabssxp 5673 |
. . . . . . 7
⊢
{〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))} ⊆ (𝑋 ×
ℝ+) |
2 | | bcthlem.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) |
3 | | elfvdm 6798 |
. . . . . . . . 9
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝑋 ∈ dom CMet) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ dom CMet) |
5 | | reex 10972 |
. . . . . . . . 9
⊢ ℝ
∈ V |
6 | | rpssre 12747 |
. . . . . . . . 9
⊢
ℝ+ ⊆ ℝ |
7 | 5, 6 | ssexi 5244 |
. . . . . . . 8
⊢
ℝ+ ∈ V |
8 | | xpexg 7590 |
. . . . . . . 8
⊢ ((𝑋 ∈ dom CMet ∧
ℝ+ ∈ V) → (𝑋 × ℝ+) ∈
V) |
9 | 4, 7, 8 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → (𝑋 × ℝ+) ∈
V) |
10 | | ssexg 5245 |
. . . . . . 7
⊢
(({〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))} ⊆ (𝑋 × ℝ+) ∧ (𝑋 × ℝ+)
∈ V) → {〈𝑥,
𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))} ∈ V) |
11 | 1, 9, 10 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))} ∈ V) |
12 | | oveq2 7275 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐴 → (1 / 𝑘) = (1 / 𝐴)) |
13 | 12 | breq2d 5085 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐴 → (𝑟 < (1 / 𝑘) ↔ 𝑟 < (1 / 𝐴))) |
14 | | fveq2 6766 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐴 → (𝑀‘𝑘) = (𝑀‘𝐴)) |
15 | 14 | difeq2d 4056 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐴 → (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) = (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝐴))) |
16 | 15 | sseq2d 3952 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐴 → (((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)) ↔ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝐴)))) |
17 | 13, 16 | anbi12d 631 |
. . . . . . . . 9
⊢ (𝑘 = 𝐴 → ((𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))) ↔ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝐴))))) |
18 | 17 | anbi2d 629 |
. . . . . . . 8
⊢ (𝑘 = 𝐴 → (((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘)))) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝐴)))))) |
19 | 18 | opabbidv 5139 |
. . . . . . 7
⊢ (𝑘 = 𝐴 → {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))} = {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝐴))))}) |
20 | | fveq2 6766 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝐵 → ((ball‘𝐷)‘𝑧) = ((ball‘𝐷)‘𝐵)) |
21 | 20 | difeq1d 4055 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐵 → (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝐴)) = (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))) |
22 | 21 | sseq2d 3952 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐵 → (((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝐴)) ↔ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴)))) |
23 | 22 | anbi2d 629 |
. . . . . . . . 9
⊢ (𝑧 = 𝐵 → ((𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝐴))) ↔ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))) |
24 | 23 | anbi2d 629 |
. . . . . . . 8
⊢ (𝑧 = 𝐵 → (((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝐴)))) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴)))))) |
25 | 24 | opabbidv 5139 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝐴))))} = {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))}) |
26 | | bcthlem.5 |
. . . . . . 7
⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦
{〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))}) |
27 | 19, 25, 26 | ovmpog 7422 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (𝑋 × ℝ+) ∧
{〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))} ∈ V) → (𝐴𝐹𝐵) = {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))}) |
28 | 11, 27 | syl3an3 1164 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (𝑋 × ℝ+) ∧ 𝜑) → (𝐴𝐹𝐵) = {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))}) |
29 | 28 | 3expa 1117 |
. . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ (𝑋 × ℝ+)) ∧ 𝜑) → (𝐴𝐹𝐵) = {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))}) |
30 | 29 | ancoms 459 |
. . 3
⊢ ((𝜑 ∧ (𝐴 ∈ ℕ ∧ 𝐵 ∈ (𝑋 × ℝ+))) →
(𝐴𝐹𝐵) = {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))}) |
31 | 30 | eleq2d 2824 |
. 2
⊢ ((𝜑 ∧ (𝐴 ∈ ℕ ∧ 𝐵 ∈ (𝑋 × ℝ+))) →
(𝐶 ∈ (𝐴𝐹𝐵) ↔ 𝐶 ∈ {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))})) |
32 | 1 | sseli 3916 |
. . 3
⊢ (𝐶 ∈ {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))} → 𝐶 ∈ (𝑋 ×
ℝ+)) |
33 | | simp1 1135 |
. . 3
⊢ ((𝐶 ∈ (𝑋 × ℝ+) ∧
(2nd ‘𝐶)
< (1 / 𝐴) ∧
((cls‘𝐽)‘((ball‘𝐷)‘𝐶)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))) → 𝐶 ∈ (𝑋 ×
ℝ+)) |
34 | | 1st2nd2 7859 |
. . . . . 6
⊢ (𝐶 ∈ (𝑋 × ℝ+) → 𝐶 = 〈(1st
‘𝐶), (2nd
‘𝐶)〉) |
35 | 34 | eleq1d 2823 |
. . . . 5
⊢ (𝐶 ∈ (𝑋 × ℝ+) → (𝐶 ∈ {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))} ↔ 〈(1st
‘𝐶), (2nd
‘𝐶)〉 ∈
{〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))})) |
36 | | fvex 6779 |
. . . . . 6
⊢
(1st ‘𝐶) ∈ V |
37 | | fvex 6779 |
. . . . . 6
⊢
(2nd ‘𝐶) ∈ V |
38 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝑥 = (1st ‘𝐶) → (𝑥 ∈ 𝑋 ↔ (1st ‘𝐶) ∈ 𝑋)) |
39 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝑟 = (2nd ‘𝐶) → (𝑟 ∈ ℝ+ ↔
(2nd ‘𝐶)
∈ ℝ+)) |
40 | 38, 39 | bi2anan9 636 |
. . . . . . 7
⊢ ((𝑥 = (1st ‘𝐶) ∧ 𝑟 = (2nd ‘𝐶)) → ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ↔
((1st ‘𝐶)
∈ 𝑋 ∧
(2nd ‘𝐶)
∈ ℝ+))) |
41 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝑥 = (1st ‘𝐶) ∧ 𝑟 = (2nd ‘𝐶)) → 𝑟 = (2nd ‘𝐶)) |
42 | 41 | breq1d 5083 |
. . . . . . . 8
⊢ ((𝑥 = (1st ‘𝐶) ∧ 𝑟 = (2nd ‘𝐶)) → (𝑟 < (1 / 𝐴) ↔ (2nd ‘𝐶) < (1 / 𝐴))) |
43 | | oveq12 7276 |
. . . . . . . . . 10
⊢ ((𝑥 = (1st ‘𝐶) ∧ 𝑟 = (2nd ‘𝐶)) → (𝑥(ball‘𝐷)𝑟) = ((1st ‘𝐶)(ball‘𝐷)(2nd ‘𝐶))) |
44 | 43 | fveq2d 6770 |
. . . . . . . . 9
⊢ ((𝑥 = (1st ‘𝐶) ∧ 𝑟 = (2nd ‘𝐶)) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) = ((cls‘𝐽)‘((1st ‘𝐶)(ball‘𝐷)(2nd ‘𝐶)))) |
45 | 44 | sseq1d 3951 |
. . . . . . . 8
⊢ ((𝑥 = (1st ‘𝐶) ∧ 𝑟 = (2nd ‘𝐶)) → (((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴)) ↔ ((cls‘𝐽)‘((1st ‘𝐶)(ball‘𝐷)(2nd ‘𝐶))) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴)))) |
46 | 42, 45 | anbi12d 631 |
. . . . . . 7
⊢ ((𝑥 = (1st ‘𝐶) ∧ 𝑟 = (2nd ‘𝐶)) → ((𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))) ↔ ((2nd ‘𝐶) < (1 / 𝐴) ∧ ((cls‘𝐽)‘((1st ‘𝐶)(ball‘𝐷)(2nd ‘𝐶))) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))) |
47 | 40, 46 | anbi12d 631 |
. . . . . 6
⊢ ((𝑥 = (1st ‘𝐶) ∧ 𝑟 = (2nd ‘𝐶)) → (((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴)))) ↔ (((1st ‘𝐶) ∈ 𝑋 ∧ (2nd ‘𝐶) ∈ ℝ+)
∧ ((2nd ‘𝐶) < (1 / 𝐴) ∧ ((cls‘𝐽)‘((1st ‘𝐶)(ball‘𝐷)(2nd ‘𝐶))) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴)))))) |
48 | 36, 37, 47 | opelopaba 5446 |
. . . . 5
⊢
(〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈ {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))} ↔ (((1st ‘𝐶) ∈ 𝑋 ∧ (2nd ‘𝐶) ∈ ℝ+)
∧ ((2nd ‘𝐶) < (1 / 𝐴) ∧ ((cls‘𝐽)‘((1st ‘𝐶)(ball‘𝐷)(2nd ‘𝐶))) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))) |
49 | 35, 48 | bitrdi 287 |
. . . 4
⊢ (𝐶 ∈ (𝑋 × ℝ+) → (𝐶 ∈ {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))} ↔ (((1st ‘𝐶) ∈ 𝑋 ∧ (2nd ‘𝐶) ∈ ℝ+)
∧ ((2nd ‘𝐶) < (1 / 𝐴) ∧ ((cls‘𝐽)‘((1st ‘𝐶)(ball‘𝐷)(2nd ‘𝐶))) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴)))))) |
50 | 34 | eleq1d 2823 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑋 × ℝ+) → (𝐶 ∈ (𝑋 × ℝ+) ↔
〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈ (𝑋 ×
ℝ+))) |
51 | | opelxp 5620 |
. . . . . . 7
⊢
(〈(1st ‘𝐶), (2nd ‘𝐶)〉 ∈ (𝑋 × ℝ+) ↔
((1st ‘𝐶)
∈ 𝑋 ∧
(2nd ‘𝐶)
∈ ℝ+)) |
52 | 50, 51 | bitr2di 288 |
. . . . . 6
⊢ (𝐶 ∈ (𝑋 × ℝ+) →
(((1st ‘𝐶)
∈ 𝑋 ∧
(2nd ‘𝐶)
∈ ℝ+) ↔ 𝐶 ∈ (𝑋 ×
ℝ+))) |
53 | | df-ov 7270 |
. . . . . . . . . 10
⊢
((1st ‘𝐶)(ball‘𝐷)(2nd ‘𝐶)) = ((ball‘𝐷)‘〈(1st ‘𝐶), (2nd ‘𝐶)〉) |
54 | 34 | fveq2d 6770 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝑋 × ℝ+) →
((ball‘𝐷)‘𝐶) = ((ball‘𝐷)‘〈(1st
‘𝐶), (2nd
‘𝐶)〉)) |
55 | 53, 54 | eqtr4id 2797 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑋 × ℝ+) →
((1st ‘𝐶)(ball‘𝐷)(2nd ‘𝐶)) = ((ball‘𝐷)‘𝐶)) |
56 | 55 | fveq2d 6770 |
. . . . . . . 8
⊢ (𝐶 ∈ (𝑋 × ℝ+) →
((cls‘𝐽)‘((1st ‘𝐶)(ball‘𝐷)(2nd ‘𝐶))) = ((cls‘𝐽)‘((ball‘𝐷)‘𝐶))) |
57 | 56 | sseq1d 3951 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑋 × ℝ+) →
(((cls‘𝐽)‘((1st ‘𝐶)(ball‘𝐷)(2nd ‘𝐶))) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴)) ↔ ((cls‘𝐽)‘((ball‘𝐷)‘𝐶)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴)))) |
58 | 57 | anbi2d 629 |
. . . . . 6
⊢ (𝐶 ∈ (𝑋 × ℝ+) →
(((2nd ‘𝐶)
< (1 / 𝐴) ∧
((cls‘𝐽)‘((1st ‘𝐶)(ball‘𝐷)(2nd ‘𝐶))) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))) ↔ ((2nd ‘𝐶) < (1 / 𝐴) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘𝐶)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))) |
59 | 52, 58 | anbi12d 631 |
. . . . 5
⊢ (𝐶 ∈ (𝑋 × ℝ+) →
((((1st ‘𝐶) ∈ 𝑋 ∧ (2nd ‘𝐶) ∈ ℝ+)
∧ ((2nd ‘𝐶) < (1 / 𝐴) ∧ ((cls‘𝐽)‘((1st ‘𝐶)(ball‘𝐷)(2nd ‘𝐶))) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴)))) ↔ (𝐶 ∈ (𝑋 × ℝ+) ∧
((2nd ‘𝐶)
< (1 / 𝐴) ∧
((cls‘𝐽)‘((ball‘𝐷)‘𝐶)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴)))))) |
60 | | 3anass 1094 |
. . . . 5
⊢ ((𝐶 ∈ (𝑋 × ℝ+) ∧
(2nd ‘𝐶)
< (1 / 𝐴) ∧
((cls‘𝐽)‘((ball‘𝐷)‘𝐶)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))) ↔ (𝐶 ∈ (𝑋 × ℝ+) ∧
((2nd ‘𝐶)
< (1 / 𝐴) ∧
((cls‘𝐽)‘((ball‘𝐷)‘𝐶)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))) |
61 | 59, 60 | bitr4di 289 |
. . . 4
⊢ (𝐶 ∈ (𝑋 × ℝ+) →
((((1st ‘𝐶) ∈ 𝑋 ∧ (2nd ‘𝐶) ∈ ℝ+)
∧ ((2nd ‘𝐶) < (1 / 𝐴) ∧ ((cls‘𝐽)‘((1st ‘𝐶)(ball‘𝐷)(2nd ‘𝐶))) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴)))) ↔ (𝐶 ∈ (𝑋 × ℝ+) ∧
(2nd ‘𝐶)
< (1 / 𝐴) ∧
((cls‘𝐽)‘((ball‘𝐷)‘𝐶)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))) |
62 | 49, 61 | bitrd 278 |
. . 3
⊢ (𝐶 ∈ (𝑋 × ℝ+) → (𝐶 ∈ {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))} ↔ (𝐶 ∈ (𝑋 × ℝ+) ∧
(2nd ‘𝐶)
< (1 / 𝐴) ∧
((cls‘𝐽)‘((ball‘𝐷)‘𝐶)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))) |
63 | 32, 33, 62 | pm5.21nii 380 |
. 2
⊢ (𝐶 ∈ {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝐴) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))} ↔ (𝐶 ∈ (𝑋 × ℝ+) ∧
(2nd ‘𝐶)
< (1 / 𝐴) ∧
((cls‘𝐽)‘((ball‘𝐷)‘𝐶)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴)))) |
64 | 31, 63 | bitrdi 287 |
1
⊢ ((𝜑 ∧ (𝐴 ∈ ℕ ∧ 𝐵 ∈ (𝑋 × ℝ+))) →
(𝐶 ∈ (𝐴𝐹𝐵) ↔ (𝐶 ∈ (𝑋 × ℝ+) ∧
(2nd ‘𝐶)
< (1 / 𝐴) ∧
((cls‘𝐽)‘((ball‘𝐷)‘𝐶)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))) |