MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bcthlem4 Structured version   Visualization version   GIF version

Theorem bcthlem4 24598
Description: Lemma for bcth 24600. Given any open ball (𝐶(ball‘𝐷)𝑅) as starting point (and in particular, a ball in int( ran 𝑀)), the limit point 𝑥 of the centers of the induced sequence of balls 𝑔 is outside ran 𝑀. Note that a set 𝐴 has empty interior iff every nonempty open set 𝑈 contains points outside 𝐴, i.e. (𝑈𝐴) ≠ ∅. (Contributed by Mario Carneiro, 7-Jan-2014.)
Hypotheses
Ref Expression
bcth.2 𝐽 = (MetOpen‘𝐷)
bcthlem.4 (𝜑𝐷 ∈ (CMet‘𝑋))
bcthlem.5 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))})
bcthlem.6 (𝜑𝑀:ℕ⟶(Clsd‘𝐽))
bcthlem.7 (𝜑𝑅 ∈ ℝ+)
bcthlem.8 (𝜑𝐶𝑋)
bcthlem.9 (𝜑𝑔:ℕ⟶(𝑋 × ℝ+))
bcthlem.10 (𝜑 → (𝑔‘1) = ⟨𝐶, 𝑅⟩)
bcthlem.11 (𝜑 → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔𝑘)))
Assertion
Ref Expression
bcthlem4 (𝜑 → ((𝐶(ball‘𝐷)𝑅) ∖ ran 𝑀) ≠ ∅)
Distinct variable groups:   𝑘,𝑟,𝑥,𝑧   𝐶,𝑟,𝑥   𝑔,𝑘,𝑟,𝑥,𝑧,𝐷   𝑔,𝐹,𝑘,𝑟,𝑥,𝑧   𝑔,𝐽,𝑘,𝑟,𝑥,𝑧   𝑔,𝑀,𝑘,𝑟,𝑥,𝑧   𝜑,𝑘,𝑟,𝑥,𝑧   𝑥,𝑅   𝑔,𝑋,𝑘,𝑟,𝑥,𝑧
Allowed substitution hints:   𝜑(𝑔)   𝐶(𝑧,𝑔,𝑘)   𝑅(𝑧,𝑔,𝑘,𝑟)

Proof of Theorem bcthlem4
Dummy variables 𝑛 𝑚 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bcthlem.4 . . . 4 (𝜑𝐷 ∈ (CMet‘𝑋))
2 cmetmet 24557 . . . . . . 7 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
31, 2syl 17 . . . . . 6 (𝜑𝐷 ∈ (Met‘𝑋))
4 metxmet 23594 . . . . . 6 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
53, 4syl 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)) ∈ (𝑘𝐹(𝑔𝑘)))
147, 1, 8, 9, 10, 11, 6, 12, 13bcthlem2 24596 . . . . 5 (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔𝑛)))
15 elrp 12834 . . . . . . . . 9 (𝑟 ∈ ℝ+ ↔ (𝑟 ∈ ℝ ∧ 0 < 𝑟))
16 nnrecl 12333 . . . . . . . . 9 ((𝑟 ∈ ℝ ∧ 0 < 𝑟) → ∃𝑚 ∈ ℕ (1 / 𝑚) < 𝑟)
1715, 16sylbi 216 . . . . . . . 8 (𝑟 ∈ ℝ+ → ∃𝑚 ∈ ℕ (1 / 𝑚) < 𝑟)
1817adantl 482 . . . . . . 7 ((𝜑𝑟 ∈ ℝ+) → ∃𝑚 ∈ ℕ (1 / 𝑚) < 𝑟)
19 peano2nn 12087 . . . . . . . . . 10 (𝑚 ∈ ℕ → (𝑚 + 1) ∈ ℕ)
2019adantl 482 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℕ)
21 fvoveq1 7361 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑚 → (𝑔‘(𝑘 + 1)) = (𝑔‘(𝑚 + 1)))
22 id 22 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑚𝑘 = 𝑚)
23 fveq2 6826 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑚 → (𝑔𝑘) = (𝑔𝑚))
2422, 23oveq12d 7356 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑚 → (𝑘𝐹(𝑔𝑘)) = (𝑚𝐹(𝑔𝑚)))
2521, 24eleq12d 2831 . . . . . . . . . . . . . . 15 (𝑘 = 𝑚 → ((𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔𝑘)) ↔ (𝑔‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑔𝑚))))
2625rspccva 3569 . . . . . . . . . . . . . 14 ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔𝑘)) ∧ 𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑔𝑚)))
2713, 26sylan 580 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑔𝑚)))
286ffvelcdmda 7018 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (𝑔𝑚) ∈ (𝑋 × ℝ+))
297, 1, 8bcthlem1 24595 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔𝑚) ∈ (𝑋 × ℝ+))) → ((𝑔‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑔𝑚)) ↔ ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) ∧ (2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑚)) ∖ (𝑀𝑚)))))
3029expr 457 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → ((𝑔𝑚) ∈ (𝑋 × ℝ+) → ((𝑔‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑔𝑚)) ↔ ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) ∧ (2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑚)) ∖ (𝑀𝑚))))))
3128, 30mpd 15 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → ((𝑔‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑔𝑚)) ↔ ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) ∧ (2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑚)) ∖ (𝑀𝑚)))))
3227, 31mpbid 231 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) ∧ (2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑚)) ∖ (𝑀𝑚))))
3332simp2d 1142 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚))
3433adantlr 712 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚))
3532simp1d 1141 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+))
36 xp2nd 7933 . . . . . . . . . . . . . 14 ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) → (2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ+)
3735, 36syl 17 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ+)
3837rpred 12874 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ)
3938adantlr 712 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ)
40 nnrecre 12117 . . . . . . . . . . . 12 (𝑚 ∈ ℕ → (1 / 𝑚) ∈ ℝ)
4140adantl 482 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (1 / 𝑚) ∈ ℝ)
42 rpre 12840 . . . . . . . . . . . 12 (𝑟 ∈ ℝ+𝑟 ∈ ℝ)
4342ad2antlr 724 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → 𝑟 ∈ ℝ)
44 lttr 11153 . . . . . . . . . . 11 (((2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ ∧ (1 / 𝑚) ∈ ℝ ∧ 𝑟 ∈ ℝ) → (((2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚) ∧ (1 / 𝑚) < 𝑟) → (2nd ‘(𝑔‘(𝑚 + 1))) < 𝑟))
4539, 41, 43, 44syl3anc 1370 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (((2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚) ∧ (1 / 𝑚) < 𝑟) → (2nd ‘(𝑔‘(𝑚 + 1))) < 𝑟))
4634, 45mpand 692 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → ((1 / 𝑚) < 𝑟 → (2nd ‘(𝑔‘(𝑚 + 1))) < 𝑟))
47 2fveq3 6831 . . . . . . . . . . 11 (𝑛 = (𝑚 + 1) → (2nd ‘(𝑔𝑛)) = (2nd ‘(𝑔‘(𝑚 + 1))))
4847breq1d 5103 . . . . . . . . . 10 (𝑛 = (𝑚 + 1) → ((2nd ‘(𝑔𝑛)) < 𝑟 ↔ (2nd ‘(𝑔‘(𝑚 + 1))) < 𝑟))
4948rspcev 3570 . . . . . . . . 9 (((𝑚 + 1) ∈ ℕ ∧ (2nd ‘(𝑔‘(𝑚 + 1))) < 𝑟) → ∃𝑛 ∈ ℕ (2nd ‘(𝑔𝑛)) < 𝑟)
5020, 46, 49syl6an 681 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → ((1 / 𝑚) < 𝑟 → ∃𝑛 ∈ ℕ (2nd ‘(𝑔𝑛)) < 𝑟))
5150rexlimdva 3148 . . . . . . 7 ((𝜑𝑟 ∈ ℝ+) → (∃𝑚 ∈ ℕ (1 / 𝑚) < 𝑟 → ∃𝑛 ∈ ℕ (2nd ‘(𝑔𝑛)) < 𝑟))
5218, 51mpd 15 . . . . . 6 ((𝜑𝑟 ∈ ℝ+) → ∃𝑛 ∈ ℕ (2nd ‘(𝑔𝑛)) < 𝑟)
5352ralrimiva 3139 . . . . 5 (𝜑 → ∀𝑟 ∈ ℝ+𝑛 ∈ ℕ (2nd ‘(𝑔𝑛)) < 𝑟)
545, 6, 14, 53caubl 24579 . . . 4 (𝜑 → (1st𝑔) ∈ (Cau‘𝐷))
557cmetcau 24560 . . . 4 ((𝐷 ∈ (CMet‘𝑋) ∧ (1st𝑔) ∈ (Cau‘𝐷)) → (1st𝑔) ∈ dom (⇝𝑡𝐽))
561, 54, 55syl2anc 584 . . 3 (𝜑 → (1st𝑔) ∈ dom (⇝𝑡𝐽))
57 fo1st 7920 . . . . . 6 1st :V–onto→V
58 fofun 6741 . . . . . 6 (1st :V–onto→V → Fun 1st )
5957, 58ax-mp 5 . . . . 5 Fun 1st
60 vex 3445 . . . . 5 𝑔 ∈ V
61 cofunexg 7860 . . . . 5 ((Fun 1st𝑔 ∈ V) → (1st𝑔) ∈ V)
6259, 60, 61mp2an 689 . . . 4 (1st𝑔) ∈ V
6362eldm 5843 . . 3 ((1st𝑔) ∈ dom (⇝𝑡𝐽) ↔ ∃𝑥(1st𝑔)(⇝𝑡𝐽)𝑥)
6456, 63sylib 217 . 2 (𝜑 → ∃𝑥(1st𝑔)(⇝𝑡𝐽)𝑥)
65 1nn 12086 . . . . . 6 1 ∈ ℕ
667, 1, 8, 9, 10, 11, 6, 12, 13bcthlem3 24597 . . . . . 6 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥 ∧ 1 ∈ ℕ) → 𝑥 ∈ ((ball‘𝐷)‘(𝑔‘1)))
6765, 66mp3an3 1449 . . . . 5 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥) → 𝑥 ∈ ((ball‘𝐷)‘(𝑔‘1)))
6812fveq2d 6830 . . . . . . 7 (𝜑 → ((ball‘𝐷)‘(𝑔‘1)) = ((ball‘𝐷)‘⟨𝐶, 𝑅⟩))
69 df-ov 7341 . . . . . . 7 (𝐶(ball‘𝐷)𝑅) = ((ball‘𝐷)‘⟨𝐶, 𝑅⟩)
7068, 69eqtr4di 2794 . . . . . 6 (𝜑 → ((ball‘𝐷)‘(𝑔‘1)) = (𝐶(ball‘𝐷)𝑅))
7170adantr 481 . . . . 5 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥) → ((ball‘𝐷)‘(𝑔‘1)) = (𝐶(ball‘𝐷)𝑅))
7267, 71eleqtrd 2839 . . . 4 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥) → 𝑥 ∈ (𝐶(ball‘𝐷)𝑅))
737mopntop 23700 . . . . . . . . . . . . . 14 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
745, 73syl 17 . . . . . . . . . . . . 13 (𝜑𝐽 ∈ Top)
7574adantr 481 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → 𝐽 ∈ Top)
765adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → 𝐷 ∈ (∞Met‘𝑋))
77 xp1st 7932 . . . . . . . . . . . . . . 15 ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) → (1st ‘(𝑔‘(𝑚 + 1))) ∈ 𝑋)
7835, 77syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝑔‘(𝑚 + 1))) ∈ 𝑋)
7937rpxrd 12875 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ*)
80 blssm 23678 . . . . . . . . . . . . . 14 ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔‘(𝑚 + 1))) ∈ 𝑋 ∧ (2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ*) → ((1st ‘(𝑔‘(𝑚 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑚 + 1)))) ⊆ 𝑋)
8176, 78, 79, 80syl3anc 1370 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → ((1st ‘(𝑔‘(𝑚 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑚 + 1)))) ⊆ 𝑋)
82 df-ov 7341 . . . . . . . . . . . . . 14 ((1st ‘(𝑔‘(𝑚 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑚 + 1)))) = ((ball‘𝐷)‘⟨(1st ‘(𝑔‘(𝑚 + 1))), (2nd ‘(𝑔‘(𝑚 + 1)))⟩)
83 1st2nd2 7939 . . . . . . . . . . . . . . . 16 ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) → (𝑔‘(𝑚 + 1)) = ⟨(1st ‘(𝑔‘(𝑚 + 1))), (2nd ‘(𝑔‘(𝑚 + 1)))⟩)
8435, 83syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) = ⟨(1st ‘(𝑔‘(𝑚 + 1))), (2nd ‘(𝑔‘(𝑚 + 1)))⟩)
8584fveq2d 6830 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) = ((ball‘𝐷)‘⟨(1st ‘(𝑔‘(𝑚 + 1))), (2nd ‘(𝑔‘(𝑚 + 1)))⟩))
8682, 85eqtr4id 2795 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → ((1st ‘(𝑔‘(𝑚 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑚 + 1)))) = ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))))
877mopnuni 23701 . . . . . . . . . . . . . . 15 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
885, 87syl 17 . . . . . . . . . . . . . 14 (𝜑𝑋 = 𝐽)
8988adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → 𝑋 = 𝐽)
9081, 86, 893sstr3d 3978 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ 𝐽)
91 eqid 2736 . . . . . . . . . . . . 13 𝐽 = 𝐽
9291sscls 22314 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ 𝐽) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))))
9375, 90, 92syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))))
9432simp3d 1143 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑚)) ∖ (𝑀𝑚)))
9593, 94sstrd 3942 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ (((ball‘𝐷)‘(𝑔𝑚)) ∖ (𝑀𝑚)))
96953adant2 1130 . . . . . . . . 9 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥𝑚 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ (((ball‘𝐷)‘(𝑔𝑚)) ∖ (𝑀𝑚)))
977, 1, 8, 9, 10, 11, 6, 12, 13bcthlem3 24597 . . . . . . . . . 10 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥 ∧ (𝑚 + 1) ∈ ℕ) → 𝑥 ∈ ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))))
9819, 97syl3an3 1164 . . . . . . . . 9 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥𝑚 ∈ ℕ) → 𝑥 ∈ ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))))
9996, 98sseldd 3933 . . . . . . . 8 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥𝑚 ∈ ℕ) → 𝑥 ∈ (((ball‘𝐷)‘(𝑔𝑚)) ∖ (𝑀𝑚)))
10099eldifbd 3911 . . . . . . 7 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥𝑚 ∈ ℕ) → ¬ 𝑥 ∈ (𝑀𝑚))
1011003expa 1117 . . . . . 6 (((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥) ∧ 𝑚 ∈ ℕ) → ¬ 𝑥 ∈ (𝑀𝑚))
102101ralrimiva 3139 . . . . 5 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥) → ∀𝑚 ∈ ℕ ¬ 𝑥 ∈ (𝑀𝑚))
103 eluni2 4857 . . . . . . . . 9 (𝑥 ran 𝑀 ↔ ∃𝑦 ∈ ran 𝑀 𝑥𝑦)
1049ffnd 6653 . . . . . . . . . 10 (𝜑𝑀 Fn ℕ)
105 eleq2 2825 . . . . . . . . . . 11 (𝑦 = (𝑀𝑚) → (𝑥𝑦𝑥 ∈ (𝑀𝑚)))
106105rexrn 7020 . . . . . . . . . 10 (𝑀 Fn ℕ → (∃𝑦 ∈ ran 𝑀 𝑥𝑦 ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑀𝑚)))
107104, 106syl 17 . . . . . . . . 9 (𝜑 → (∃𝑦 ∈ ran 𝑀 𝑥𝑦 ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑀𝑚)))
108103, 107bitrid 282 . . . . . . . 8 (𝜑 → (𝑥 ran 𝑀 ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑀𝑚)))
109108notbid 317 . . . . . . 7 (𝜑 → (¬ 𝑥 ran 𝑀 ↔ ¬ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑀𝑚)))
110 ralnex 3072 . . . . . . 7 (∀𝑚 ∈ ℕ ¬ 𝑥 ∈ (𝑀𝑚) ↔ ¬ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑀𝑚))
111109, 110bitr4di 288 . . . . . 6 (𝜑 → (¬ 𝑥 ran 𝑀 ↔ ∀𝑚 ∈ ℕ ¬ 𝑥 ∈ (𝑀𝑚)))
112111biimpar 478 . . . . 5 ((𝜑 ∧ ∀𝑚 ∈ ℕ ¬ 𝑥 ∈ (𝑀𝑚)) → ¬ 𝑥 ran 𝑀)
113102, 112syldan 591 . . . 4 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥) → ¬ 𝑥 ran 𝑀)
11472, 113eldifd 3909 . . 3 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥) → 𝑥 ∈ ((𝐶(ball‘𝐷)𝑅) ∖ ran 𝑀))
115114ne0d 4283 . 2 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥) → ((𝐶(ball‘𝐷)𝑅) ∖ ran 𝑀) ≠ ∅)
11664, 115exlimddv 1937 1 (𝜑 → ((𝐶(ball‘𝐷)𝑅) ∖ ran 𝑀) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wex 1780  wcel 2105  wne 2940  wral 3061  wrex 3070  Vcvv 3441  cdif 3895  wss 3898  c0 4270  cop 4580   cuni 4853   class class class wbr 5093  {copab 5155   × cxp 5619  dom cdm 5621  ran crn 5622  ccom 5625  Fun wfun 6474   Fn wfn 6475  wf 6476  ontowfo 6478  cfv 6480  (class class class)co 7338  cmpo 7340  1st c1st 7898  2nd c2nd 7899  cr 10972  0cc0 10973  1c1 10974   + caddc 10976  *cxr 11110   < clt 11111   / cdiv 11734  cn 12075  +crp 12832  ∞Metcxmet 20689  Metcmet 20690  ballcbl 20691  MetOpencmopn 20694  Topctop 22149  Clsdccld 22274  clsccl 22276  𝑡clm 22484  Cauccau 24524  CMetccmet 24525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-cnex 11029  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049  ax-pre-mulgt0 11050  ax-pre-sup 11051
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-int 4896  df-iun 4944  df-iin 4945  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-riota 7294  df-ov 7341  df-oprab 7342  df-mpo 7343  df-om 7782  df-1st 7900  df-2nd 7901  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-er 8570  df-map 8689  df-pm 8690  df-en 8806  df-dom 8807  df-sdom 8808  df-sup 9300  df-inf 9301  df-pnf 11113  df-mnf 11114  df-xr 11115  df-ltxr 11116  df-le 11117  df-sub 11309  df-neg 11310  df-div 11735  df-nn 12076  df-2 12138  df-n0 12336  df-z 12422  df-uz 12685  df-q 12791  df-rp 12833  df-xneg 12950  df-xadd 12951  df-xmul 12952  df-ico 13187  df-rest 17231  df-topgen 17252  df-psmet 20696  df-xmet 20697  df-met 20698  df-bl 20699  df-mopn 20700  df-fbas 20701  df-fg 20702  df-top 22150  df-topon 22167  df-bases 22203  df-cld 22277  df-ntr 22278  df-cls 22279  df-nei 22356  df-lm 22487  df-fil 23104  df-fm 23196  df-flim 23197  df-flf 23198  df-cfil 24526  df-cau 24527  df-cmet 24528
This theorem is referenced by:  bcthlem5  24599
  Copyright terms: Public domain W3C validator