Step | Hyp | Ref
| Expression |
1 | | bcthlem.4 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) |
2 | | cmetmet 23084 |
. . . . . . 7
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
4 | | metxmet 22139 |
. . . . . 6
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
6 | | bcthlem.9 |
. . . . 5
⊢ (𝜑 → 𝑔:ℕ⟶(𝑋 ×
ℝ+)) |
7 | | bcth.2 |
. . . . . 6
⊢ 𝐽 = (MetOpen‘𝐷) |
8 | | bcthlem.5 |
. . . . . 6
⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦
{〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))}) |
9 | | bcthlem.6 |
. . . . . 6
⊢ (𝜑 → 𝑀:ℕ⟶(Clsd‘𝐽)) |
10 | | bcthlem.7 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
11 | | bcthlem.8 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
12 | | bcthlem.10 |
. . . . . 6
⊢ (𝜑 → (𝑔‘1) = 〈𝐶, 𝑅〉) |
13 | | bcthlem.11 |
. . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘))) |
14 | 7, 1, 8, 9, 10, 11, 6, 12, 13 | bcthlem2 23122 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔‘𝑛))) |
15 | | elrp 11834 |
. . . . . . . . 9
⊢ (𝑟 ∈ ℝ+
↔ (𝑟 ∈ ℝ
∧ 0 < 𝑟)) |
16 | | nnrecl 11290 |
. . . . . . . . 9
⊢ ((𝑟 ∈ ℝ ∧ 0 <
𝑟) → ∃𝑚 ∈ ℕ (1 / 𝑚) < 𝑟) |
17 | 15, 16 | sylbi 207 |
. . . . . . . 8
⊢ (𝑟 ∈ ℝ+
→ ∃𝑚 ∈
ℕ (1 / 𝑚) < 𝑟) |
18 | 17 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑚 ∈ ℕ (1
/ 𝑚) < 𝑟) |
19 | | peano2nn 11032 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → (𝑚 + 1) ∈
ℕ) |
20 | 19 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈
ℕ) |
21 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑚 → (𝑘 + 1) = (𝑚 + 1)) |
22 | 21 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑚 → (𝑔‘(𝑘 + 1)) = (𝑔‘(𝑚 + 1))) |
23 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑚 → 𝑘 = 𝑚) |
24 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑚 → (𝑔‘𝑘) = (𝑔‘𝑚)) |
25 | 23, 24 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑚 → (𝑘𝐹(𝑔‘𝑘)) = (𝑚𝐹(𝑔‘𝑚))) |
26 | 22, 25 | eleq12d 2695 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑚 → ((𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)) ↔ (𝑔‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑔‘𝑚)))) |
27 | 26 | rspccva 3308 |
. . . . . . . . . . . . . 14
⊢
((∀𝑘 ∈
ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)) ∧ 𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑔‘𝑚))) |
28 | 13, 27 | sylan 488 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑔‘𝑚))) |
29 | 6 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑔‘𝑚) ∈ (𝑋 ×
ℝ+)) |
30 | 7, 1, 8 | bcthlem1 23121 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔‘𝑚) ∈ (𝑋 × ℝ+))) →
((𝑔‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑔‘𝑚)) ↔ ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) ∧
(2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑚)) ∖ (𝑀‘𝑚))))) |
31 | 30 | expr 643 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑔‘𝑚) ∈ (𝑋 × ℝ+) → ((𝑔‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑔‘𝑚)) ↔ ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) ∧
(2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑚)) ∖ (𝑀‘𝑚)))))) |
32 | 29, 31 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑔‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑔‘𝑚)) ↔ ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) ∧
(2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑚)) ∖ (𝑀‘𝑚))))) |
33 | 28, 32 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) ∧
(2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑚)) ∖ (𝑀‘𝑚)))) |
34 | 33 | simp2d 1074 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2nd
‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚)) |
35 | 34 | adantlr 751 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) →
(2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚)) |
36 | 33 | simp1d 1073 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ∈ (𝑋 ×
ℝ+)) |
37 | | xp2nd 7199 |
. . . . . . . . . . . . . 14
⊢ ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) →
(2nd ‘(𝑔‘(𝑚 + 1))) ∈
ℝ+) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2nd
‘(𝑔‘(𝑚 + 1))) ∈
ℝ+) |
39 | 38 | rpred 11872 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2nd
‘(𝑔‘(𝑚 + 1))) ∈
ℝ) |
40 | 39 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) →
(2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ) |
41 | | nnrecre 11057 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ → (1 /
𝑚) ∈
ℝ) |
42 | 41 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (1 /
𝑚) ∈
ℝ) |
43 | | rpre 11839 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
44 | 43 | ad2antlr 763 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → 𝑟 ∈
ℝ) |
45 | | lttr 10114 |
. . . . . . . . . . 11
⊢
(((2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ ∧ (1 / 𝑚) ∈ ℝ ∧ 𝑟 ∈ ℝ) →
(((2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚) ∧ (1 / 𝑚) < 𝑟) → (2nd ‘(𝑔‘(𝑚 + 1))) < 𝑟)) |
46 | 40, 42, 44, 45 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) →
(((2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚) ∧ (1 / 𝑚) < 𝑟) → (2nd ‘(𝑔‘(𝑚 + 1))) < 𝑟)) |
47 | 35, 46 | mpand 711 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → ((1 /
𝑚) < 𝑟 → (2nd ‘(𝑔‘(𝑚 + 1))) < 𝑟)) |
48 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑚 + 1) → (𝑔‘𝑛) = (𝑔‘(𝑚 + 1))) |
49 | 48 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑚 + 1) → (2nd ‘(𝑔‘𝑛)) = (2nd ‘(𝑔‘(𝑚 + 1)))) |
50 | 49 | breq1d 4663 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑚 + 1) → ((2nd ‘(𝑔‘𝑛)) < 𝑟 ↔ (2nd ‘(𝑔‘(𝑚 + 1))) < 𝑟)) |
51 | 50 | rspcev 3309 |
. . . . . . . . 9
⊢ (((𝑚 + 1) ∈ ℕ ∧
(2nd ‘(𝑔‘(𝑚 + 1))) < 𝑟) → ∃𝑛 ∈ ℕ (2nd ‘(𝑔‘𝑛)) < 𝑟) |
52 | 20, 47, 51 | syl6an 568 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → ((1 /
𝑚) < 𝑟 → ∃𝑛 ∈ ℕ (2nd ‘(𝑔‘𝑛)) < 𝑟)) |
53 | 52 | rexlimdva 3031 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∃𝑚 ∈ ℕ (1
/ 𝑚) < 𝑟 → ∃𝑛 ∈ ℕ (2nd
‘(𝑔‘𝑛)) < 𝑟)) |
54 | 18, 53 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑛 ∈ ℕ
(2nd ‘(𝑔‘𝑛)) < 𝑟) |
55 | 54 | ralrimiva 2966 |
. . . . 5
⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑛 ∈ ℕ (2nd
‘(𝑔‘𝑛)) < 𝑟) |
56 | 5, 6, 14, 55 | caubl 23106 |
. . . 4
⊢ (𝜑 → (1st ∘
𝑔) ∈ (Cau‘𝐷)) |
57 | 7 | cmetcau 23087 |
. . . 4
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (1st ∘
𝑔) ∈ (Cau‘𝐷)) → (1st
∘ 𝑔) ∈ dom
(⇝𝑡‘𝐽)) |
58 | 1, 56, 57 | syl2anc 693 |
. . 3
⊢ (𝜑 → (1st ∘
𝑔) ∈ dom
(⇝𝑡‘𝐽)) |
59 | | fo1st 7188 |
. . . . . 6
⊢
1st :V–onto→V |
60 | | fofun 6116 |
. . . . . 6
⊢
(1st :V–onto→V → Fun 1st ) |
61 | 59, 60 | ax-mp 5 |
. . . . 5
⊢ Fun
1st |
62 | | vex 3203 |
. . . . 5
⊢ 𝑔 ∈ V |
63 | | cofunexg 7130 |
. . . . 5
⊢ ((Fun
1st ∧ 𝑔
∈ V) → (1st ∘ 𝑔) ∈ V) |
64 | 61, 62, 63 | mp2an 708 |
. . . 4
⊢
(1st ∘ 𝑔) ∈ V |
65 | 64 | eldm 5321 |
. . 3
⊢
((1st ∘ 𝑔) ∈ dom
(⇝𝑡‘𝐽) ↔ ∃𝑥(1st ∘ 𝑔)(⇝𝑡‘𝐽)𝑥) |
66 | 58, 65 | sylib 208 |
. 2
⊢ (𝜑 → ∃𝑥(1st ∘ 𝑔)(⇝𝑡‘𝐽)𝑥) |
67 | | 1nn 11031 |
. . . . . 6
⊢ 1 ∈
ℕ |
68 | 7, 1, 8, 9, 10, 11, 6, 12, 13 | bcthlem3 23123 |
. . . . . 6
⊢ ((𝜑 ∧ (1st ∘
𝑔)(⇝𝑡‘𝐽)𝑥 ∧ 1 ∈ ℕ) → 𝑥 ∈ ((ball‘𝐷)‘(𝑔‘1))) |
69 | 67, 68 | mp3an3 1413 |
. . . . 5
⊢ ((𝜑 ∧ (1st ∘
𝑔)(⇝𝑡‘𝐽)𝑥) → 𝑥 ∈ ((ball‘𝐷)‘(𝑔‘1))) |
70 | 12 | fveq2d 6195 |
. . . . . . 7
⊢ (𝜑 → ((ball‘𝐷)‘(𝑔‘1)) = ((ball‘𝐷)‘〈𝐶, 𝑅〉)) |
71 | | df-ov 6653 |
. . . . . . 7
⊢ (𝐶(ball‘𝐷)𝑅) = ((ball‘𝐷)‘〈𝐶, 𝑅〉) |
72 | 70, 71 | syl6eqr 2674 |
. . . . . 6
⊢ (𝜑 → ((ball‘𝐷)‘(𝑔‘1)) = (𝐶(ball‘𝐷)𝑅)) |
73 | 72 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (1st ∘
𝑔)(⇝𝑡‘𝐽)𝑥) → ((ball‘𝐷)‘(𝑔‘1)) = (𝐶(ball‘𝐷)𝑅)) |
74 | 69, 73 | eleqtrd 2703 |
. . . 4
⊢ ((𝜑 ∧ (1st ∘
𝑔)(⇝𝑡‘𝐽)𝑥) → 𝑥 ∈ (𝐶(ball‘𝐷)𝑅)) |
75 | 7 | mopntop 22245 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) |
76 | 5, 75 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ Top) |
77 | 76 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐽 ∈ Top) |
78 | 5 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐷 ∈ (∞Met‘𝑋)) |
79 | | xp1st 7198 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) →
(1st ‘(𝑔‘(𝑚 + 1))) ∈ 𝑋) |
80 | 36, 79 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (1st
‘(𝑔‘(𝑚 + 1))) ∈ 𝑋) |
81 | 38 | rpxrd 11873 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2nd
‘(𝑔‘(𝑚 + 1))) ∈
ℝ*) |
82 | | blssm 22223 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st
‘(𝑔‘(𝑚 + 1))) ∈ 𝑋 ∧ (2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ*) →
((1st ‘(𝑔‘(𝑚 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑚 + 1)))) ⊆ 𝑋) |
83 | 78, 80, 81, 82 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((1st
‘(𝑔‘(𝑚 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑚 + 1)))) ⊆ 𝑋) |
84 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) → (𝑔‘(𝑚 + 1)) = 〈(1st ‘(𝑔‘(𝑚 + 1))), (2nd ‘(𝑔‘(𝑚 + 1)))〉) |
85 | 36, 84 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) = 〈(1st ‘(𝑔‘(𝑚 + 1))), (2nd ‘(𝑔‘(𝑚 + 1)))〉) |
86 | 85 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) = ((ball‘𝐷)‘〈(1st ‘(𝑔‘(𝑚 + 1))), (2nd ‘(𝑔‘(𝑚 + 1)))〉)) |
87 | | df-ov 6653 |
. . . . . . . . . . . . . 14
⊢
((1st ‘(𝑔‘(𝑚 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑚 + 1)))) = ((ball‘𝐷)‘〈(1st ‘(𝑔‘(𝑚 + 1))), (2nd ‘(𝑔‘(𝑚 + 1)))〉) |
88 | 86, 87 | syl6reqr 2675 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((1st
‘(𝑔‘(𝑚 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑚 + 1)))) = ((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))) |
89 | 7 | mopnuni 22246 |
. . . . . . . . . . . . . . 15
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
90 | 5, 89 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
91 | 90 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑋 = ∪ 𝐽) |
92 | 83, 88, 91 | 3sstr3d 3647 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ ∪
𝐽) |
93 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ ∪ 𝐽 =
∪ 𝐽 |
94 | 93 | sscls 20860 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧
((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ ∪
𝐽) →
((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1))))) |
95 | 77, 92, 94 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1))))) |
96 | 33 | simp3d 1075 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑚)) ∖ (𝑀‘𝑚))) |
97 | 95, 96 | sstrd 3613 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑚)) ∖ (𝑀‘𝑚))) |
98 | 97 | 3adant2 1080 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (1st ∘
𝑔)(⇝𝑡‘𝐽)𝑥 ∧ 𝑚 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ (((ball‘𝐷)‘(𝑔‘𝑚)) ∖ (𝑀‘𝑚))) |
99 | 7, 1, 8, 9, 10, 11, 6, 12, 13 | bcthlem3 23123 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (1st ∘
𝑔)(⇝𝑡‘𝐽)𝑥 ∧ (𝑚 + 1) ∈ ℕ) → 𝑥 ∈ ((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))) |
100 | 19, 99 | syl3an3 1361 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (1st ∘
𝑔)(⇝𝑡‘𝐽)𝑥 ∧ 𝑚 ∈ ℕ) → 𝑥 ∈ ((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))) |
101 | 98, 100 | sseldd 3604 |
. . . . . . . 8
⊢ ((𝜑 ∧ (1st ∘
𝑔)(⇝𝑡‘𝐽)𝑥 ∧ 𝑚 ∈ ℕ) → 𝑥 ∈ (((ball‘𝐷)‘(𝑔‘𝑚)) ∖ (𝑀‘𝑚))) |
102 | 101 | eldifbd 3587 |
. . . . . . 7
⊢ ((𝜑 ∧ (1st ∘
𝑔)(⇝𝑡‘𝐽)𝑥 ∧ 𝑚 ∈ ℕ) → ¬ 𝑥 ∈ (𝑀‘𝑚)) |
103 | 102 | 3expa 1265 |
. . . . . 6
⊢ (((𝜑 ∧ (1st ∘
𝑔)(⇝𝑡‘𝐽)𝑥) ∧ 𝑚 ∈ ℕ) → ¬ 𝑥 ∈ (𝑀‘𝑚)) |
104 | 103 | ralrimiva 2966 |
. . . . 5
⊢ ((𝜑 ∧ (1st ∘
𝑔)(⇝𝑡‘𝐽)𝑥) → ∀𝑚 ∈ ℕ ¬ 𝑥 ∈ (𝑀‘𝑚)) |
105 | | eluni2 4440 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∪ ran 𝑀 ↔ ∃𝑦 ∈ ran 𝑀 𝑥 ∈ 𝑦) |
106 | | ffn 6045 |
. . . . . . . . . . 11
⊢ (𝑀:ℕ⟶(Clsd‘𝐽) → 𝑀 Fn ℕ) |
107 | 9, 106 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 Fn ℕ) |
108 | | eleq2 2690 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑀‘𝑚) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑀‘𝑚))) |
109 | 108 | rexrn 6361 |
. . . . . . . . . 10
⊢ (𝑀 Fn ℕ → (∃𝑦 ∈ ran 𝑀 𝑥 ∈ 𝑦 ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑀‘𝑚))) |
110 | 107, 109 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑦 ∈ ran 𝑀 𝑥 ∈ 𝑦 ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑀‘𝑚))) |
111 | 105, 110 | syl5bb 272 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ∪ ran
𝑀 ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑀‘𝑚))) |
112 | 111 | notbid 308 |
. . . . . . 7
⊢ (𝜑 → (¬ 𝑥 ∈ ∪ ran
𝑀 ↔ ¬ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑀‘𝑚))) |
113 | | ralnex 2992 |
. . . . . . 7
⊢
(∀𝑚 ∈
ℕ ¬ 𝑥 ∈
(𝑀‘𝑚) ↔ ¬ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑀‘𝑚)) |
114 | 112, 113 | syl6bbr 278 |
. . . . . 6
⊢ (𝜑 → (¬ 𝑥 ∈ ∪ ran
𝑀 ↔ ∀𝑚 ∈ ℕ ¬ 𝑥 ∈ (𝑀‘𝑚))) |
115 | 114 | biimpar 502 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ ¬ 𝑥 ∈ (𝑀‘𝑚)) → ¬ 𝑥 ∈ ∪ ran
𝑀) |
116 | 104, 115 | syldan 487 |
. . . 4
⊢ ((𝜑 ∧ (1st ∘
𝑔)(⇝𝑡‘𝐽)𝑥) → ¬ 𝑥 ∈ ∪ ran
𝑀) |
117 | 74, 116 | eldifd 3585 |
. . 3
⊢ ((𝜑 ∧ (1st ∘
𝑔)(⇝𝑡‘𝐽)𝑥) → 𝑥 ∈ ((𝐶(ball‘𝐷)𝑅) ∖ ∪ ran
𝑀)) |
118 | | ne0i 3921 |
. . 3
⊢ (𝑥 ∈ ((𝐶(ball‘𝐷)𝑅) ∖ ∪ ran
𝑀) → ((𝐶(ball‘𝐷)𝑅) ∖ ∪ ran
𝑀) ≠
∅) |
119 | 117, 118 | syl 17 |
. 2
⊢ ((𝜑 ∧ (1st ∘
𝑔)(⇝𝑡‘𝐽)𝑥) → ((𝐶(ball‘𝐷)𝑅) ∖ ∪ ran
𝑀) ≠
∅) |
120 | 66, 119 | exlimddv 1863 |
1
⊢ (𝜑 → ((𝐶(ball‘𝐷)𝑅) ∖ ∪ ran
𝑀) ≠
∅) |