Metamath Proof Explorer

Theorem ubthlem1

Description: Lemma for ubth . The function A exhibits a countable collection of sets that are closed, being the inverse image under t of the closed ball of radius k , and by assumption they cover X . Thus, by the Baire Category theorem bcth2 , for some n the set An has an interior, meaning that there is a closed ball { z e. X | ( y D z ) <_ r } in the set. (Contributed by Mario Carneiro, 11-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses ubth.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ubth.2 ⊢ 𝑁 = ( normCV ‘ 𝑊 )
ubthlem.3 ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
ubthlem.4 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
ubthlem.5 ⊢ 𝑈 ∈ CBan
ubthlem.6 ⊢ 𝑊 ∈ NrmCVec
ubthlem.7 ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) )
ubthlem.8 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 )
ubthlem.9 ⊢ 𝐴 = ( 𝑘 ∈ ℕ ↦ { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } )
Assertion ubthlem1 ( 𝜑 → ∃ 𝑛 ∈ ℕ ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) )

Proof

Step Hyp Ref Expression
1 ubth.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 ubth.2 ⊢ 𝑁 = ( normCV ‘ 𝑊 )
3 ubthlem.3 ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
4 ubthlem.4 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
5 ubthlem.5 ⊢ 𝑈 ∈ CBan
6 ubthlem.6 ⊢ 𝑊 ∈ NrmCVec
7 ubthlem.7 ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) )
8 ubthlem.8 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 )
9 ubthlem.9 ⊢ 𝐴 = ( 𝑘 ∈ ℕ ↦ { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } )
10 rzal ⊢ ( 𝑇 = ∅ → ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 )
11 10 ralrimivw ⊢ ( 𝑇 = ∅ → ∀ 𝑧 ∈ 𝑋 ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 )
12 rabid2 ⊢ ( 𝑋 = { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 )
13 11 12 sylibr ⊢ ( 𝑇 = ∅ → 𝑋 = { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } )
14 13 eqcomd ⊢ ( 𝑇 = ∅ → { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } = 𝑋 )
15 14 eleq1d ⊢ ( 𝑇 = ∅ → ( { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } ∈ ( Clsd ‘ 𝐽 ) ↔ 𝑋 ∈ ( Clsd ‘ 𝐽 ) ) )
16 iinrab ⊢ ( 𝑇 ≠ ∅ → ∩ 𝑡 ∈ 𝑇 { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } = { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } )
17 16 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑇 ≠ ∅ ) → ∩ 𝑡 ∈ 𝑇 { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } = { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } )
18 id ⊢ ( 𝑇 ≠ ∅ → 𝑇 ≠ ∅ )
19 7 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) )
20 eqid ⊢ ( IndMet ‘ 𝑊 ) = ( IndMet ‘ 𝑊 )
21 eqid ⊢ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) = ( MetOpen ‘ ( IndMet ‘ 𝑊 ) )
22 eqid ⊢ ( 𝑈 BLnOp 𝑊 ) = ( 𝑈 BLnOp 𝑊 )
23 bnnv ⊢ ( 𝑈 ∈ CBan → 𝑈 ∈ NrmCVec )
24 5 23 ax-mp ⊢ 𝑈 ∈ NrmCVec
25 3 20 4 21 22 24 6 blocn2 ⊢ ( 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) → 𝑡 ∈ ( 𝐽 Cn ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) )
26 1 3 cbncms ⊢ ( 𝑈 ∈ CBan → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
27 5 26 ax-mp ⊢ 𝐷 ∈ ( CMet ‘ 𝑋 )
28 cmetmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
29 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
30 27 28 29 mp2b ⊢ 𝐷 ∈ ( ∞Met ‘ 𝑋 )
31 4 mopntopon ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
32 30 31 ax-mp ⊢ 𝐽 ∈ ( TopOn ‘ 𝑋 )
33 eqid ⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
34 33 20 imsxmet ⊢ ( 𝑊 ∈ NrmCVec → ( IndMet ‘ 𝑊 ) ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑊 ) ) )
35 6 34 ax-mp ⊢ ( IndMet ‘ 𝑊 ) ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑊 ) )
36 21 mopntopon ⊢ ( ( IndMet ‘ 𝑊 ) ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑊 ) ) → ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ∈ ( TopOn ‘ ( BaseSet ‘ 𝑊 ) ) )
37 35 36 ax-mp ⊢ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ∈ ( TopOn ‘ ( BaseSet ‘ 𝑊 ) )
38 iscncl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ∈ ( TopOn ‘ ( BaseSet ‘ 𝑊 ) ) ) → ( 𝑡 ∈ ( 𝐽 Cn ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) ↔ ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Clsd ‘ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) ( ◡ 𝑡 “ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
39 32 37 38 mp2an ⊢ ( 𝑡 ∈ ( 𝐽 Cn ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) ↔ ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Clsd ‘ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) ( ◡ 𝑡 “ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ) )
40 25 39 sylib ⊢ ( 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) → ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Clsd ‘ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) ( ◡ 𝑡 “ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ) )
41 19 40 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Clsd ‘ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) ( ◡ 𝑡 “ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ) )
42 41 simpld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
43 42 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑡 ∈ 𝑇 ) → 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
44 43 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑡 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) )
45 44 biantrurd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ↔ ( ( 𝑡 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) ∧ ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) ) )
46 fveq2 ⊢ ( 𝑦 = ( 𝑡 ‘ 𝑥 ) → ( 𝑁 ‘ 𝑦 ) = ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) )
47 46 breq1d ⊢ ( 𝑦 = ( 𝑡 ‘ 𝑥 ) → ( ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 ↔ ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) )
48 47 elrab ⊢ ( ( 𝑡 ‘ 𝑥 ) ∈ { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } ↔ ( ( 𝑡 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) ∧ ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) )
49 45 48 bitr4di ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ↔ ( 𝑡 ‘ 𝑥 ) ∈ { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } ) )
50 49 pm5.32da ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑡 ‘ 𝑥 ) ∈ { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } ) ) )
51 2fveq3 ⊢ ( 𝑧 = 𝑥 → ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) = ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) )
52 51 breq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 ↔ ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) )
53 52 elrab ⊢ ( 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) )
54 53 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) ) )
55 ffn ⊢ ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) → 𝑡 Fn 𝑋 )
56 elpreima ⊢ ( 𝑡 Fn 𝑋 → ( 𝑥 ∈ ( ◡ 𝑡 “ { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑡 ‘ 𝑥 ) ∈ { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } ) ) )
57 43 55 56 3syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝑥 ∈ ( ◡ 𝑡 “ { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑡 ‘ 𝑥 ) ∈ { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } ) ) )
58 50 54 57 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } ↔ 𝑥 ∈ ( ◡ 𝑡 “ { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } ) ) )
59 58 eqrdv ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑡 ∈ 𝑇 ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } = ( ◡ 𝑡 “ { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } ) )
60 imaeq2 ⊢ ( 𝑥 = { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } → ( ◡ 𝑡 “ 𝑥 ) = ( ◡ 𝑡 “ { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } ) )
61 60 eleq1d ⊢ ( 𝑥 = { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } → ( ( ◡ 𝑡 “ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ↔ ( ◡ 𝑡 “ { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } ) ∈ ( Clsd ‘ 𝐽 ) ) )
62 41 simprd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ∀ 𝑥 ∈ ( Clsd ‘ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) ( ◡ 𝑡 “ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
63 62 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑡 ∈ 𝑇 ) → ∀ 𝑥 ∈ ( Clsd ‘ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) ( ◡ 𝑡 “ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
64 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
65 64 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑡 ∈ 𝑇 ) → 𝑘 ∈ ℝ )
66 65 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑡 ∈ 𝑇 ) → 𝑘 ∈ ℝ* )
67 eqid ⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 )
68 33 67 nvzcl ⊢ ( 𝑊 ∈ NrmCVec → ( 0vec ‘ 𝑊 ) ∈ ( BaseSet ‘ 𝑊 ) )
69 6 68 ax-mp ⊢ ( 0vec ‘ 𝑊 ) ∈ ( BaseSet ‘ 𝑊 )
70 33 67 2 20 nvnd ⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑁 ‘ 𝑦 ) = ( 𝑦 ( IndMet ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) )
71 6 70 mpan ⊢ ( 𝑦 ∈ ( BaseSet ‘ 𝑊 ) → ( 𝑁 ‘ 𝑦 ) = ( 𝑦 ( IndMet ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) )
72 xmetsym ⊢ ( ( ( IndMet ‘ 𝑊 ) ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑊 ) ) ∧ ( 0vec ‘ 𝑊 ) ∈ ( BaseSet ‘ 𝑊 ) ∧ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ) → ( ( 0vec ‘ 𝑊 ) ( IndMet ‘ 𝑊 ) 𝑦 ) = ( 𝑦 ( IndMet ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) )
73 35 69 72 mp3an12 ⊢ ( 𝑦 ∈ ( BaseSet ‘ 𝑊 ) → ( ( 0vec ‘ 𝑊 ) ( IndMet ‘ 𝑊 ) 𝑦 ) = ( 𝑦 ( IndMet ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) )
74 71 73 eqtr4d ⊢ ( 𝑦 ∈ ( BaseSet ‘ 𝑊 ) → ( 𝑁 ‘ 𝑦 ) = ( ( 0vec ‘ 𝑊 ) ( IndMet ‘ 𝑊 ) 𝑦 ) )
75 74 breq1d ⊢ ( 𝑦 ∈ ( BaseSet ‘ 𝑊 ) → ( ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 ↔ ( ( 0vec ‘ 𝑊 ) ( IndMet ‘ 𝑊 ) 𝑦 ) ≤ 𝑘 ) )
76 75 rabbiia ⊢ { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } = { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( ( 0vec ‘ 𝑊 ) ( IndMet ‘ 𝑊 ) 𝑦 ) ≤ 𝑘 }
77 21 76 blcld ⊢ ( ( ( IndMet ‘ 𝑊 ) ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑊 ) ) ∧ ( 0vec ‘ 𝑊 ) ∈ ( BaseSet ‘ 𝑊 ) ∧ 𝑘 ∈ ℝ* ) → { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } ∈ ( Clsd ‘ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) )
78 35 69 77 mp3an12 ⊢ ( 𝑘 ∈ ℝ* → { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } ∈ ( Clsd ‘ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) )
79 66 78 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑡 ∈ 𝑇 ) → { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } ∈ ( Clsd ‘ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) )
80 61 63 79 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑡 ∈ 𝑇 ) → ( ◡ 𝑡 “ { 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ∣ ( 𝑁 ‘ 𝑦 ) ≤ 𝑘 } ) ∈ ( Clsd ‘ 𝐽 ) )
81 59 80 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑡 ∈ 𝑇 ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } ∈ ( Clsd ‘ 𝐽 ) )
82 81 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ∀ 𝑡 ∈ 𝑇 { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } ∈ ( Clsd ‘ 𝐽 ) )
83 iincld ⊢ ( ( 𝑇 ≠ ∅ ∧ ∀ 𝑡 ∈ 𝑇 { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } ∈ ( Clsd ‘ 𝐽 ) ) → ∩ 𝑡 ∈ 𝑇 { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } ∈ ( Clsd ‘ 𝐽 ) )
84 18 82 83 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑇 ≠ ∅ ) → ∩ 𝑡 ∈ 𝑇 { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } ∈ ( Clsd ‘ 𝐽 ) )
85 17 84 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑇 ≠ ∅ ) → { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } ∈ ( Clsd ‘ 𝐽 ) )
86 4 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
87 30 86 ax-mp ⊢ 𝐽 ∈ Top
88 32 toponunii ⊢ 𝑋 = ∪ 𝐽
89 88 topcld ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ ( Clsd ‘ 𝐽 ) )
90 87 89 ax-mp ⊢ 𝑋 ∈ ( Clsd ‘ 𝐽 )
91 90 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑋 ∈ ( Clsd ‘ 𝐽 ) )
92 15 85 91 pm2.61ne ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } ∈ ( Clsd ‘ 𝐽 ) )
93 92 9 fmptd ⊢ ( 𝜑 → 𝐴 : ℕ ⟶ ( Clsd ‘ 𝐽 ) )
94 93 frnd ⊢ ( 𝜑 → ran 𝐴 ⊆ ( Clsd ‘ 𝐽 ) )
95 88 cldss2 ⊢ ( Clsd ‘ 𝐽 ) ⊆ 𝒫 𝑋
96 94 95 sstrdi ⊢ ( 𝜑 → ran 𝐴 ⊆ 𝒫 𝑋 )
97 sspwuni ⊢ ( ran 𝐴 ⊆ 𝒫 𝑋 ↔ ∪ ran 𝐴 ⊆ 𝑋 )
98 96 97 sylib ⊢ ( 𝜑 → ∪ ran 𝐴 ⊆ 𝑋 )
99 arch ⊢ ( 𝑐 ∈ ℝ → ∃ 𝑘 ∈ ℕ 𝑐 < 𝑘 )
100 99 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) → ∃ 𝑘 ∈ ℕ 𝑐 < 𝑘 )
101 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) → 𝑐 ∈ ℝ )
102 ltle ⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑐 < 𝑘 → 𝑐 ≤ 𝑘 ) )
103 101 64 102 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑐 < 𝑘 → 𝑐 ≤ 𝑘 ) )
104 103 impr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑐 < 𝑘 ) ) → 𝑐 ≤ 𝑘 )
105 104 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑐 < 𝑘 ) ) ∧ 𝑡 ∈ 𝑇 ) → 𝑐 ≤ 𝑘 )
106 42 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑡 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) )
107 106 an32s ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝑡 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) )
108 33 2 nvcl ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑡 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ∈ ℝ )
109 6 107 108 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ∈ ℝ )
110 109 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ∈ ℝ )
111 110 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑐 < 𝑘 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ∈ ℝ )
112 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑐 < 𝑘 ) ) ∧ 𝑡 ∈ 𝑇 ) → 𝑐 ∈ ℝ )
113 simplrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑐 < 𝑘 ) ) ∧ 𝑡 ∈ 𝑇 ) → 𝑘 ∈ ℕ )
114 113 64 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑐 < 𝑘 ) ) ∧ 𝑡 ∈ 𝑇 ) → 𝑘 ∈ ℝ )
115 letr ⊢ ( ( ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ∧ 𝑐 ≤ 𝑘 ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) )
116 111 112 114 115 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑐 < 𝑘 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( ( ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ∧ 𝑐 ≤ 𝑘 ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) )
117 105 116 mpan2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑐 < 𝑘 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) )
118 117 ralimdva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑐 < 𝑘 ) ) → ( ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 → ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) )
119 118 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑐 < 𝑘 → ( ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 → ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) ) )
120 1 fvexi ⊢ 𝑋 ∈ V
121 120 rabex ⊢ { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } ∈ V
122 9 fvmpt2 ⊢ ( ( 𝑘 ∈ ℕ ∧ { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } ∈ V ) → ( 𝐴 ‘ 𝑘 ) = { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } )
123 121 122 mpan2 ⊢ ( 𝑘 ∈ ℕ → ( 𝐴 ‘ 𝑘 ) = { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } )
124 123 eleq2d ⊢ ( 𝑘 ∈ ℕ → ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) ↔ 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } ) )
125 52 ralbidv ⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) )
126 125 elrab ⊢ ( 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } ↔ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) )
127 124 126 bitrdi ⊢ ( 𝑘 ∈ ℕ → ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) ) )
128 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
129 128 biantrurd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ↔ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) ) )
130 129 bicomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) )
131 127 130 sylan9bbr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 ) )
132 93 ffnd ⊢ ( 𝜑 → 𝐴 Fn ℕ )
133 132 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 Fn ℕ )
134 fnfvelrn ⊢ ( ( 𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ‘ 𝑘 ) ∈ ran 𝐴 )
135 elssuni ⊢ ( ( 𝐴 ‘ 𝑘 ) ∈ ran 𝐴 → ( 𝐴 ‘ 𝑘 ) ⊆ ∪ ran 𝐴 )
136 134 135 syl ⊢ ( ( 𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ‘ 𝑘 ) ⊆ ∪ ran 𝐴 )
137 136 sseld ⊢ ( ( 𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) → 𝑥 ∈ ∪ ran 𝐴 ) )
138 133 137 sylan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ∈ ( 𝐴 ‘ 𝑘 ) → 𝑥 ∈ ∪ ran 𝐴 ) )
139 131 138 sylbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ ℕ ) → ( ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 → 𝑥 ∈ ∪ ran 𝐴 ) )
140 139 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑘 → 𝑥 ∈ ∪ ran 𝐴 ) )
141 119 140 syl6d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑐 < 𝑘 → ( ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴 ) ) )
142 141 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) → ( ∃ 𝑘 ∈ ℕ 𝑐 < 𝑘 → ( ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴 ) ) )
143 100 142 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ℝ ) → ( ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴 ) )
144 143 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 → 𝑥 ∈ ∪ ran 𝐴 ) )
145 144 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 → ∀ 𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran 𝐴 ) )
146 8 145 mpd ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran 𝐴 )
147 dfss3 ⊢ ( 𝑋 ⊆ ∪ ran 𝐴 ↔ ∀ 𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran 𝐴 )
148 146 147 sylibr ⊢ ( 𝜑 → 𝑋 ⊆ ∪ ran 𝐴 )
149 98 148 eqssd ⊢ ( 𝜑 → ∪ ran 𝐴 = 𝑋 )
150 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
151 1 150 nvzcl ⊢ ( 𝑈 ∈ NrmCVec → ( 0vec ‘ 𝑈 ) ∈ 𝑋 )
152 ne0i ⊢ ( ( 0vec ‘ 𝑈 ) ∈ 𝑋 → 𝑋 ≠ ∅ )
153 24 151 152 mp2b ⊢ 𝑋 ≠ ∅
154 4 bcth2 ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑋 ≠ ∅ ) ∧ ( 𝐴 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ∧ ∪ ran 𝐴 = 𝑋 ) ) → ∃ 𝑛 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ≠ ∅ )
155 27 153 154 mpanl12 ⊢ ( ( 𝐴 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ∧ ∪ ran 𝐴 = 𝑋 ) → ∃ 𝑛 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ≠ ∅ )
156 93 149 155 syl2anc ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ≠ ∅ )
157 ffvelrn ⊢ ( ( 𝐴 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ∈ ( Clsd ‘ 𝐽 ) )
158 95 157 sselid ⊢ ( ( 𝐴 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ∈ 𝒫 𝑋 )
159 158 elpwid ⊢ ( ( 𝐴 : ℕ ⟶ ( Clsd ‘ 𝐽 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ⊆ 𝑋 )
160 93 159 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ⊆ 𝑋 )
161 88 ntrss3 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ‘ 𝑛 ) ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ⊆ 𝑋 )
162 87 160 161 sylancr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ⊆ 𝑋 )
163 162 sseld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) → 𝑦 ∈ 𝑋 ) )
164 88 ntropn ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ‘ 𝑛 ) ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ 𝐽 )
165 87 160 164 sylancr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ 𝐽 )
166 4 mopni2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ 𝐽 ∧ 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) )
167 30 166 mp3an1 ⊢ ( ( ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ 𝐽 ∧ 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) )
168 165 167 sylan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) )
169 elssuni ⊢ ( ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ 𝐽 → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ⊆ ∪ 𝐽 )
170 169 88 sseqtrrdi ⊢ ( ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ∈ 𝐽 → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ⊆ 𝑋 )
171 165 170 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ⊆ 𝑋 )
172 171 sselda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) → 𝑦 ∈ 𝑋 )
173 88 ntrss2 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ‘ 𝑛 ) ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ⊆ ( 𝐴 ‘ 𝑛 ) )
174 87 160 173 sylancr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ⊆ ( 𝐴 ‘ 𝑛 ) )
175 sstr2 ⊢ ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) → ( ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ⊆ ( 𝐴 ‘ 𝑛 ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐴 ‘ 𝑛 ) ) )
176 174 175 syl5com ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐴 ‘ 𝑛 ) ) )
177 176 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐴 ‘ 𝑛 ) ) )
178 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
179 178 30 jctil ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) )
180 rphalfcl ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 / 2 ) ∈ ℝ+ )
181 180 rpxrd ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 / 2 ) ∈ ℝ* )
182 rpxr ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ* )
183 rphalflt ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 / 2 ) < 𝑥 )
184 181 182 183 3jca ⊢ ( 𝑥 ∈ ℝ+ → ( ( 𝑥 / 2 ) ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ ( 𝑥 / 2 ) < 𝑥 ) )
185 eqid ⊢ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ ( 𝑥 / 2 ) } = { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ ( 𝑥 / 2 ) }
186 4 185 blsscls2 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( ( 𝑥 / 2 ) ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ ( 𝑥 / 2 ) < 𝑥 ) ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ ( 𝑥 / 2 ) } ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) )
187 179 184 186 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ ( 𝑥 / 2 ) } ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) )
188 sstr2 ⊢ ( { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ ( 𝑥 / 2 ) } ⊆ ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) → ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐴 ‘ 𝑛 ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ ( 𝑥 / 2 ) } ⊆ ( 𝐴 ‘ 𝑛 ) ) )
189 187 188 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝐴 ‘ 𝑛 ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ ( 𝑥 / 2 ) } ⊆ ( 𝐴 ‘ 𝑛 ) ) )
190 180 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / 2 ) ∈ ℝ+ )
191 breq2 ⊢ ( 𝑟 = ( 𝑥 / 2 ) → ( ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 ↔ ( 𝑦 𝐷 𝑧 ) ≤ ( 𝑥 / 2 ) ) )
192 191 rabbidv ⊢ ( 𝑟 = ( 𝑥 / 2 ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } = { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ ( 𝑥 / 2 ) } )
193 192 sseq1d ⊢ ( 𝑟 = ( 𝑥 / 2 ) → ( { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) ↔ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ ( 𝑥 / 2 ) } ⊆ ( 𝐴 ‘ 𝑛 ) ) )
194 193 rspcev ⊢ ( ( ( 𝑥 / 2 ) ∈ ℝ+ ∧ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ ( 𝑥 / 2 ) } ⊆ ( 𝐴 ‘ 𝑛 ) ) → ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) )
195 194 ex ⊢ ( ( 𝑥 / 2 ) ∈ ℝ+ → ( { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ ( 𝑥 / 2 ) } ⊆ ( 𝐴 ‘ 𝑛 ) → ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) ) )
196 190 195 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ ( 𝑥 / 2 ) } ⊆ ( 𝐴 ‘ 𝑛 ) → ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) ) )
197 177 189 196 3syld ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) → ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) ) )
198 197 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ 𝑋 ) → ( ∃ 𝑥 ∈ ℝ+ ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) → ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) ) )
199 172 198 syldan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) → ( ∃ 𝑥 ∈ ℝ+ ( 𝑦 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) → ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) ) )
200 168 199 mpd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) → ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) )
201 200 ex ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) → ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) ) )
202 163 201 jcad ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) → ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) ) ) )
203 202 eximdv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∃ 𝑦 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) → ∃ 𝑦 ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) ) ) )
204 n0 ⊢ ( ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) )
205 df-rex ⊢ ( ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) ) )
206 203 204 205 3imtr4g ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ≠ ∅ → ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) ) )
207 206 reximdva ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ≠ ∅ → ∃ 𝑛 ∈ ℕ ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) ) )
208 156 207 mpd ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( 𝐴 ‘ 𝑛 ) )