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

Theorem bcthlem5 22933
 Description: Lemma for bcth 22934. The proof makes essential use of the Axiom of Dependent Choice axdc4uz 12645, 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 22930) 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 22932). 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 22931) 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 22892 . . . . . 6 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
3 metxmet 21949 . . . . . 6 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
41, 2, 33syl 18 . . . . 5 (𝜑𝐷 ∈ (∞Met‘𝑋))
5 bcth.2 . . . . . . . 8 𝐽 = (MetOpen‘𝐷)
65mopntop 22055 . . . . . . 7 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
74, 6syl 17 . . . . . 6 (𝜑𝐽 ∈ Top)
8 bcthlem.6 . . . . . . . . 9 (𝜑𝑀:ℕ⟶(Clsd‘𝐽))
9 frn 5966 . . . . . . . . 9 (𝑀:ℕ⟶(Clsd‘𝐽) → ran 𝑀 ⊆ (Clsd‘𝐽))
108, 9syl 17 . . . . . . . 8 (𝜑 → ran 𝑀 ⊆ (Clsd‘𝐽))
11 eqid 2610 . . . . . . . . 9 𝐽 = 𝐽
1211cldss2 20644 . . . . . . . 8 (Clsd‘𝐽) ⊆ 𝒫 𝐽
1310, 12syl6ss 3580 . . . . . . 7 (𝜑 → ran 𝑀 ⊆ 𝒫 𝐽)
14 sspwuni 4547 . . . . . . 7 (ran 𝑀 ⊆ 𝒫 𝐽 ran 𝑀 𝐽)
1513, 14sylib 207 . . . . . 6 (𝜑 ran 𝑀 𝐽)
1611ntropn 20663 . . . . . 6 ((𝐽 ∈ Top ∧ ran 𝑀 𝐽) → ((int‘𝐽)‘ ran 𝑀) ∈ 𝐽)
177, 15, 16syl2anc 691 . . . . 5 (𝜑 → ((int‘𝐽)‘ ran 𝑀) ∈ 𝐽)
184, 17jca 553 . . . 4 (𝜑 → (𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘ ran 𝑀) ∈ 𝐽))
195mopni2 22108 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘ ran 𝑀) ∈ 𝐽𝑛 ∈ ((int‘𝐽)‘ ran 𝑀)) → ∃𝑚 ∈ ℝ+ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀))
20193expa 1257 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘ ran 𝑀) ∈ 𝐽) ∧ 𝑛 ∈ ((int‘𝐽)‘ ran 𝑀)) → ∃𝑚 ∈ ℝ+ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀))
2118, 20sylan 487 . . 3 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀)) → ∃𝑚 ∈ ℝ+ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀))
225mopnuni 22056 . . . . . . . . . . . 12 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
234, 22syl 17 . . . . . . . . . . 11 (𝜑𝑋 = 𝐽)
2411topopn 20536 . . . . . . . . . . . 12 (𝐽 ∈ Top → 𝐽𝐽)
257, 24syl 17 . . . . . . . . . . 11 (𝜑 𝐽𝐽)
2623, 25eqeltrd 2688 . . . . . . . . . 10 (𝜑𝑋𝐽)
27 reex 9906 . . . . . . . . . . 11 ℝ ∈ V
28 rpssre 11719 . . . . . . . . . . 11 + ⊆ ℝ
2927, 28ssexi 4731 . . . . . . . . . 10 + ∈ V
30 xpexg 6858 . . . . . . . . . 10 ((𝑋𝐽 ∧ ℝ+ ∈ V) → (𝑋 × ℝ+) ∈ V)
3126, 29, 30sylancl 693 . . . . . . . . 9 (𝜑 → (𝑋 × ℝ+) ∈ V)
32313ad2ant1 1075 . . . . . . . 8 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → (𝑋 × ℝ+) ∈ V)
3311ntrss3 20674 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ran 𝑀 𝐽) → ((int‘𝐽)‘ ran 𝑀) ⊆ 𝐽)
347, 15, 33syl2anc 691 . . . . . . . . . . . 12 (𝜑 → ((int‘𝐽)‘ ran 𝑀) ⊆ 𝐽)
3534, 23sseqtr4d 3605 . . . . . . . . . . 11 (𝜑 → ((int‘𝐽)‘ ran 𝑀) ⊆ 𝑋)
36353ad2ant1 1075 . . . . . . . . . 10 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → ((int‘𝐽)‘ ran 𝑀) ⊆ 𝑋)
37 simp2 1055 . . . . . . . . . 10 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → 𝑛 ∈ ((int‘𝐽)‘ ran 𝑀))
3836, 37sseldd 3569 . . . . . . . . 9 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → 𝑛𝑋)
39 simp3 1056 . . . . . . . . 9 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → 𝑚 ∈ ℝ+)
40 opelxpi 5072 . . . . . . . . 9 ((𝑛𝑋𝑚 ∈ ℝ+) → ⟨𝑛, 𝑚⟩ ∈ (𝑋 × ℝ+))
4138, 39, 40syl2anc 691 . . . . . . . 8 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → ⟨𝑛, 𝑚⟩ ∈ (𝑋 × ℝ+))
42 opabssxp 5116 . . . . . . . . . . . . 13 {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ⊆ (𝑋 × ℝ+)
43 elpw2g 4754 . . . . . . . . . . . . . . 15 ((𝑋 × ℝ+) ∈ V → ({⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ 𝒫 (𝑋 × ℝ+) ↔ {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ⊆ (𝑋 × ℝ+)))
4431, 43syl 17 . . . . . . . . . . . . . 14 (𝜑 → ({⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ 𝒫 (𝑋 × ℝ+) ↔ {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ⊆ (𝑋 × ℝ+)))
4544adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ({⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ 𝒫 (𝑋 × ℝ+) ↔ {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ⊆ (𝑋 × ℝ+)))
4642, 45mpbiri 247 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ 𝒫 (𝑋 × ℝ+))
47 bcthlem5.7 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑘 ∈ ℕ ((int‘𝐽)‘(𝑀𝑘)) = ∅)
48 simpl 472 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) → 𝑘 ∈ ℕ)
49 rspa 2914 . . . . . . . . . . . . . . . 16 ((∀𝑘 ∈ ℕ ((int‘𝐽)‘(𝑀𝑘)) = ∅ ∧ 𝑘 ∈ ℕ) → ((int‘𝐽)‘(𝑀𝑘)) = ∅)
5047, 48, 49syl2an 493 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((int‘𝐽)‘(𝑀𝑘)) = ∅)
51 ssdif0 3896 . . . . . . . . . . . . . . . . 17 (((ball‘𝐷)‘𝑧) ⊆ (𝑀𝑘) ↔ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) = ∅)
52 1st2nd2 7096 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ (𝑋 × ℝ+) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
5352ad2antll 761 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
5453fveq2d 6107 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) = ((ball‘𝐷)‘⟨(1st𝑧), (2nd𝑧)⟩))
55 df-ov 6552 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑧)(ball‘𝐷)(2nd𝑧)) = ((ball‘𝐷)‘⟨(1st𝑧), (2nd𝑧)⟩)
5654, 55syl6eqr 2662 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) = ((1st𝑧)(ball‘𝐷)(2nd𝑧)))
574adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → 𝐷 ∈ (∞Met‘𝑋))
58 xp1st 7089 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ (𝑋 × ℝ+) → (1st𝑧) ∈ 𝑋)
5958ad2antll 761 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (1st𝑧) ∈ 𝑋)
60 xp2nd 7090 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ (𝑋 × ℝ+) → (2nd𝑧) ∈ ℝ+)
6160ad2antll 761 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (2nd𝑧) ∈ ℝ+)
62 bln0 22030 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st𝑧) ∈ 𝑋 ∧ (2nd𝑧) ∈ ℝ+) → ((1st𝑧)(ball‘𝐷)(2nd𝑧)) ≠ ∅)
6357, 59, 61, 62syl3anc 1318 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((1st𝑧)(ball‘𝐷)(2nd𝑧)) ≠ ∅)
6456, 63eqnetrd 2849 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) ≠ ∅)
657adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → 𝐽 ∈ Top)
66 ffvelrn 6265 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀:ℕ⟶(Clsd‘𝐽) ∧ 𝑘 ∈ ℕ) → (𝑀𝑘) ∈ (Clsd‘𝐽))
678, 48, 66syl2an 493 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑀𝑘) ∈ (Clsd‘𝐽))
6811cldss 20643 . . . . . . . . . . . . . . . . . . . 20 ((𝑀𝑘) ∈ (Clsd‘𝐽) → (𝑀𝑘) ⊆ 𝐽)
6967, 68syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑀𝑘) ⊆ 𝐽)
7061rpxrd 11749 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (2nd𝑧) ∈ ℝ*)
715blopn 22115 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st𝑧) ∈ 𝑋 ∧ (2nd𝑧) ∈ ℝ*) → ((1st𝑧)(ball‘𝐷)(2nd𝑧)) ∈ 𝐽)
7257, 59, 70, 71syl3anc 1318 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((1st𝑧)(ball‘𝐷)(2nd𝑧)) ∈ 𝐽)
7356, 72eqeltrd 2688 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) ∈ 𝐽)
7411ssntr 20672 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ Top ∧ (𝑀𝑘) ⊆ 𝐽) ∧ (((ball‘𝐷)‘𝑧) ∈ 𝐽 ∧ ((ball‘𝐷)‘𝑧) ⊆ (𝑀𝑘))) → ((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀𝑘)))
7574expr 641 . . . . . . . . . . . . . . . . . . 19 (((𝐽 ∈ Top ∧ (𝑀𝑘) ⊆ 𝐽) ∧ ((ball‘𝐷)‘𝑧) ∈ 𝐽) → (((ball‘𝐷)‘𝑧) ⊆ (𝑀𝑘) → ((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀𝑘))))
7665, 69, 73, 75syl21anc 1317 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((ball‘𝐷)‘𝑧) ⊆ (𝑀𝑘) → ((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀𝑘))))
77 ssn0 3928 . . . . . . . . . . . . . . . . . . 19 ((((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀𝑘)) ∧ ((ball‘𝐷)‘𝑧) ≠ ∅) → ((int‘𝐽)‘(𝑀𝑘)) ≠ ∅)
7877expcom 450 . . . . . . . . . . . . . . . . . 18 (((ball‘𝐷)‘𝑧) ≠ ∅ → (((ball‘𝐷)‘𝑧) ⊆ ((int‘𝐽)‘(𝑀𝑘)) → ((int‘𝐽)‘(𝑀𝑘)) ≠ ∅))
7964, 76, 78sylsyld 59 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((ball‘𝐷)‘𝑧) ⊆ (𝑀𝑘) → ((int‘𝐽)‘(𝑀𝑘)) ≠ ∅))
8051, 79syl5bir 232 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) = ∅ → ((int‘𝐽)‘(𝑀𝑘)) ≠ ∅))
8180necon2d 2805 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((int‘𝐽)‘(𝑀𝑘)) = ∅ → (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ≠ ∅))
8250, 81mpd 15 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ≠ ∅)
83 n0 3890 . . . . . . . . . . . . . . 15 ((((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))
8443ad2ant1 1075 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → 𝐷 ∈ (∞Met‘𝑋))
8511difopn 20648 . . . . . . . . . . . . . . . . . . . . 21 ((((ball‘𝐷)‘𝑧) ∈ 𝐽 ∧ (𝑀𝑘) ∈ (Clsd‘𝐽)) → (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ∈ 𝐽)
8673, 67, 85syl2anc 691 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ∈ 𝐽)
87863adant3 1074 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ∈ 𝐽)
88 simp3 1056 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))
89 simp2l 1080 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → 𝑘 ∈ ℕ)
90 nnrp 11718 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
9190rpreccld 11758 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
9289, 91syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → (1 / 𝑘) ∈ ℝ+)
935mopni3 22109 . . . . . . . . . . . . . . . . . . 19 (((𝐷 ∈ (∞Met‘𝑋) ∧ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ∈ 𝐽𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) ∧ (1 / 𝑘) ∈ ℝ+) → ∃𝑛 ∈ ℝ+ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))
9484, 87, 88, 92, 93syl31anc 1321 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → ∃𝑛 ∈ ℝ+ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))
95 simp1 1054 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → 𝜑)
96 elssuni 4403 . . . . . . . . . . . . . . . . . . . . . . . 24 (((ball‘𝐷)‘𝑧) ∈ 𝐽 → ((ball‘𝐷)‘𝑧) ⊆ 𝐽)
9773, 96syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) ⊆ 𝐽)
9823adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → 𝑋 = 𝐽)
9997, 98sseqtr4d 3605 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((ball‘𝐷)‘𝑧) ⊆ 𝑋)
10099ssdifssd 3710 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ⊆ 𝑋)
101100sseld 3567 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) → 𝑥𝑋))
1021013impia 1253 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → 𝑥𝑋)
103 simp2 1055 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)))
104 rphalfcl 11734 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℝ+ → (𝑛 / 2) ∈ ℝ+)
105 rphalflt 11736 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ ℝ+ → (𝑛 / 2) < 𝑛)
106 breq1 4586 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑟 = (𝑛 / 2) → (𝑟 < 𝑛 ↔ (𝑛 / 2) < 𝑛))
107106rspcev 3282 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 / 2) ∈ ℝ+ ∧ (𝑛 / 2) < 𝑛) → ∃𝑟 ∈ ℝ+ 𝑟 < 𝑛)
108104, 105, 107syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℝ+ → ∃𝑟 ∈ ℝ+ 𝑟 < 𝑛)
109108ad2antlr 759 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) ∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))) → ∃𝑟 ∈ ℝ+ 𝑟 < 𝑛)
110 df-rex 2902 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑟 ∈ ℝ+ 𝑟 < 𝑛 ↔ ∃𝑟(𝑟 ∈ ℝ+𝑟 < 𝑛))
111 simpr3 1062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → 𝑟 ∈ ℝ+)
112111rpred 11748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → 𝑟 ∈ ℝ)
113 simpr1 1060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → 𝑛 ∈ ℝ+)
114113rpred 11748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → 𝑛 ∈ ℝ)
115 simplrl 796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → 𝑘 ∈ ℕ)
116115nnrecred 10943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → (1 / 𝑘) ∈ ℝ)
117 simpr2 1061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → 𝑟 < 𝑛)
118 lttr 9993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑟 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (1 / 𝑘) ∈ ℝ) → ((𝑟 < 𝑛𝑛 < (1 / 𝑘)) → 𝑟 < (1 / 𝑘)))
119118expdimp 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑟 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (1 / 𝑘) ∈ ℝ) ∧ 𝑟 < 𝑛) → (𝑛 < (1 / 𝑘) → 𝑟 < (1 / 𝑘)))
120112, 114, 116, 117, 119syl31anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → (𝑛 < (1 / 𝑘) → 𝑟 < (1 / 𝑘)))
1214anim1i 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑥𝑋) → (𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋))
122121adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋))
123 rpxr 11716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
124 rpxr 11716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑛 ∈ ℝ+𝑛 ∈ ℝ*)
125 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑟 < 𝑛𝑟 < 𝑛)
126123, 124, 1253anim123i 1240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑟 ∈ ℝ+𝑛 ∈ ℝ+𝑟 < 𝑛) → (𝑟 ∈ ℝ*𝑛 ∈ ℝ*𝑟 < 𝑛))
1271263coml 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+) → (𝑟 ∈ ℝ*𝑛 ∈ ℝ*𝑟 < 𝑛))
1285blsscls 22122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥𝑋) ∧ (𝑟 ∈ ℝ*𝑛 ∈ ℝ*𝑟 < 𝑛)) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (𝑥(ball‘𝐷)𝑛))
129122, 127, 128syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (𝑥(ball‘𝐷)𝑛))
130 sstr2 3575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (𝑥(ball‘𝐷)𝑛) → ((𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))
131129, 130syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → ((𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) → ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))
132120, 131anim12d 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))))
133 simpllr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → 𝑥𝑋)
134133, 111jca 553 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → (𝑥𝑋𝑟 ∈ ℝ+))
135132, 134jctild 564 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ (𝑛 ∈ ℝ+𝑟 < 𝑛𝑟 ∈ ℝ+)) → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
1361353exp2 1277 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑛 ∈ ℝ+ → (𝑟 < 𝑛 → (𝑟 ∈ ℝ+ → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))))))))
137136com35 96 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑛 ∈ ℝ+ → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → (𝑟 ∈ ℝ+ → (𝑟 < 𝑛 → ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))))))))
138137imp5d 623 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) ∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))) → ((𝑟 ∈ ℝ+𝑟 < 𝑛) → ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
139138eximdv 1833 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) ∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))) → (∃𝑟(𝑟 ∈ ℝ+𝑟 < 𝑛) → ∃𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
140110, 139syl5bi 231 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) ∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))) → (∃𝑟 ∈ ℝ+ 𝑟 < 𝑛 → ∃𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
141109, 140mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) ∧ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))) → ∃𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))))
142141ex 449 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) ∧ 𝑛 ∈ ℝ+) → ((𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → ∃𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
143142rexlimdva 3013 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (∃𝑛 ∈ ℝ+ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → ∃𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
14495, 102, 103, 143syl21anc 1317 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → (∃𝑛 ∈ ℝ+ (𝑛 < (1 / 𝑘) ∧ (𝑥(ball‘𝐷)𝑛) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → ∃𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
14594, 144mpd 15 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+)) ∧ 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))) → ∃𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))))
1461453expia 1259 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) → ∃𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
147146eximdv 1833 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → (∃𝑥 𝑥 ∈ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) → ∃𝑥𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
14883, 147syl5bi 231 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ((((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)) ≠ ∅ → ∃𝑥𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))))
14982, 148mpd 15 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → ∃𝑥𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))))
150 opabn0 4931 . . . . . . . . . . . . 13 ({⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ≠ ∅ ↔ ∃𝑥𝑟((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘)))))
151149, 150sylibr 223 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ≠ ∅)
152 eldifsn 4260 . . . . . . . . . . . 12 ({⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ (𝒫 (𝑋 × ℝ+) ∖ {∅}) ↔ ({⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ 𝒫 (𝑋 × ℝ+) ∧ {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ≠ ∅))
15346, 151, 152sylanbrc 695 . . . . . . . . . . 11 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑧 ∈ (𝑋 × ℝ+))) → {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ (𝒫 (𝑋 × ℝ+) ∖ {∅}))
154153ralrimivva 2954 . . . . . . . . . 10 (𝜑 → ∀𝑘 ∈ ℕ ∀𝑧 ∈ (𝑋 × ℝ+){⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ (𝒫 (𝑋 × ℝ+) ∖ {∅}))
155 bcthlem.5 . . . . . . . . . . 11 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))})
156155fmpt2 7126 . . . . . . . . . 10 (∀𝑘 ∈ ℕ ∀𝑧 ∈ (𝑋 × ℝ+){⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))} ∈ (𝒫 (𝑋 × ℝ+) ∖ {∅}) ↔ 𝐹:(ℕ × (𝑋 × ℝ+))⟶(𝒫 (𝑋 × ℝ+) ∖ {∅}))
157154, 156sylib 207 . . . . . . . . 9 (𝜑𝐹:(ℕ × (𝑋 × ℝ+))⟶(𝒫 (𝑋 × ℝ+) ∖ {∅}))
1581573ad2ant1 1075 . . . . . . . 8 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → 𝐹:(ℕ × (𝑋 × ℝ+))⟶(𝒫 (𝑋 × ℝ+) ∖ {∅}))
159 1z 11284 . . . . . . . . 9 1 ∈ ℤ
160 nnuz 11599 . . . . . . . . 9 ℕ = (ℤ‘1)
161159, 160axdc4uz 12645 . . . . . . . 8 (((𝑋 × ℝ+) ∈ V ∧ ⟨𝑛, 𝑚⟩ ∈ (𝑋 × ℝ+) ∧ 𝐹:(ℕ × (𝑋 × ℝ+))⟶(𝒫 (𝑋 × ℝ+) ∖ {∅})) → ∃𝑔(𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛))))
16232, 41, 158, 161syl3anc 1318 . . . . . . 7 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → ∃𝑔(𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛))))
163 simpl1 1057 . . . . . . . . 9 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → 𝜑)
164163, 1syl 17 . . . . . . . 8 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → 𝐷 ∈ (CMet‘𝑋))
165163, 8syl 17 . . . . . . . 8 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → 𝑀:ℕ⟶(Clsd‘𝐽))
166 simpl3 1059 . . . . . . . 8 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → 𝑚 ∈ ℝ+)
16738adantr 480 . . . . . . . 8 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → 𝑛𝑋)
168 simpr1 1060 . . . . . . . 8 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → 𝑔:ℕ⟶(𝑋 × ℝ+))
169 simpr2 1061 . . . . . . . 8 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → (𝑔‘1) = ⟨𝑛, 𝑚⟩)
170 simpr3 1062 . . . . . . . . 9 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))
171 oveq1 6556 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1))
172171fveq2d 6107 . . . . . . . . . . 11 (𝑛 = 𝑘 → (𝑔‘(𝑛 + 1)) = (𝑔‘(𝑘 + 1)))
173 id 22 . . . . . . . . . . . 12 (𝑛 = 𝑘𝑛 = 𝑘)
174 fveq2 6103 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝑔𝑛) = (𝑔𝑘))
175173, 174oveq12d 6567 . . . . . . . . . . 11 (𝑛 = 𝑘 → (𝑛𝐹(𝑔𝑛)) = (𝑘𝐹(𝑔𝑘)))
176172, 175eleq12d 2682 . . . . . . . . . 10 (𝑛 = 𝑘 → ((𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)) ↔ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔𝑘))))
177176cbvralv 3147 . . . . . . . . 9 (∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)) ↔ ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔𝑘)))
178170, 177sylib 207 . . . . . . . 8 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔𝑘)))
1795, 164, 155, 165, 166, 167, 168, 169, 178bcthlem4 22932 . . . . . . 7 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) ∧ (𝑔:ℕ⟶(𝑋 × ℝ+) ∧ (𝑔‘1) = ⟨𝑛, 𝑚⟩ ∧ ∀𝑛 ∈ ℕ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))) → ((𝑛(ball‘𝐷)𝑚) ∖ ran 𝑀) ≠ ∅)
180162, 179exlimddv 1850 . . . . . 6 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → ((𝑛(ball‘𝐷)𝑚) ∖ ran 𝑀) ≠ ∅)
18111ntrss2 20671 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ ran 𝑀 𝐽) → ((int‘𝐽)‘ ran 𝑀) ⊆ ran 𝑀)
1827, 15, 181syl2anc 691 . . . . . . . . . 10 (𝜑 → ((int‘𝐽)‘ ran 𝑀) ⊆ ran 𝑀)
183 sstr2 3575 . . . . . . . . . 10 ((𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀) → (((int‘𝐽)‘ ran 𝑀) ⊆ ran 𝑀 → (𝑛(ball‘𝐷)𝑚) ⊆ ran 𝑀))
184182, 183syl5com 31 . . . . . . . . 9 (𝜑 → ((𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀) → (𝑛(ball‘𝐷)𝑚) ⊆ ran 𝑀))
185 ssdif0 3896 . . . . . . . . 9 ((𝑛(ball‘𝐷)𝑚) ⊆ ran 𝑀 ↔ ((𝑛(ball‘𝐷)𝑚) ∖ ran 𝑀) = ∅)
186184, 185syl6ib 240 . . . . . . . 8 (𝜑 → ((𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀) → ((𝑛(ball‘𝐷)𝑚) ∖ ran 𝑀) = ∅))
187186necon3ad 2795 . . . . . . 7 (𝜑 → (((𝑛(ball‘𝐷)𝑚) ∖ ran 𝑀) ≠ ∅ → ¬ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀)))
1881873ad2ant1 1075 . . . . . 6 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → (((𝑛(ball‘𝐷)𝑚) ∖ ran 𝑀) ≠ ∅ → ¬ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀)))
189180, 188mpd 15 . . . . 5 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀) ∧ 𝑚 ∈ ℝ+) → ¬ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀))
1901893expa 1257 . . . 4 (((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀)) ∧ 𝑚 ∈ ℝ+) → ¬ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀))
191190nrexdv 2984 . . 3 ((𝜑𝑛 ∈ ((int‘𝐽)‘ ran 𝑀)) → ¬ ∃𝑚 ∈ ℝ+ (𝑛(ball‘𝐷)𝑚) ⊆ ((int‘𝐽)‘ ran 𝑀))
19221, 191pm2.65da 598 . 2 (𝜑 → ¬ 𝑛 ∈ ((int‘𝐽)‘ ran 𝑀))
193192eq0rdv 3931 1 (𝜑 → ((int‘𝐽)‘ ran 𝑀) = ∅)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ⟨cop 4131  ∪ cuni 4372   class class class wbr 4583  {copab 4642   × cxp 5036  ran crn 5039  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  1st c1st 7057  2nd c2nd 7058  ℝcr 9814  1c1 9816   + caddc 9818  ℝ*cxr 9952   < clt 9953   / cdiv 10563  ℕcn 10897  2c2 10947  ℝ+crp 11708  ∞Metcxmt 19552  Metcme 19553  ballcbl 19554  MetOpencmopn 19557  Topctop 20517  Clsdccld 20630  intcnt 20631  clsccl 20632  CMetcms 22860 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-dc 9151  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ico 12052  df-rest 15906  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-top 20521  df-bases 20522  df-topon 20523  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-lm 20843  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-cfil 22861  df-cau 22862  df-cmet 22863 This theorem is referenced by:  bcth  22934
 Copyright terms: Public domain W3C validator