Description: Lemma for bcth . The proof makes essential use of the Axiom of Dependent Choice axdc4uz , which in the form used here accepts a "selection" function F from each element of K to a nonempty subset of K , and the result function g maps g ( n + 1 ) to an element of F ( n , g ( n ) ) . The trick here is thus in the choice of F and K : we let K 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 F ( k , <. x , z >. ) gives the set of all balls of size less than 1 / k , tagged by their centers, whose closures fit within the given open set z and miss M ( k ) .
Since M ( k ) is closed, z \ M ( k ) is open and also nonempty, since z is nonempty and M ( k ) has empty interior. Then there is some ball contained in it, and hence our function F is valid (it never maps to the empty set). Now starting at a point in the interior of U. ran M , DC gives us the function g all whose elements are constrained by F acting on the previous value. (This is all proven in this lemma.) Now g is a sequence of tagged open balls, forming an inclusion chain (see bcthlem2 ) and whose sizes tend to zero, since they are bounded above by 1 / k . Thus, the centers of these balls form a Cauchy sequence, and converge to a point x (see bcthlem4 ). Since the inclusion chain also ensures the closure of each ball is in the previous ball, the point x must be in all these balls (see bcthlem3 ) and hence misses each M ( k ) , contradicting the fact that x is in the interior of U. ran M (which was the starting point). (Contributed by Mario Carneiro, 6-Jan-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | bcth.2 | ⊢ 𝐽 = ( MetOpen ‘ 𝐷 ) | |
| bcthlem.4 | ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) ) | ||
| bcthlem.5 | ⊢ 𝐹 = ( 𝑘 ∈ ℕ , 𝑧 ∈ ( 𝑋 × ℝ+ ) ↦ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ) | ||
| bcthlem.6 | ⊢ ( 𝜑 → 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) | ||
| bcthlem5.7 | ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ ) | ||
| Assertion | bcthlem5 | ⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) = ∅ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bcth.2 | ⊢ 𝐽 = ( MetOpen ‘ 𝐷 ) | |
| 2 | bcthlem.4 | ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) ) | |
| 3 | bcthlem.5 | ⊢ 𝐹 = ( 𝑘 ∈ ℕ , 𝑧 ∈ ( 𝑋 × ℝ+ ) ↦ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ) | |
| 4 | bcthlem.6 | ⊢ ( 𝜑 → 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) | |
| 5 | bcthlem5.7 | ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ ) | |
| 6 | cmetmet | ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) ) | |
| 7 | metxmet | ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) | |
| 8 | 2 6 7 | 3syl | ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
| 9 | 1 | mopntop | ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top ) |
| 10 | 8 9 | syl | ⊢ ( 𝜑 → 𝐽 ∈ Top ) |
| 11 | 4 | frnd | ⊢ ( 𝜑 → ran 𝑀 ⊆ ( Clsd ‘ 𝐽 ) ) |
| 12 | eqid | ⊢ ∪ 𝐽 = ∪ 𝐽 | |
| 13 | 12 | cldss2 | ⊢ ( Clsd ‘ 𝐽 ) ⊆ 𝒫 ∪ 𝐽 |
| 14 | 11 13 | sstrdi | ⊢ ( 𝜑 → ran 𝑀 ⊆ 𝒫 ∪ 𝐽 ) |
| 15 | sspwuni | ⊢ ( ran 𝑀 ⊆ 𝒫 ∪ 𝐽 ↔ ∪ ran 𝑀 ⊆ ∪ 𝐽 ) | |
| 16 | 14 15 | sylib | ⊢ ( 𝜑 → ∪ ran 𝑀 ⊆ ∪ 𝐽 ) |
| 17 | 12 | ntropn | ⊢ ( ( 𝐽 ∈ Top ∧ ∪ ran 𝑀 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∈ 𝐽 ) |
| 18 | 10 16 17 | syl2anc | ⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∈ 𝐽 ) |
| 19 | 8 18 | jca | ⊢ ( 𝜑 → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∈ 𝐽 ) ) |
| 20 | 1 | mopni2 | ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∈ 𝐽 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ) → ∃ 𝑚 ∈ ℝ+ ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ) |
| 21 | 20 | 3expa | ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∈ 𝐽 ) ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ) → ∃ 𝑚 ∈ ℝ+ ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ) |
| 22 | 19 21 | sylan | ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ) → ∃ 𝑚 ∈ ℝ+ ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ) |
| 23 | 1 | mopnuni | ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 ) |
| 24 | 8 23 | syl | ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 ) |
| 25 | 12 | topopn | ⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽 ) |
| 26 | 10 25 | syl | ⊢ ( 𝜑 → ∪ 𝐽 ∈ 𝐽 ) |
| 27 | 24 26 | eqeltrd | ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 ) |
| 28 | reex | ⊢ ℝ ∈ V | |
| 29 | rpssre | ⊢ ℝ+ ⊆ ℝ | |
| 30 | 28 29 | ssexi | ⊢ ℝ+ ∈ V |
| 31 | xpexg | ⊢ ( ( 𝑋 ∈ 𝐽 ∧ ℝ+ ∈ V ) → ( 𝑋 × ℝ+ ) ∈ V ) | |
| 32 | 27 30 31 | sylancl | ⊢ ( 𝜑 → ( 𝑋 × ℝ+ ) ∈ V ) |
| 33 | 32 | 3ad2ant1 | ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) → ( 𝑋 × ℝ+ ) ∈ V ) |
| 34 | 12 | ntrss3 | ⊢ ( ( 𝐽 ∈ Top ∧ ∪ ran 𝑀 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ⊆ ∪ 𝐽 ) |
| 35 | 10 16 34 | syl2anc | ⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ⊆ ∪ 𝐽 ) |
| 36 | 35 24 | sseqtrrd | ⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ⊆ 𝑋 ) |
| 37 | 36 | 3ad2ant1 | ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) → ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ⊆ 𝑋 ) |
| 38 | simp2 | ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) → 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ) | |
| 39 | 37 38 | sseldd | ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) → 𝑛 ∈ 𝑋 ) |
| 40 | simp3 | ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) → 𝑚 ∈ ℝ+ ) | |
| 41 | 39 40 | opelxpd | ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) → ⟨ 𝑛 , 𝑚 ⟩ ∈ ( 𝑋 × ℝ+ ) ) |
| 42 | opabssxp | ⊢ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ⊆ ( 𝑋 × ℝ+ ) | |
| 43 | elpw2g | ⊢ ( ( 𝑋 × ℝ+ ) ∈ V → ( { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ∈ 𝒫 ( 𝑋 × ℝ+ ) ↔ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ⊆ ( 𝑋 × ℝ+ ) ) ) | |
| 44 | 32 43 | syl | ⊢ ( 𝜑 → ( { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ∈ 𝒫 ( 𝑋 × ℝ+ ) ↔ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ⊆ ( 𝑋 × ℝ+ ) ) ) |
| 45 | 44 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ∈ 𝒫 ( 𝑋 × ℝ+ ) ↔ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ⊆ ( 𝑋 × ℝ+ ) ) ) |
| 46 | 42 45 | mpbiri | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ∈ 𝒫 ( 𝑋 × ℝ+ ) ) |
| 47 | simpl | ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) → 𝑘 ∈ ℕ ) | |
| 48 | rspa | ⊢ ( ( ∀ 𝑘 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ ∧ 𝑘 ∈ ℕ ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ ) | |
| 49 | 5 47 48 | syl2an | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ ) |
| 50 | ssdif0 | ⊢ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ⊆ ( 𝑀 ‘ 𝑘 ) ↔ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) = ∅ ) | |
| 51 | 1st2nd2 | ⊢ ( 𝑧 ∈ ( 𝑋 × ℝ+ ) → 𝑧 = ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) | |
| 52 | 51 | ad2antll | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → 𝑧 = ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) |
| 53 | 52 | fveq2d | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) ) |
| 54 | df-ov | ⊢ ( ( 1st ‘ 𝑧 ) ( ball ‘ 𝐷 ) ( 2nd ‘ 𝑧 ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ ) | |
| 55 | 53 54 | eqtr4di | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) = ( ( 1st ‘ 𝑧 ) ( ball ‘ 𝐷 ) ( 2nd ‘ 𝑧 ) ) ) |
| 56 | 8 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
| 57 | xp1st | ⊢ ( 𝑧 ∈ ( 𝑋 × ℝ+ ) → ( 1st ‘ 𝑧 ) ∈ 𝑋 ) | |
| 58 | 57 | ad2antll | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( 1st ‘ 𝑧 ) ∈ 𝑋 ) |
| 59 | xp2nd | ⊢ ( 𝑧 ∈ ( 𝑋 × ℝ+ ) → ( 2nd ‘ 𝑧 ) ∈ ℝ+ ) | |
| 60 | 59 | ad2antll | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( 2nd ‘ 𝑧 ) ∈ ℝ+ ) |
| 61 | bln0 | ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1st ‘ 𝑧 ) ∈ 𝑋 ∧ ( 2nd ‘ 𝑧 ) ∈ ℝ+ ) → ( ( 1st ‘ 𝑧 ) ( ball ‘ 𝐷 ) ( 2nd ‘ 𝑧 ) ) ≠ ∅ ) | |
| 62 | 56 58 60 61 | syl3anc | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( 1st ‘ 𝑧 ) ( ball ‘ 𝐷 ) ( 2nd ‘ 𝑧 ) ) ≠ ∅ ) |
| 63 | 55 62 | eqnetrd | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ≠ ∅ ) |
| 64 | 10 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → 𝐽 ∈ Top ) |
| 65 | ffvelcdm | ⊢ ( ( 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑀 ‘ 𝑘 ) ∈ ( Clsd ‘ 𝐽 ) ) | |
| 66 | 4 47 65 | syl2an | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( 𝑀 ‘ 𝑘 ) ∈ ( Clsd ‘ 𝐽 ) ) |
| 67 | 12 | cldss | ⊢ ( ( 𝑀 ‘ 𝑘 ) ∈ ( Clsd ‘ 𝐽 ) → ( 𝑀 ‘ 𝑘 ) ⊆ ∪ 𝐽 ) |
| 68 | 66 67 | syl | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( 𝑀 ‘ 𝑘 ) ⊆ ∪ 𝐽 ) |
| 69 | 60 | rpxrd | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( 2nd ‘ 𝑧 ) ∈ ℝ* ) |
| 70 | 1 | blopn | ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1st ‘ 𝑧 ) ∈ 𝑋 ∧ ( 2nd ‘ 𝑧 ) ∈ ℝ* ) → ( ( 1st ‘ 𝑧 ) ( ball ‘ 𝐷 ) ( 2nd ‘ 𝑧 ) ) ∈ 𝐽 ) |
| 71 | 56 58 69 70 | syl3anc | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( 1st ‘ 𝑧 ) ( ball ‘ 𝐷 ) ( 2nd ‘ 𝑧 ) ) ∈ 𝐽 ) |
| 72 | 55 71 | eqeltrd | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∈ 𝐽 ) |
| 73 | 12 | ssntr | ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑀 ‘ 𝑘 ) ⊆ ∪ 𝐽 ) ∧ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∈ 𝐽 ∧ ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ⊆ ( 𝑀 ‘ 𝑘 ) ) ) → ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ) |
| 74 | 73 | expr | ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑀 ‘ 𝑘 ) ⊆ ∪ 𝐽 ) ∧ ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∈ 𝐽 ) → ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ⊆ ( 𝑀 ‘ 𝑘 ) → ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ) ) |
| 75 | 64 68 72 74 | syl21anc | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ⊆ ( 𝑀 ‘ 𝑘 ) → ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ) ) |
| 76 | ssn0 | ⊢ ( ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ∧ ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ≠ ∅ ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ≠ ∅ ) | |
| 77 | 76 | expcom | ⊢ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ≠ ∅ → ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ≠ ∅ ) ) |
| 78 | 63 75 77 | sylsyld | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ⊆ ( 𝑀 ‘ 𝑘 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ≠ ∅ ) ) |
| 79 | 50 78 | biimtrrid | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) = ∅ → ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ≠ ∅ ) ) |
| 80 | 79 | necon2d | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ∅ → ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ≠ ∅ ) ) |
| 81 | 49 80 | mpd | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ≠ ∅ ) |
| 82 | n0 | ⊢ ( ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) | |
| 83 | 8 | 3ad2ant1 | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ∧ 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
| 84 | 12 | difopn | ⊢ ( ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∈ 𝐽 ∧ ( 𝑀 ‘ 𝑘 ) ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ∈ 𝐽 ) |
| 85 | 72 66 84 | syl2anc | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ∈ 𝐽 ) |
| 86 | 85 | 3adant3 | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ∧ 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ∈ 𝐽 ) |
| 87 | simp3 | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ∧ 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) | |
| 88 | simp2l | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ∧ 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → 𝑘 ∈ ℕ ) | |
| 89 | nnrp | ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ ) | |
| 90 | 89 | rpreccld | ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ+ ) |
| 91 | 88 90 | syl | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ∧ 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → ( 1 / 𝑘 ) ∈ ℝ+ ) |
| 92 | 1 | mopni3 | ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ∈ 𝐽 ∧ 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ∧ ( 1 / 𝑘 ) ∈ ℝ+ ) → ∃ 𝑛 ∈ ℝ+ ( 𝑛 < ( 1 / 𝑘 ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) |
| 93 | 83 86 87 91 92 | syl31anc | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ∧ 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → ∃ 𝑛 ∈ ℝ+ ( 𝑛 < ( 1 / 𝑘 ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) |
| 94 | simp1 | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ∧ 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → 𝜑 ) | |
| 95 | elssuni | ⊢ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∈ 𝐽 → ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ⊆ ∪ 𝐽 ) | |
| 96 | 72 95 | syl | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ⊆ ∪ 𝐽 ) |
| 97 | 24 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → 𝑋 = ∪ 𝐽 ) |
| 98 | 96 97 | sseqtrrd | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ⊆ 𝑋 ) |
| 99 | 98 | ssdifssd | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ⊆ 𝑋 ) |
| 100 | 99 | sseld | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) → 𝑥 ∈ 𝑋 ) ) |
| 101 | 100 | 3impia | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ∧ 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → 𝑥 ∈ 𝑋 ) |
| 102 | simp2 | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ∧ 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) | |
| 103 | rphalfcl | ⊢ ( 𝑛 ∈ ℝ+ → ( 𝑛 / 2 ) ∈ ℝ+ ) | |
| 104 | rphalflt | ⊢ ( 𝑛 ∈ ℝ+ → ( 𝑛 / 2 ) < 𝑛 ) | |
| 105 | breq1 | ⊢ ( 𝑟 = ( 𝑛 / 2 ) → ( 𝑟 < 𝑛 ↔ ( 𝑛 / 2 ) < 𝑛 ) ) | |
| 106 | 105 | rspcev | ⊢ ( ( ( 𝑛 / 2 ) ∈ ℝ+ ∧ ( 𝑛 / 2 ) < 𝑛 ) → ∃ 𝑟 ∈ ℝ+ 𝑟 < 𝑛 ) |
| 107 | 103 104 106 | syl2anc | ⊢ ( 𝑛 ∈ ℝ+ → ∃ 𝑟 ∈ ℝ+ 𝑟 < 𝑛 ) |
| 108 | 107 | ad2antlr | ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ 𝑛 ∈ ℝ+ ) ∧ ( 𝑛 < ( 1 / 𝑘 ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) → ∃ 𝑟 ∈ ℝ+ 𝑟 < 𝑛 ) |
| 109 | df-rex | ⊢ ( ∃ 𝑟 ∈ ℝ+ 𝑟 < 𝑛 ↔ ∃ 𝑟 ( 𝑟 ∈ ℝ+ ∧ 𝑟 < 𝑛 ) ) | |
| 110 | simpr3 | ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℝ+ ) | |
| 111 | 110 | rpred | ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℝ ) |
| 112 | simpr1 | ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑛 ∈ ℝ+ ) | |
| 113 | 112 | rpred | ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑛 ∈ ℝ ) |
| 114 | simplrl | ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑘 ∈ ℕ ) | |
| 115 | 114 | nnrecred | ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+ ) ) → ( 1 / 𝑘 ) ∈ ℝ ) |
| 116 | simpr2 | ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑟 < 𝑛 ) | |
| 117 | lttr | ⊢ ( ( 𝑟 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ ( 1 / 𝑘 ) ∈ ℝ ) → ( ( 𝑟 < 𝑛 ∧ 𝑛 < ( 1 / 𝑘 ) ) → 𝑟 < ( 1 / 𝑘 ) ) ) | |
| 118 | 117 | expdimp | ⊢ ( ( ( 𝑟 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ ( 1 / 𝑘 ) ∈ ℝ ) ∧ 𝑟 < 𝑛 ) → ( 𝑛 < ( 1 / 𝑘 ) → 𝑟 < ( 1 / 𝑘 ) ) ) |
| 119 | 111 113 115 116 118 | syl31anc | ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑛 < ( 1 / 𝑘 ) → 𝑟 < ( 1 / 𝑘 ) ) ) |
| 120 | 8 | anim1i | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ) |
| 121 | 120 | adantr | ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ) |
| 122 | rpxr | ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* ) | |
| 123 | rpxr | ⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ∈ ℝ* ) | |
| 124 | id | ⊢ ( 𝑟 < 𝑛 → 𝑟 < 𝑛 ) | |
| 125 | 122 123 124 | 3anim123i | ⊢ ( ( 𝑟 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ) → ( 𝑟 ∈ ℝ* ∧ 𝑛 ∈ ℝ* ∧ 𝑟 < 𝑛 ) ) |
| 126 | 125 | 3coml | ⊢ ( ( 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+ ) → ( 𝑟 ∈ ℝ* ∧ 𝑛 ∈ ℝ* ∧ 𝑟 < 𝑛 ) ) |
| 127 | 1 | blsscls | ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ* ∧ 𝑛 ∈ ℝ* ∧ 𝑟 < 𝑛 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ) |
| 128 | 121 126 127 | syl2an | ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+ ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ) |
| 129 | sstr2 | ⊢ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) → ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) | |
| 130 | 128 129 | syl | ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+ ) ) → ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) |
| 131 | 119 130 | anim12d | ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+ ) ) → ( ( 𝑛 < ( 1 / 𝑘 ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) |
| 132 | simpllr | ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑥 ∈ 𝑋 ) | |
| 133 | 132 110 | jca | ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) |
| 134 | 131 133 | jctild | ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑟 < 𝑛 ∧ 𝑟 ∈ ℝ+ ) ) → ( ( 𝑛 < ( 1 / 𝑘 ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) ) |
| 135 | 134 | 3exp2 | ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( 𝑛 ∈ ℝ+ → ( 𝑟 < 𝑛 → ( 𝑟 ∈ ℝ+ → ( ( 𝑛 < ( 1 / 𝑘 ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) ) ) ) ) |
| 136 | 135 | com35 | ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( 𝑛 ∈ ℝ+ → ( ( 𝑛 < ( 1 / 𝑘 ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → ( 𝑟 ∈ ℝ+ → ( 𝑟 < 𝑛 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) ) ) ) ) |
| 137 | 136 | imp5d | ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ 𝑛 ∈ ℝ+ ) ∧ ( 𝑛 < ( 1 / 𝑘 ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) → ( ( 𝑟 ∈ ℝ+ ∧ 𝑟 < 𝑛 ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) ) |
| 138 | 137 | eximdv | ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ 𝑛 ∈ ℝ+ ) ∧ ( 𝑛 < ( 1 / 𝑘 ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) → ( ∃ 𝑟 ( 𝑟 ∈ ℝ+ ∧ 𝑟 < 𝑛 ) → ∃ 𝑟 ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) ) |
| 139 | 109 138 | biimtrid | ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ 𝑛 ∈ ℝ+ ) ∧ ( 𝑛 < ( 1 / 𝑘 ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) → ( ∃ 𝑟 ∈ ℝ+ 𝑟 < 𝑛 → ∃ 𝑟 ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) ) |
| 140 | 108 139 | mpd | ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) ∧ 𝑛 ∈ ℝ+ ) ∧ ( 𝑛 < ( 1 / 𝑘 ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) → ∃ 𝑟 ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) |
| 141 | 140 | rexlimdva2 | ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ∃ 𝑛 ∈ ℝ+ ( 𝑛 < ( 1 / 𝑘 ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → ∃ 𝑟 ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) ) |
| 142 | 94 101 102 141 | syl21anc | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ∧ 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → ( ∃ 𝑛 ∈ ℝ+ ( 𝑛 < ( 1 / 𝑘 ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑛 ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → ∃ 𝑟 ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) ) |
| 143 | 93 142 | mpd | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ∧ 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) → ∃ 𝑟 ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) |
| 144 | 143 | 3expia | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) → ∃ 𝑟 ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) ) |
| 145 | 144 | eximdv | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ∃ 𝑥 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) → ∃ 𝑥 ∃ 𝑟 ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) ) |
| 146 | 82 145 | biimtrid | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ( ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ≠ ∅ → ∃ 𝑥 ∃ 𝑟 ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) ) |
| 147 | 81 146 | mpd | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → ∃ 𝑥 ∃ 𝑟 ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) |
| 148 | opabn0 | ⊢ ( { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ≠ ∅ ↔ ∃ 𝑥 ∃ 𝑟 ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ) | |
| 149 | 147 148 | sylibr | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ≠ ∅ ) |
| 150 | eldifsn | ⊢ ( { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ∈ ( 𝒫 ( 𝑋 × ℝ+ ) ∖ { ∅ } ) ↔ ( { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ∈ 𝒫 ( 𝑋 × ℝ+ ) ∧ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ≠ ∅ ) ) | |
| 151 | 46 149 150 | sylanbrc | ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ( 𝑋 × ℝ+ ) ) ) → { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ∈ ( 𝒫 ( 𝑋 × ℝ+ ) ∖ { ∅ } ) ) |
| 152 | 151 | ralrimivva | ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ∀ 𝑧 ∈ ( 𝑋 × ℝ+ ) { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ∈ ( 𝒫 ( 𝑋 × ℝ+ ) ∖ { ∅ } ) ) |
| 153 | 3 | fmpo | ⊢ ( ∀ 𝑘 ∈ ℕ ∀ 𝑧 ∈ ( 𝑋 × ℝ+ ) { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } ∈ ( 𝒫 ( 𝑋 × ℝ+ ) ∖ { ∅ } ) ↔ 𝐹 : ( ℕ × ( 𝑋 × ℝ+ ) ) ⟶ ( 𝒫 ( 𝑋 × ℝ+ ) ∖ { ∅ } ) ) |
| 154 | 152 153 | sylib | ⊢ ( 𝜑 → 𝐹 : ( ℕ × ( 𝑋 × ℝ+ ) ) ⟶ ( 𝒫 ( 𝑋 × ℝ+ ) ∖ { ∅ } ) ) |
| 155 | 154 | 3ad2ant1 | ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) → 𝐹 : ( ℕ × ( 𝑋 × ℝ+ ) ) ⟶ ( 𝒫 ( 𝑋 × ℝ+ ) ∖ { ∅ } ) ) |
| 156 | 1z | ⊢ 1 ∈ ℤ | |
| 157 | nnuz | ⊢ ℕ = ( ℤ≥ ‘ 1 ) | |
| 158 | 156 157 | axdc4uz | ⊢ ( ( ( 𝑋 × ℝ+ ) ∈ V ∧ ⟨ 𝑛 , 𝑚 ⟩ ∈ ( 𝑋 × ℝ+ ) ∧ 𝐹 : ( ℕ × ( 𝑋 × ℝ+ ) ) ⟶ ( 𝒫 ( 𝑋 × ℝ+ ) ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ ( 𝑋 × ℝ+ ) ∧ ( 𝑔 ‘ 1 ) = ⟨ 𝑛 , 𝑚 ⟩ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑛 𝐹 ( 𝑔 ‘ 𝑛 ) ) ) ) |
| 159 | 33 41 155 158 | syl3anc | ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) → ∃ 𝑔 ( 𝑔 : ℕ ⟶ ( 𝑋 × ℝ+ ) ∧ ( 𝑔 ‘ 1 ) = ⟨ 𝑛 , 𝑚 ⟩ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑛 𝐹 ( 𝑔 ‘ 𝑛 ) ) ) ) |
| 160 | simpl1 | ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑔 : ℕ ⟶ ( 𝑋 × ℝ+ ) ∧ ( 𝑔 ‘ 1 ) = ⟨ 𝑛 , 𝑚 ⟩ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑛 𝐹 ( 𝑔 ‘ 𝑛 ) ) ) ) → 𝜑 ) | |
| 161 | 160 2 | syl | ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑔 : ℕ ⟶ ( 𝑋 × ℝ+ ) ∧ ( 𝑔 ‘ 1 ) = ⟨ 𝑛 , 𝑚 ⟩ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑛 𝐹 ( 𝑔 ‘ 𝑛 ) ) ) ) → 𝐷 ∈ ( CMet ‘ 𝑋 ) ) |
| 162 | 160 4 | syl | ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑔 : ℕ ⟶ ( 𝑋 × ℝ+ ) ∧ ( 𝑔 ‘ 1 ) = ⟨ 𝑛 , 𝑚 ⟩ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑛 𝐹 ( 𝑔 ‘ 𝑛 ) ) ) ) → 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ) |
| 163 | simpl3 | ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑔 : ℕ ⟶ ( 𝑋 × ℝ+ ) ∧ ( 𝑔 ‘ 1 ) = ⟨ 𝑛 , 𝑚 ⟩ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑛 𝐹 ( 𝑔 ‘ 𝑛 ) ) ) ) → 𝑚 ∈ ℝ+ ) | |
| 164 | 39 | adantr | ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑔 : ℕ ⟶ ( 𝑋 × ℝ+ ) ∧ ( 𝑔 ‘ 1 ) = ⟨ 𝑛 , 𝑚 ⟩ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑛 𝐹 ( 𝑔 ‘ 𝑛 ) ) ) ) → 𝑛 ∈ 𝑋 ) |
| 165 | simpr1 | ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑔 : ℕ ⟶ ( 𝑋 × ℝ+ ) ∧ ( 𝑔 ‘ 1 ) = ⟨ 𝑛 , 𝑚 ⟩ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑛 𝐹 ( 𝑔 ‘ 𝑛 ) ) ) ) → 𝑔 : ℕ ⟶ ( 𝑋 × ℝ+ ) ) | |
| 166 | simpr2 | ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑔 : ℕ ⟶ ( 𝑋 × ℝ+ ) ∧ ( 𝑔 ‘ 1 ) = ⟨ 𝑛 , 𝑚 ⟩ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑛 𝐹 ( 𝑔 ‘ 𝑛 ) ) ) ) → ( 𝑔 ‘ 1 ) = ⟨ 𝑛 , 𝑚 ⟩ ) | |
| 167 | simpr3 | ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑔 : ℕ ⟶ ( 𝑋 × ℝ+ ) ∧ ( 𝑔 ‘ 1 ) = ⟨ 𝑛 , 𝑚 ⟩ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑛 𝐹 ( 𝑔 ‘ 𝑛 ) ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑛 𝐹 ( 𝑔 ‘ 𝑛 ) ) ) | |
| 168 | fvoveq1 | ⊢ ( 𝑛 = 𝑘 → ( 𝑔 ‘ ( 𝑛 + 1 ) ) = ( 𝑔 ‘ ( 𝑘 + 1 ) ) ) | |
| 169 | id | ⊢ ( 𝑛 = 𝑘 → 𝑛 = 𝑘 ) | |
| 170 | fveq2 | ⊢ ( 𝑛 = 𝑘 → ( 𝑔 ‘ 𝑛 ) = ( 𝑔 ‘ 𝑘 ) ) | |
| 171 | 169 170 | oveq12d | ⊢ ( 𝑛 = 𝑘 → ( 𝑛 𝐹 ( 𝑔 ‘ 𝑛 ) ) = ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) |
| 172 | 168 171 | eleq12d | ⊢ ( 𝑛 = 𝑘 → ( ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑛 𝐹 ( 𝑔 ‘ 𝑛 ) ) ↔ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ) |
| 173 | 172 | cbvralvw | ⊢ ( ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑛 𝐹 ( 𝑔 ‘ 𝑛 ) ) ↔ ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) |
| 174 | 167 173 | sylib | ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑔 : ℕ ⟶ ( 𝑋 × ℝ+ ) ∧ ( 𝑔 ‘ 1 ) = ⟨ 𝑛 , 𝑚 ⟩ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑛 𝐹 ( 𝑔 ‘ 𝑛 ) ) ) ) → ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) |
| 175 | 1 161 3 162 163 164 165 166 174 | bcthlem4 | ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) ∧ ( 𝑔 : ℕ ⟶ ( 𝑋 × ℝ+ ) ∧ ( 𝑔 ‘ 1 ) = ⟨ 𝑛 , 𝑚 ⟩ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑛 𝐹 ( 𝑔 ‘ 𝑛 ) ) ) ) → ( ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ∖ ∪ ran 𝑀 ) ≠ ∅ ) |
| 176 | 159 175 | exlimddv | ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) → ( ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ∖ ∪ ran 𝑀 ) ≠ ∅ ) |
| 177 | 12 | ntrss2 | ⊢ ( ( 𝐽 ∈ Top ∧ ∪ ran 𝑀 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ⊆ ∪ ran 𝑀 ) |
| 178 | 10 16 177 | syl2anc | ⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ⊆ ∪ ran 𝑀 ) |
| 179 | sstr2 | ⊢ ( ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) → ( ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ⊆ ∪ ran 𝑀 → ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ⊆ ∪ ran 𝑀 ) ) | |
| 180 | 178 179 | syl5com | ⊢ ( 𝜑 → ( ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) → ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ⊆ ∪ ran 𝑀 ) ) |
| 181 | ssdif0 | ⊢ ( ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ⊆ ∪ ran 𝑀 ↔ ( ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ∖ ∪ ran 𝑀 ) = ∅ ) | |
| 182 | 180 181 | imbitrdi | ⊢ ( 𝜑 → ( ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) → ( ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ∖ ∪ ran 𝑀 ) = ∅ ) ) |
| 183 | 182 | necon3ad | ⊢ ( 𝜑 → ( ( ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ∖ ∪ ran 𝑀 ) ≠ ∅ → ¬ ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ) ) |
| 184 | 183 | 3ad2ant1 | ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) → ( ( ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ∖ ∪ ran 𝑀 ) ≠ ∅ → ¬ ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ) ) |
| 185 | 176 184 | mpd | ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ∧ 𝑚 ∈ ℝ+ ) → ¬ ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ) |
| 186 | 185 | 3expa | ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ) ∧ 𝑚 ∈ ℝ+ ) → ¬ ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ) |
| 187 | 186 | nrexdv | ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ) → ¬ ∃ 𝑚 ∈ ℝ+ ( 𝑛 ( ball ‘ 𝐷 ) 𝑚 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ) |
| 188 | 22 187 | pm2.65da | ⊢ ( 𝜑 → ¬ 𝑛 ∈ ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) ) |
| 189 | 188 | eq0rdv | ⊢ ( 𝜑 → ( ( int ‘ 𝐽 ) ‘ ∪ ran 𝑀 ) = ∅ ) |