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

Theorem bcthlem5 25381
Description: Lemma for bcth 25382. The proof makes essential use of the Axiom of Dependent Choice axdc4uz 14035, which in the form used here accepts a "selection" function 𝐹 from each element of 𝐾 to a nonempty subset of 𝐾, and the result function 𝑔 maps 𝑔(𝑛 + 1) to an element of 𝐹(𝑛, 𝑔(𝑛)). The trick here is thus in the choice of 𝐹 and 𝐾: we let 𝐾 be the set of all tagged nonempty open sets (tagged here meaning that we have a point and an open set, in an ordered pair), and 𝐹(𝑘, ⟨𝑥, 𝑧⟩) gives the set of all balls of size less than 1 / 𝑘, tagged by their centers, whose closures fit within the given open set 𝑧 and miss 𝑀(𝑘).

Since 𝑀(𝑘) is closed, 𝑧𝑀(𝑘) is open and also nonempty, since 𝑧 is nonempty and 𝑀(𝑘) has empty interior. Then there is some ball contained in it, and hence our function 𝐹 is valid (it never maps to the empty set). Now starting at a point in the interior of ran 𝑀, DC gives us the function 𝑔 all whose elements are constrained by 𝐹 acting on the previous value. (This is all proven in this lemma.) Now 𝑔 is a sequence of tagged open balls, forming an inclusion chain (see bcthlem2 25378) and whose sizes tend to zero, since they are bounded above by 1 / 𝑘. Thus, the centers of these balls form a Cauchy sequence, and converge to a point 𝑥 (see bcthlem4 25380). Since the inclusion chain also ensures the closure of each ball is in the previous ball, the point 𝑥 must be in all these balls (see bcthlem3 25379) and hence misses each 𝑀(𝑘), contradicting the fact that 𝑥 is in the interior of ran 𝑀 (which was the starting point). (Contributed by Mario Carneiro, 6-Jan-2014.)

Hypotheses
Ref Expression
bcth.2 𝐽 = (MetOpen‘𝐷)
bcthlem.4 (𝜑𝐷 ∈ (CMet‘𝑋))
bcthlem.5 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))})
bcthlem.6 (𝜑𝑀:ℕ⟶(Clsd‘𝐽))
bcthlem5.7 (𝜑 → ∀𝑘 ∈ ℕ ((int‘𝐽)‘(𝑀𝑘)) = ∅)
Assertion
Ref Expression
bcthlem5 (𝜑 → ((int‘𝐽)‘ ran 𝑀) = ∅)
Distinct variable groups:   𝑘,𝑟,𝑥,𝑧,𝐷   𝑘,𝐹,𝑟,𝑥,𝑧   𝑘,𝐽,𝑟,𝑥,𝑧   𝑘,𝑀,𝑟,𝑥,𝑧   𝜑,𝑘,𝑟,𝑥,𝑧   𝑘,𝑋,𝑟,𝑥,𝑧

Proof of Theorem bcthlem5
Dummy variables 𝑛 𝑔 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bcthlem.4 . . . . . 6 (𝜑𝐷 ∈ (CMet‘𝑋))
2 cmetmet 25339 . . . . . 6 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
3 metxmet 24365 . . . . . 6 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
41, 2, 33syl 18 . . . . 5 (𝜑𝐷 ∈ (∞Met‘𝑋))
5 bcth.2 . . . . . . . 8 𝐽 = (MetOpen‘𝐷)
65mopntop 24471 . . . . . . 7 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
74, 6syl 17 . . . . . 6 (𝜑𝐽 ∈ Top)
8 bcthlem.6 . . . . . . . . 9 (𝜑𝑀:ℕ⟶(Clsd‘𝐽))
98frnd 6755 . . . . . . . 8 (𝜑 → ran 𝑀 ⊆ (Clsd‘𝐽))
10 eqid 2740 . . . . . . . . 9 𝐽 = 𝐽
1110cldss2 23059 . . . . . . . 8 (Clsd‘𝐽) ⊆ 𝒫 𝐽
129, 11sstrdi 4021 . . . . . . 7 (𝜑 → ran 𝑀 ⊆ 𝒫 𝐽)
13 sspwuni 5123 . . . . . . 7 (ran 𝑀 ⊆ 𝒫 𝐽 ran 𝑀 𝐽)
1412, 13sylib 218 . . . . . 6 (𝜑 ran 𝑀 𝐽)
1510ntropn 23078 . . . . . 6 ((𝐽 ∈ Top ∧ ran 𝑀 𝐽) → ((int‘𝐽)‘ ran 𝑀) ∈ 𝐽)
167, 14, 15syl2anc 583 . . . . 5 (𝜑 → ((int‘𝐽)‘ ran 𝑀) ∈ 𝐽)
174, 16jca 511 . . . 4 (𝜑 → (𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘ ran 𝑀) ∈ 𝐽))
185mopni2 24527 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘ ran 𝑀) ∈ 𝐽𝑛 ∈ ((int‘𝐽)‘ ran 𝑀)) → ∃𝑚 ∈ ℝ+ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀))
19183expa 1118 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘ ran 𝑀) ∈ 𝐽) ∧ 𝑛 ∈ ((int‘𝐽)‘ ran 𝑀)) → ∃𝑚 ∈ ℝ+ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀))
2017, 19sylan 579 . . 3 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀)) → ∃𝑚 ∈ ℝ+ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀))
215mopnuni 24472 . . . . . . . . . . . 12 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
224, 21syl 17 . . . . . . . . . . 11 (𝜑𝑋 = 𝐽)
2310topopn 22933 . . . . . . . . . . . 12 (𝐽 ∈ Top → 𝐽𝐽)
247, 23syl 17 . . . . . . . . . . 11 (𝜑 𝐽𝐽)
2522, 24eqeltrd 2844 . . . . . . . . . 10 (𝜑𝑋𝐽)
26 reex 11275 . . . . . . . . . . 11 ℝ ∈ V
27 rpssre 13064 . . . . . . . . . . 11 + ⊆ ℝ
2826, 27ssexi 5340 . . . . . . . . . 10 + ∈ V
29 xpexg 7785 . . . . . . . . . 10 ((𝑋𝐽 ∧ ℝ+ ∈ V) → (𝑋 × ℝ+) ∈ V)
3025, 28, 29sylancl 585 . . . . . . . . 9 (𝜑 → (𝑋 × ℝ+) ∈ V)
31303ad2ant1 1133 . . . . . . . 8 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → (𝑋 × ℝ+) ∈ V)
3210ntrss3 23089 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ran 𝑀 𝐽) → ((int‘𝐽)‘ ran 𝑀) ⊆ 𝐽)
337, 14, 32syl2anc 583 . . . . . . . . . . . 12 (𝜑 → ((int‘𝐽)‘ ran 𝑀) ⊆ 𝐽)
3433, 22sseqtrrd 4050 . . . . . . . . . . 11 (𝜑 → ((int‘𝐽)‘ ran 𝑀) ⊆ 𝑋)
35343ad2ant1 1133 . . . . . . . . . 10 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → ((int‘𝐽)‘ ran 𝑀) ⊆ 𝑋)
36 simp2 1137 . . . . . . . . . 10 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → 𝑛 ∈ ((int‘𝐽)‘ ran 𝑀))
3735, 36sseldd 4009 . . . . . . . . 9 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → 𝑛𝑋)
38 simp3 1138 . . . . . . . . 9 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → 𝑚 ∈ ℝ+)
3937, 38opelxpd 5739 . . . . . . . 8 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → ⟨𝑛, 𝑚⟩ ∈ (𝑋 × ℝ+))
40 opabssxp 5792 . . . . . . . . . . . . 13 {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ⊆ (𝑋 × ℝ+)
41 elpw2g 5351 . . . . . . . . . . . . . . 15 ((𝑋 × ℝ+) ∈ V → ({⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ 𝒫 (𝑋 × ℝ+) ↔ {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ⊆ (𝑋 × ℝ+)))
4230, 41syl 17 . . . . . . . . . . . . . 14 (𝜑 → ({⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ 𝒫 (𝑋 × ℝ+) ↔ {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ⊆ (𝑋 × ℝ+)))
4342adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ({⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ 𝒫 (𝑋 × ℝ+) ↔ {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ⊆ (𝑋 × ℝ+)))
4440, 43mpbiri 258 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ 𝒫 (𝑋 × ℝ+))
45 bcthlem5.7 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑘 ∈ ℕ ((int‘𝐽)‘(𝑀𝑘)) = ∅)
46 simpl 482 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) → 𝑘 ∈ ℕ)
47 rspa 3254 . . . . . . . . . . . . . . . 16 ((∀𝑘 ∈ ℕ ((int‘𝐽)‘(𝑀𝑘)) = ∅ ∧ 𝑘 ∈ ℕ) → ((int‘𝐽)‘(𝑀𝑘)) = ∅)
4845, 46, 47syl2an 595 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((int‘𝐽)‘(𝑀𝑘)) = ∅)
49 ssdif0 4389 . . . . . . . . . . . . . . . . 17 (((ball‘𝐷)‘𝑧) ⊆ (𝑀𝑘) ↔ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) = ∅)
50 1st2nd2 8069 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝑋 × ℝ+) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
5150ad2antll 728 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
5251fveq2d 6924 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) = ((ball‘𝐷)‘⟨(1st𝑧), (2nd𝑧)⟩))
53 df-ov 7451 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑧)(ball‘𝐷)(2nd𝑧)) = ((ball‘𝐷)‘⟨(1st𝑧), (2nd𝑧)⟩)
5452, 53eqtr4di 2798 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) = ((1st𝑧)(ball‘𝐷)(2nd𝑧)))
554adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → 𝐷 ∈ (∞Met‘𝑋))
56 xp1st 8062 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ (𝑋 × ℝ+) → (1st𝑧) ∈ 𝑋)
5756ad2antll 728 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (1st𝑧) ∈ 𝑋)
58 xp2nd 8063 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ (𝑋 × ℝ+) → (2nd𝑧) ∈ ℝ+)
5958ad2antll 728 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (2nd𝑧) ∈ ℝ+)
60 bln0 24446 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st𝑧) ∈ 𝑋 ∧ (2nd𝑧) ∈ ℝ+) → ((1st𝑧)(ball‘𝐷)(2nd𝑧)) ≠ ∅)
6155, 57, 59, 60syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((1st𝑧)(ball‘𝐷)(2nd𝑧)) ≠ ∅)
6254, 61eqnetrd 3014 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) ≠ ∅)
637adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → 𝐽 ∈ Top)
64 ffvelcdm 7115 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀:ℕ⟶(Clsd‘𝐽) ∧ 𝑘 ∈ ℕ) → (𝑀𝑘) ∈ (Clsd‘𝐽))
658, 46, 64syl2an 595 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑀𝑘) ∈ (Clsd‘𝐽))
6610cldss 23058 . . . . . . . . . . . . . . . . . . . 20 ((𝑀𝑘) ∈ (Clsd‘𝐽) → (𝑀𝑘) ⊆ 𝐽)
6765, 66syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑀𝑘) ⊆ 𝐽)
6859rpxrd 13100 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (2nd𝑧) ∈ ℝ*)
695blopn 24534 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st𝑧) ∈ 𝑋 ∧ (2nd𝑧) ∈ ℝ*) → ((1st𝑧)(ball‘𝐷)(2nd𝑧)) ∈ 𝐽)
7055, 57, 68, 69syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((1st𝑧)(ball‘𝐷)(2nd𝑧)) ∈ 𝐽)
7154, 70eqeltrd 2844 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) ∈ 𝐽)
7210ssntr 23087 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ Top ∧ (𝑀𝑘) ⊆ 𝐽) ∧ (((ball‘𝐷)‘𝑧) ∈ 𝐽 ∧ ((ball‘𝐷)‘𝑧) ⊆ (𝑀𝑘))) → ((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀𝑘)))
7372expr 456 . . . . . . . . . . . . . . . . . . 19 (((𝐽 ∈ Top ∧ (𝑀𝑘) ⊆ 𝐽) ∧ ((ball‘𝐷)‘𝑧) ∈ 𝐽) → (((ball‘𝐷)‘𝑧) ⊆ (𝑀𝑘) → ((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀𝑘))))
7463, 67, 71, 73syl21anc 837 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((ball‘𝐷)‘𝑧) ⊆ (𝑀𝑘) → ((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀𝑘))))
75 ssn0 4427 . . . . . . . . . . . . . . . . . . 19 ((((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀𝑘)) ∧ ((ball‘𝐷)‘𝑧) ≠ ∅) → ((int‘𝐽)‘(𝑀𝑘)) ≠ ∅)
7675expcom 413 . . . . . . . . . . . . . . . . . 18 (((ball‘𝐷)‘𝑧) ≠ ∅ → (((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀𝑘)) → ((int‘𝐽)‘(𝑀𝑘)) ≠ ∅))
7762, 74, 76sylsyld 61 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((ball‘𝐷)‘𝑧) ⊆ (𝑀𝑘) → ((int‘𝐽)‘(𝑀𝑘)) ≠ ∅))
7849, 77biimtrrid 243 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) = ∅ → ((int‘𝐽)‘(𝑀𝑘)) ≠ ∅))
7978necon2d 2969 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((int‘𝐽)‘(𝑀𝑘)) = ∅ → (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ≠ ∅))
8048, 79mpd 15 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ≠ ∅)
81 n0 4376 . . . . . . . . . . . . . . 15 ((((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))
8243ad2ant1 1133 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → 𝐷 ∈ (∞Met‘𝑋))
8310difopn 23063 . . . . . . . . . . . . . . . . . . . . 21 ((((ball‘𝐷)‘𝑧) ∈ 𝐽 ∧ (𝑀𝑘) ∈ (Clsd‘𝐽)) → (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ∈ 𝐽)
8471, 65, 83syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ∈ 𝐽)
85843adant3 1132 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ∈ 𝐽)
86 simp3 1138 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))
87 simp2l 1199 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → 𝑘 ∈ ℕ)
88 nnrp 13068 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
8988rpreccld 13109 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
9087, 89syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → (1 / 𝑘) ∈ ℝ+)
915mopni3 24528 . . . . . . . . . . . . . . . . . . 19 (((𝐷 ∈ (∞Met‘𝑋) ∧ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ∈ 𝐽𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) ∧ (1 / 𝑘) ∈ ℝ+) → ∃𝑛 ∈ ℝ+ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))
9282, 85, 86, 90, 91syl31anc 1373 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → ∃𝑛 ∈ ℝ+ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))
93 simp1 1136 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → 𝜑)
94 elssuni 4961 . . . . . . . . . . . . . . . . . . . . . . . 24 (((ball‘𝐷)‘𝑧) ∈ 𝐽 → ((ball‘𝐷)‘𝑧) ⊆ 𝐽)
9571, 94syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) ⊆ 𝐽)
9622adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → 𝑋 = 𝐽)
9795, 96sseqtrrd 4050 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) ⊆ 𝑋)
9897ssdifssd 4170 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ⊆ 𝑋)
9998sseld 4007 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) → 𝑥𝑋))
100993impia 1117 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → 𝑥𝑋)
101 simp2 1137 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)))
102 rphalfcl 13084 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℝ+ → (𝑛 / 2) ∈ ℝ+)
103 rphalflt 13086 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℝ+ → (𝑛 / 2) < 𝑛)
104 breq1 5169 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑟 = (𝑛 / 2) → (𝑟 < 𝑛 ↔ (𝑛 / 2) < 𝑛))
105104rspcev 3635 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 / 2) ∈ ℝ+ ∧ (𝑛 / 2) < 𝑛) → ∃𝑟 ∈ ℝ+ 𝑟 < 𝑛)
106102, 103, 105syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℝ+ → ∃𝑟 ∈ ℝ+ 𝑟 < 𝑛)
107106ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) ∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))) → ∃𝑟 ∈ ℝ+ 𝑟 < 𝑛)
108 df-rex 3077 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑟 ∈ ℝ+ 𝑟 < 𝑛 ↔ ∃𝑟(𝑟 ∈ ℝ+𝑟 < 𝑛))
109 simpr3 1196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → 𝑟 ∈ ℝ+)
110109rpred 13099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → 𝑟 ∈ ℝ)
111 simpr1 1194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → 𝑛 ∈ ℝ+)
112111rpred 13099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → 𝑛 ∈ ℝ)
113 simplrl 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → 𝑘 ∈ ℕ)
114113nnrecred 12344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → (1 / 𝑘) ∈ ℝ)
115 simpr2 1195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → 𝑟 < 𝑛)
116 lttr 11366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑟 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (1 / 𝑘) ∈ ℝ) → ((𝑟 < 𝑛𝑛 < (1 / 𝑘)) → 𝑟 < (1 / 𝑘)))
117116expdimp 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑟 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (1 / 𝑘) ∈ ℝ) ∧ 𝑟 < 𝑛) → (𝑛 < (1 / 𝑘) → 𝑟 < (1 / 𝑘)))
118110, 112, 114, 115, 117syl31anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → (𝑛 < (1 / 𝑘) → 𝑟 < (1 / 𝑘)))
1194anim1i 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑥𝑋) → (𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋))
120119adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋))
121 rpxr 13066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
122 rpxr 13066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 ∈ ℝ+𝑛 ∈ ℝ*)
123 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑟 < 𝑛𝑟 < 𝑛)
124121, 122, 1233anim123i 1151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑟 ∈ ℝ+𝑛 ∈ ℝ+𝑟 < 𝑛) → (𝑟 ∈ ℝ*𝑛 ∈ ℝ*𝑟 < 𝑛))
1251243coml 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+) → (𝑟 ∈ ℝ*𝑛 ∈ ℝ*𝑟 < 𝑛))
1265blsscls 24541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑟 ∈ ℝ*𝑛 ∈ ℝ*𝑟 < 𝑛)) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (𝑥(ball‘𝐷)𝑛))
127120, 125, 126syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (𝑥(ball‘𝐷)𝑛))
128 sstr2 4015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (𝑥(ball‘𝐷)𝑛) → ((𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))
129127, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → ((𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))
130118, 129anim12d 608 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))))
131 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → 𝑥𝑋)
132131, 109jca 511 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → (𝑥𝑋𝑟 ∈ ℝ+))
133130, 132jctild 525 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
1341333exp2 1354 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑛 ∈ ℝ+ → (𝑟 < 𝑛 → (𝑟 ∈ ℝ+ → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))))))))
135134com35 98 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑛 ∈ ℝ+ → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → (𝑟 ∈ ℝ+ → (𝑟 < 𝑛 → ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))))))))
136135imp5d 439 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) ∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))) → ((𝑟 ∈ ℝ+𝑟 < 𝑛) → ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
137136eximdv 1916 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) ∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))) → (∃𝑟(𝑟 ∈ ℝ+𝑟 < 𝑛) → ∃𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
138108, 137biimtrid 242 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) ∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))) → (∃𝑟 ∈ ℝ+ 𝑟 < 𝑛 → ∃𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
139107, 138mpd 15 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) ∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))) → ∃𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))))
140139rexlimdva2 3163 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (∃𝑛 ∈ ℝ+ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → ∃𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
14193, 100, 101, 140syl21anc 837 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → (∃𝑛 ∈ ℝ+ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → ∃𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
14292, 141mpd 15 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → ∃𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))))
1431423expia 1121 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) → ∃𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
144143eximdv 1916 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (∃𝑥 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) → ∃𝑥𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
14581, 144biimtrid 242 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ≠ ∅ → ∃𝑥𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
14680, 145mpd 15 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ∃𝑥𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))))
147 opabn0 5572 . . . . . . . . . . . . 13 ({⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ≠ ∅ ↔ ∃𝑥𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))))
148146, 147sylibr 234 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ≠ ∅)
149 eldifsn 4811 . . . . . . . . . . . 12 ({⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ (𝒫 (𝑋 × ℝ+) ∖ {∅}) ↔ ({⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ 𝒫 (𝑋 × ℝ+) ∧ {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ≠ ∅))
15044, 148, 149sylanbrc 582 . . . . . . . . . . 11 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ (𝒫 (𝑋 × ℝ+) ∖ {∅}))
151150ralrimivva 3208 . . . . . . . . . 10 (𝜑 → ∀𝑘 ∈ ℕ ∀𝑧 ∈ (𝑋 × ℝ+){⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ (𝒫 (𝑋 × ℝ+) ∖ {∅}))
152 bcthlem.5 . . . . . . . . . . 11 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))})
153152fmpo 8109 . . . . . . . . . 10 (∀𝑘 ∈ ℕ ∀𝑧 ∈ (𝑋 × ℝ+){⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ (𝒫 (𝑋 × ℝ+) ∖ {∅}) ↔ 𝐹:(ℕ × (𝑋 × ℝ+))⟶(𝒫 (𝑋 × ℝ+) ∖ {∅}))
154151, 153sylib 218 . . . . . . . . 9 (𝜑𝐹:(ℕ × (𝑋 × ℝ+))⟶(𝒫 (𝑋 × ℝ+) ∖ {∅}))
1551543ad2ant1 1133 . . . . . . . 8 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → 𝐹:(ℕ × (𝑋 × ℝ+))⟶(𝒫 (𝑋 × ℝ+) ∖ {∅}))
156 1z 12673 . . . . . . . . 9 1 ∈ ℤ
157 nnuz 12946 . . . . . . . . 9 ℕ = (ℤ‘1)
158156, 157axdc4uz 14035 . . . . . . . 8 (((𝑋 × ℝ+) ∈ V ∧ ⟨𝑛, 𝑚⟩ ∈ (𝑋 × ℝ+) ∧ 𝐹:(ℕ × (𝑋 × ℝ+))⟶(𝒫 (𝑋 × ℝ+) ∖ {∅})) → ∃𝑔(𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛))))
15931, 39, 155, 158syl3anc 1371 . . . . . . 7 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → ∃𝑔(𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛))))
160 simpl1 1191 . . . . . . . . 9 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → 𝜑)
161160, 1syl 17 . . . . . . . 8 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → 𝐷 ∈ (CMet‘𝑋))
162160, 8syl 17 . . . . . . . 8 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → 𝑀:ℕ⟶(Clsd‘𝐽))
163 simpl3 1193 . . . . . . . 8 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → 𝑚 ∈ ℝ+)
16437adantr 480 . . . . . . . 8 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → 𝑛𝑋)
165 simpr1 1194 . . . . . . . 8 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → 𝑔:ℕ⟶(𝑋 × ℝ+))
166 simpr2 1195 . . . . . . . 8 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → (𝑔‘1) = ⟨𝑛, 𝑚⟩)
167 simpr3 1196 . . . . . . . . 9 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))
168 fvoveq1 7471 . . . . . . . . . . 11 (𝑛 = 𝑘 → (𝑔‘(𝑛 + 1)) = (𝑔‘(𝑘 + 1)))
169 id 22 . . . . . . . . . . . 12 (𝑛 = 𝑘𝑛 = 𝑘)
170 fveq2 6920 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝑔𝑛) = (𝑔𝑘))
171169, 170oveq12d 7466 . . . . . . . . . . 11 (𝑛 = 𝑘 → (𝑛𝐹(𝑔𝑛)) = (𝑘𝐹(𝑔𝑘)))
172168, 171eleq12d 2838 . . . . . . . . . 10 (𝑛 = 𝑘 → ((𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)) ↔ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔𝑘))))
173172cbvralvw 3243 . . . . . . . . 9 (∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)) ↔ ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔𝑘)))
174167, 173sylib 218 . . . . . . . 8 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔𝑘)))
1755, 161, 152, 162, 163, 164, 165, 166, 174bcthlem4 25380 . . . . . . 7 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → ((𝑛(ball‘𝐷)𝑚) ∖ ran 𝑀) ≠ ∅)
176159, 175exlimddv 1934 . . . . . 6 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → ((𝑛(ball‘𝐷)𝑚) ∖ ran 𝑀) ≠ ∅)
17710ntrss2 23086 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ ran 𝑀 𝐽) → ((int‘𝐽)‘ ran 𝑀) ⊆ ran 𝑀)
1787, 14, 177syl2anc 583 . . . . . . . . . 10 (𝜑 → ((int‘𝐽)‘ ran 𝑀) ⊆ ran 𝑀)
179 sstr2 4015 . . . . . . . . . 10 ((𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀) → (((int‘𝐽)‘ ran 𝑀) ⊆ ran 𝑀 → (𝑛(ball‘𝐷)𝑚) ⊆ ran 𝑀))
180178, 179syl5com 31 . . . . . . . . 9 (𝜑 → ((𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀) → (𝑛(ball‘𝐷)𝑚) ⊆ ran 𝑀))
181 ssdif0 4389 . . . . . . . . 9 ((𝑛(ball‘𝐷)𝑚) ⊆ ran 𝑀 ↔ ((𝑛(ball‘𝐷)𝑚) ∖ ran 𝑀) = ∅)
182180, 181imbitrdi 251 . . . . . . . 8 (𝜑 → ((𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀) → ((𝑛(ball‘𝐷)𝑚) ∖ ran 𝑀) = ∅))
183182necon3ad 2959 . . . . . . 7 (𝜑 → (((𝑛(ball‘𝐷)𝑚) ∖ ran 𝑀) ≠ ∅ → ¬ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀)))
1841833ad2ant1 1133 . . . . . 6 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → (((𝑛(ball‘𝐷)𝑚) ∖ ran 𝑀) ≠ ∅ → ¬ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀)))
185176, 184mpd 15 . . . . 5 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → ¬ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀))
1861853expa 1118 . . . 4 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀)) ∧ 𝑚 ∈ ℝ+) → ¬ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀))
187186nrexdv 3155 . . 3 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀)) → ¬ ∃𝑚 ∈ ℝ+ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀))
18820, 187pm2.65da 816 . 2 (𝜑 → ¬ 𝑛 ∈ ((int‘𝐽)‘ ran 𝑀))
189188eq0rdv 4430 1 (𝜑 → ((int‘𝐽)‘ ran 𝑀) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087   = wceq 1537  wex 1777  wcel 2108  wne 2946  wral 3067  wrex 3076  Vcvv 3488  cdif 3973  wss 3976  c0 4352  𝒫 cpw 4622  {csn 4648  cop 4654   cuni 4931   class class class wbr 5166  {copab 5228   × cxp 5698  ran crn 5701  wf 6569  cfv 6573  (class class class)co 7448  cmpo 7450  1st c1st 8028  2nd c2nd 8029  cr 11183  1c1 11185   + caddc 11187  *cxr 11323   < clt 11324   / cdiv 11947  cn 12293  2c2 12348  +crp 13057  ∞Metcxmet 21372  Metcmet 21373  ballcbl 21374  MetOpencmopn 21377  Topctop 22920  Clsdccld 23045  intcnt 23046  clsccl 23047  CMetccmet 25307
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-inf2 9710  ax-dc 10515  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-iin 5018  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-er 8763  df-map 8886  df-pm 8887  df-en 9004  df-dom 9005  df-sdom 9006  df-sup 9511  df-inf 9512  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-n0 12554  df-z 12640  df-uz 12904  df-q 13014  df-rp 13058  df-xneg 13175  df-xadd 13176  df-xmul 13177  df-ico 13413  df-rest 17482  df-topgen 17503  df-psmet 21379  df-xmet 21380  df-met 21381  df-bl 21382  df-mopn 21383  df-fbas 21384  df-fg 21385  df-top 22921  df-topon 22938  df-bases 22974  df-cld 23048  df-ntr 23049  df-cls 23050  df-nei 23127  df-lm 23258  df-fil 23875  df-fm 23967  df-flim 23968  df-flf 23969  df-cfil 25308  df-cau 25309  df-cmet 25310
This theorem is referenced by:  bcth  25382
  Copyright terms: Public domain W3C validator