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

Theorem bcthlem4 23537
Description: Lemma for bcth 23539. 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 23496 . . . . . . 7 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
31, 2syl 17 . . . . . 6 (𝜑𝐷 ∈ (Met‘𝑋))
4 metxmet 22551 . . . . . 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 23535 . . . . 5 (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔𝑛)))
15 elrp 12143 . . . . . . . . 9 (𝑟 ∈ ℝ+ ↔ (𝑟 ∈ ℝ ∧ 0 < 𝑟))
16 nnrecl 11644 . . . . . . . . 9 ((𝑟 ∈ ℝ ∧ 0 < 𝑟) → ∃𝑚 ∈ ℕ (1 / 𝑚) < 𝑟)
1715, 16sylbi 209 . . . . . . . 8 (𝑟 ∈ ℝ+ → ∃𝑚 ∈ ℕ (1 / 𝑚) < 𝑟)
1817adantl 475 . . . . . . 7 ((𝜑𝑟 ∈ ℝ+) → ∃𝑚 ∈ ℕ (1 / 𝑚) < 𝑟)
19 peano2nn 11392 . . . . . . . . . 10 (𝑚 ∈ ℕ → (𝑚 + 1) ∈ ℕ)
2019adantl 475 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℕ)
21 fvoveq1 6947 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑚 → (𝑔‘(𝑘 + 1)) = (𝑔‘(𝑚 + 1)))
22 id 22 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑚𝑘 = 𝑚)
23 fveq2 6448 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑚 → (𝑔𝑘) = (𝑔𝑚))
2422, 23oveq12d 6942 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑚 → (𝑘𝐹(𝑔𝑘)) = (𝑚𝐹(𝑔𝑚)))
2521, 24eleq12d 2853 . . . . . . . . . . . . . . 15 (𝑘 = 𝑚 → ((𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔𝑘)) ↔ (𝑔‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑔𝑚))))
2625rspccva 3510 . . . . . . . . . . . . . 14 ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔𝑘)) ∧ 𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑔𝑚)))
2713, 26sylan 575 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑔𝑚)))
286ffvelrnda 6625 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (𝑔𝑚) ∈ (𝑋 × ℝ+))
297, 1, 8bcthlem1 23534 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔𝑚) ∈ (𝑋 × ℝ+))) → ((𝑔‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑔𝑚)) ↔ ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) ∧ (2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑚)) ∖ (𝑀𝑚)))))
3029expr 450 . . . . . . . . . . . . . 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 224 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) ∧ (2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑚)) ∖ (𝑀𝑚))))
3332simp2d 1134 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚))
3433adantlr 705 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚))
3532simp1d 1133 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+))
36 xp2nd 7480 . . . . . . . . . . . . . 14 ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) → (2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ+)
3735, 36syl 17 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ+)
3837rpred 12185 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ)
3938adantlr 705 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ)
40 nnrecre 11421 . . . . . . . . . . . 12 (𝑚 ∈ ℕ → (1 / 𝑚) ∈ ℝ)
4140adantl 475 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (1 / 𝑚) ∈ ℝ)
42 rpre 12149 . . . . . . . . . . . 12 (𝑟 ∈ ℝ+𝑟 ∈ ℝ)
4342ad2antlr 717 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → 𝑟 ∈ ℝ)
44 lttr 10455 . . . . . . . . . . 11 (((2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ ∧ (1 / 𝑚) ∈ ℝ ∧ 𝑟 ∈ ℝ) → (((2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚) ∧ (1 / 𝑚) < 𝑟) → (2nd ‘(𝑔‘(𝑚 + 1))) < 𝑟))
4539, 41, 43, 44syl3anc 1439 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (((2nd ‘(𝑔‘(𝑚 + 1))) < (1 / 𝑚) ∧ (1 / 𝑚) < 𝑟) → (2nd ‘(𝑔‘(𝑚 + 1))) < 𝑟))
4634, 45mpand 685 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → ((1 / 𝑚) < 𝑟 → (2nd ‘(𝑔‘(𝑚 + 1))) < 𝑟))
47 2fveq3 6453 . . . . . . . . . . 11 (𝑛 = (𝑚 + 1) → (2nd ‘(𝑔𝑛)) = (2nd ‘(𝑔‘(𝑚 + 1))))
4847breq1d 4898 . . . . . . . . . 10 (𝑛 = (𝑚 + 1) → ((2nd ‘(𝑔𝑛)) < 𝑟 ↔ (2nd ‘(𝑔‘(𝑚 + 1))) < 𝑟))
4948rspcev 3511 . . . . . . . . 9 (((𝑚 + 1) ∈ ℕ ∧ (2nd ‘(𝑔‘(𝑚 + 1))) < 𝑟) → ∃𝑛 ∈ ℕ (2nd ‘(𝑔𝑛)) < 𝑟)
5020, 46, 49syl6an 674 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → ((1 / 𝑚) < 𝑟 → ∃𝑛 ∈ ℕ (2nd ‘(𝑔𝑛)) < 𝑟))
5150rexlimdva 3213 . . . . . . 7 ((𝜑𝑟 ∈ ℝ+) → (∃𝑚 ∈ ℕ (1 / 𝑚) < 𝑟 → ∃𝑛 ∈ ℕ (2nd ‘(𝑔𝑛)) < 𝑟))
5218, 51mpd 15 . . . . . 6 ((𝜑𝑟 ∈ ℝ+) → ∃𝑛 ∈ ℕ (2nd ‘(𝑔𝑛)) < 𝑟)
5352ralrimiva 3148 . . . . 5 (𝜑 → ∀𝑟 ∈ ℝ+𝑛 ∈ ℕ (2nd ‘(𝑔𝑛)) < 𝑟)
545, 6, 14, 53caubl 23518 . . . 4 (𝜑 → (1st𝑔) ∈ (Cau‘𝐷))
557cmetcau 23499 . . . 4 ((𝐷 ∈ (CMet‘𝑋) ∧ (1st𝑔) ∈ (Cau‘𝐷)) → (1st𝑔) ∈ dom (⇝𝑡𝐽))
561, 54, 55syl2anc 579 . . 3 (𝜑 → (1st𝑔) ∈ dom (⇝𝑡𝐽))
57 fo1st 7467 . . . . . 6 1st :V–onto→V
58 fofun 6369 . . . . . 6 (1st :V–onto→V → Fun 1st )
5957, 58ax-mp 5 . . . . 5 Fun 1st
60 vex 3401 . . . . 5 𝑔 ∈ V
61 cofunexg 7411 . . . . 5 ((Fun 1st𝑔 ∈ V) → (1st𝑔) ∈ V)
6259, 60, 61mp2an 682 . . . 4 (1st𝑔) ∈ V
6362eldm 5568 . . 3 ((1st𝑔) ∈ dom (⇝𝑡𝐽) ↔ ∃𝑥(1st𝑔)(⇝𝑡𝐽)𝑥)
6456, 63sylib 210 . 2 (𝜑 → ∃𝑥(1st𝑔)(⇝𝑡𝐽)𝑥)
65 1nn 11391 . . . . . 6 1 ∈ ℕ
667, 1, 8, 9, 10, 11, 6, 12, 13bcthlem3 23536 . . . . . 6 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥 ∧ 1 ∈ ℕ) → 𝑥 ∈ ((ball‘𝐷)‘(𝑔‘1)))
6765, 66mp3an3 1523 . . . . 5 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥) → 𝑥 ∈ ((ball‘𝐷)‘(𝑔‘1)))
6812fveq2d 6452 . . . . . . 7 (𝜑 → ((ball‘𝐷)‘(𝑔‘1)) = ((ball‘𝐷)‘⟨𝐶, 𝑅⟩))
69 df-ov 6927 . . . . . . 7 (𝐶(ball‘𝐷)𝑅) = ((ball‘𝐷)‘⟨𝐶, 𝑅⟩)
7068, 69syl6eqr 2832 . . . . . 6 (𝜑 → ((ball‘𝐷)‘(𝑔‘1)) = (𝐶(ball‘𝐷)𝑅))
7170adantr 474 . . . . 5 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥) → ((ball‘𝐷)‘(𝑔‘1)) = (𝐶(ball‘𝐷)𝑅))
7267, 71eleqtrd 2861 . . . 4 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥) → 𝑥 ∈ (𝐶(ball‘𝐷)𝑅))
737mopntop 22657 . . . . . . . . . . . . . 14 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
745, 73syl 17 . . . . . . . . . . . . 13 (𝜑𝐽 ∈ Top)
7574adantr 474 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → 𝐽 ∈ Top)
765adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → 𝐷 ∈ (∞Met‘𝑋))
77 xp1st 7479 . . . . . . . . . . . . . . 15 ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) → (1st ‘(𝑔‘(𝑚 + 1))) ∈ 𝑋)
7835, 77syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝑔‘(𝑚 + 1))) ∈ 𝑋)
7937rpxrd 12186 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ*)
80 blssm 22635 . . . . . . . . . . . . . 14 ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔‘(𝑚 + 1))) ∈ 𝑋 ∧ (2nd ‘(𝑔‘(𝑚 + 1))) ∈ ℝ*) → ((1st ‘(𝑔‘(𝑚 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑚 + 1)))) ⊆ 𝑋)
8176, 78, 79, 80syl3anc 1439 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → ((1st ‘(𝑔‘(𝑚 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑚 + 1)))) ⊆ 𝑋)
82 1st2nd2 7486 . . . . . . . . . . . . . . . 16 ((𝑔‘(𝑚 + 1)) ∈ (𝑋 × ℝ+) → (𝑔‘(𝑚 + 1)) = ⟨(1st ‘(𝑔‘(𝑚 + 1))), (2nd ‘(𝑔‘(𝑚 + 1)))⟩)
8335, 82syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (𝑔‘(𝑚 + 1)) = ⟨(1st ‘(𝑔‘(𝑚 + 1))), (2nd ‘(𝑔‘(𝑚 + 1)))⟩)
8483fveq2d 6452 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) = ((ball‘𝐷)‘⟨(1st ‘(𝑔‘(𝑚 + 1))), (2nd ‘(𝑔‘(𝑚 + 1)))⟩))
85 df-ov 6927 . . . . . . . . . . . . . 14 ((1st ‘(𝑔‘(𝑚 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑚 + 1)))) = ((ball‘𝐷)‘⟨(1st ‘(𝑔‘(𝑚 + 1))), (2nd ‘(𝑔‘(𝑚 + 1)))⟩)
8684, 85syl6reqr 2833 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → ((1st ‘(𝑔‘(𝑚 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑚 + 1)))) = ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))))
877mopnuni 22658 . . . . . . . . . . . . . . 15 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
885, 87syl 17 . . . . . . . . . . . . . 14 (𝜑𝑋 = 𝐽)
8988adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → 𝑋 = 𝐽)
9081, 86, 893sstr3d 3866 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ 𝐽)
91 eqid 2778 . . . . . . . . . . . . 13 𝐽 = 𝐽
9291sscls 21272 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ 𝐽) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))))
9375, 90, 92syl2anc 579 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))))
9432simp3d 1135 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑚 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑚)) ∖ (𝑀𝑚)))
9593, 94sstrd 3831 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ (((ball‘𝐷)‘(𝑔𝑚)) ∖ (𝑀𝑚)))
96953adant2 1122 . . . . . . . . 9 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥𝑚 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))) ⊆ (((ball‘𝐷)‘(𝑔𝑚)) ∖ (𝑀𝑚)))
977, 1, 8, 9, 10, 11, 6, 12, 13bcthlem3 23536 . . . . . . . . . 10 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥 ∧ (𝑚 + 1) ∈ ℕ) → 𝑥 ∈ ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))))
9819, 97syl3an3 1166 . . . . . . . . 9 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥𝑚 ∈ ℕ) → 𝑥 ∈ ((ball‘𝐷)‘(𝑔‘(𝑚 + 1))))
9996, 98sseldd 3822 . . . . . . . 8 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥𝑚 ∈ ℕ) → 𝑥 ∈ (((ball‘𝐷)‘(𝑔𝑚)) ∖ (𝑀𝑚)))
10099eldifbd 3805 . . . . . . 7 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥𝑚 ∈ ℕ) → ¬ 𝑥 ∈ (𝑀𝑚))
1011003expa 1108 . . . . . 6 (((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥) ∧ 𝑚 ∈ ℕ) → ¬ 𝑥 ∈ (𝑀𝑚))
102101ralrimiva 3148 . . . . 5 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥) → ∀𝑚 ∈ ℕ ¬ 𝑥 ∈ (𝑀𝑚))
103 eluni2 4677 . . . . . . . . 9 (𝑥 ran 𝑀 ↔ ∃𝑦 ∈ ran 𝑀 𝑥𝑦)
1049ffnd 6294 . . . . . . . . . 10 (𝜑𝑀 Fn ℕ)
105 eleq2 2848 . . . . . . . . . . 11 (𝑦 = (𝑀𝑚) → (𝑥𝑦𝑥 ∈ (𝑀𝑚)))
106105rexrn 6627 . . . . . . . . . 10 (𝑀 Fn ℕ → (∃𝑦 ∈ ran 𝑀 𝑥𝑦 ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑀𝑚)))
107104, 106syl 17 . . . . . . . . 9 (𝜑 → (∃𝑦 ∈ ran 𝑀 𝑥𝑦 ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑀𝑚)))
108103, 107syl5bb 275 . . . . . . . 8 (𝜑 → (𝑥 ran 𝑀 ↔ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑀𝑚)))
109108notbid 310 . . . . . . 7 (𝜑 → (¬ 𝑥 ran 𝑀 ↔ ¬ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑀𝑚)))
110 ralnex 3174 . . . . . . 7 (∀𝑚 ∈ ℕ ¬ 𝑥 ∈ (𝑀𝑚) ↔ ¬ ∃𝑚 ∈ ℕ 𝑥 ∈ (𝑀𝑚))
111109, 110syl6bbr 281 . . . . . 6 (𝜑 → (¬ 𝑥 ran 𝑀 ↔ ∀𝑚 ∈ ℕ ¬ 𝑥 ∈ (𝑀𝑚)))
112111biimpar 471 . . . . 5 ((𝜑 ∧ ∀𝑚 ∈ ℕ ¬ 𝑥 ∈ (𝑀𝑚)) → ¬ 𝑥 ran 𝑀)
113102, 112syldan 585 . . . 4 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥) → ¬ 𝑥 ran 𝑀)
11472, 113eldifd 3803 . . 3 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥) → 𝑥 ∈ ((𝐶(ball‘𝐷)𝑅) ∖ ran 𝑀))
115114ne0d 4150 . 2 ((𝜑 ∧ (1st𝑔)(⇝𝑡𝐽)𝑥) → ((𝐶(ball‘𝐷)𝑅) ∖ ran 𝑀) ≠ ∅)
11664, 115exlimddv 1978 1 (𝜑 → ((𝐶(ball‘𝐷)𝑅) ∖ ran 𝑀) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  w3a 1071   = wceq 1601  wex 1823  wcel 2107  wne 2969  wral 3090  wrex 3091  Vcvv 3398  cdif 3789  wss 3792  c0 4141  cop 4404   cuni 4673   class class class wbr 4888  {copab 4950   × cxp 5355  dom cdm 5357  ran crn 5358  ccom 5361  Fun wfun 6131   Fn wfn 6132  wf 6133  ontowfo 6135  cfv 6137  (class class class)co 6924  cmpt2 6926  1st c1st 7445  2nd c2nd 7446  cr 10273  0cc0 10274  1c1 10275   + caddc 10277  *cxr 10412   < clt 10413   / cdiv 11034  cn 11378  +crp 12141  ∞Metcxmet 20131  Metcmet 20132  ballcbl 20133  MetOpencmopn 20136  Topctop 21109  Clsdccld 21232  clsccl 21234  𝑡clm 21442  Cauccau 23463  CMetccmet 23464
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351  ax-pre-sup 10352
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-iin 4758  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-om 7346  df-1st 7447  df-2nd 7448  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-er 8028  df-map 8144  df-pm 8145  df-en 8244  df-dom 8245  df-sdom 8246  df-sup 8638  df-inf 8639  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11035  df-nn 11379  df-2 11442  df-n0 11647  df-z 11733  df-uz 11997  df-q 12100  df-rp 12142  df-xneg 12261  df-xadd 12262  df-xmul 12263  df-ico 12497  df-rest 16473  df-topgen 16494  df-psmet 20138  df-xmet 20139  df-met 20140  df-bl 20141  df-mopn 20142  df-fbas 20143  df-fg 20144  df-top 21110  df-topon 21127  df-bases 21162  df-cld 21235  df-ntr 21236  df-cls 21237  df-nei 21314  df-lm 21445  df-fil 22062  df-fm 22154  df-flim 22155  df-flf 22156  df-cfil 23465  df-cau 23466  df-cmet 23467
This theorem is referenced by:  bcthlem5  23538
  Copyright terms: Public domain W3C validator