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

Theorem ubthlem1 30390
Description: Lemma for ubth 30393. The function 𝐴 exhibits a countable collection of sets that are closed, being the inverse image under 𝑑 of the closed ball of radius π‘˜, and by assumption they cover 𝑋. Thus, by the Baire Category theorem bcth2 25078, for some 𝑛 the set π΄β€˜π‘› has an interior, meaning that there is a closed ball {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} in the set. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
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
Ref Expression
ubthlem1 (πœ‘ β†’ βˆƒπ‘› ∈ β„• βˆƒπ‘¦ ∈ 𝑋 βˆƒπ‘Ÿ ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›))
Distinct variable groups:   π‘˜,𝑐,𝑛,π‘Ÿ,π‘₯,𝑦,𝑧,𝐴   𝑑,𝑐,𝐷,π‘˜,𝑛,π‘Ÿ,π‘₯,𝑧   π‘˜,𝐽,𝑛   𝑦,𝑑,𝐽,π‘₯   𝑁,𝑐,π‘˜,𝑛,π‘Ÿ,𝑑,π‘₯,𝑦,𝑧   πœ‘,𝑐,π‘˜,𝑛,π‘Ÿ,𝑑,π‘₯,𝑦   𝑇,𝑐,π‘˜,𝑛,π‘Ÿ,𝑑,π‘₯,𝑦,𝑧   π‘ˆ,𝑐,𝑛,π‘Ÿ,𝑑,π‘₯,𝑦,𝑧   π‘Š,𝑐,𝑛,π‘Ÿ,𝑑,π‘₯,𝑦   𝑋,𝑐,π‘˜,𝑛,π‘Ÿ,𝑑,π‘₯,𝑦,𝑧
Allowed substitution hints:   πœ‘(𝑧)   𝐴(𝑑)   𝐷(𝑦)   π‘ˆ(π‘˜)   𝐽(𝑧,π‘Ÿ,𝑐)   π‘Š(𝑧,π‘˜)

Proof of Theorem ubthlem1
StepHypRef Expression
1 rzal 4507 . . . . . . . . 9 (𝑇 = βˆ… β†’ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜)
21ralrimivw 3148 . . . . . . . 8 (𝑇 = βˆ… β†’ βˆ€π‘§ ∈ 𝑋 βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜)
3 rabid2 3462 . . . . . . . 8 (𝑋 = {𝑧 ∈ 𝑋 ∣ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} ↔ βˆ€π‘§ ∈ 𝑋 βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜)
42, 3sylibr 233 . . . . . . 7 (𝑇 = βˆ… β†’ 𝑋 = {𝑧 ∈ 𝑋 ∣ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜})
54eqcomd 2736 . . . . . 6 (𝑇 = βˆ… β†’ {𝑧 ∈ 𝑋 ∣ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} = 𝑋)
65eleq1d 2816 . . . . 5 (𝑇 = βˆ… β†’ ({𝑧 ∈ 𝑋 ∣ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} ∈ (Clsdβ€˜π½) ↔ 𝑋 ∈ (Clsdβ€˜π½)))
7 iinrab 5071 . . . . . . 7 (𝑇 β‰  βˆ… β†’ ∩ 𝑑 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} = {𝑧 ∈ 𝑋 ∣ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜})
87adantl 480 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑇 β‰  βˆ…) β†’ ∩ 𝑑 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} = {𝑧 ∈ 𝑋 ∣ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜})
9 id 22 . . . . . . 7 (𝑇 β‰  βˆ… β†’ 𝑇 β‰  βˆ…)
10 ubthlem.7 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑇 βŠ† (π‘ˆ BLnOp π‘Š))
1110sselda 3981 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ 𝑑 ∈ (π‘ˆ BLnOp π‘Š))
12 ubthlem.3 . . . . . . . . . . . . . . . . . . . 20 𝐷 = (IndMetβ€˜π‘ˆ)
13 eqid 2730 . . . . . . . . . . . . . . . . . . . 20 (IndMetβ€˜π‘Š) = (IndMetβ€˜π‘Š)
14 ubthlem.4 . . . . . . . . . . . . . . . . . . . 20 𝐽 = (MetOpenβ€˜π·)
15 eqid 2730 . . . . . . . . . . . . . . . . . . . 20 (MetOpenβ€˜(IndMetβ€˜π‘Š)) = (MetOpenβ€˜(IndMetβ€˜π‘Š))
16 eqid 2730 . . . . . . . . . . . . . . . . . . . 20 (π‘ˆ BLnOp π‘Š) = (π‘ˆ BLnOp π‘Š)
17 ubthlem.5 . . . . . . . . . . . . . . . . . . . . 21 π‘ˆ ∈ CBan
18 bnnv 30386 . . . . . . . . . . . . . . . . . . . . 21 (π‘ˆ ∈ CBan β†’ π‘ˆ ∈ NrmCVec)
1917, 18ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 π‘ˆ ∈ NrmCVec
20 ubthlem.6 . . . . . . . . . . . . . . . . . . . 20 π‘Š ∈ NrmCVec
2112, 13, 14, 15, 16, 19, 20blocn2 30328 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ (π‘ˆ BLnOp π‘Š) β†’ 𝑑 ∈ (𝐽 Cn (MetOpenβ€˜(IndMetβ€˜π‘Š))))
22 ubth.1 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑋 = (BaseSetβ€˜π‘ˆ)
2322, 12cbncms 30385 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘ˆ ∈ CBan β†’ 𝐷 ∈ (CMetβ€˜π‘‹))
2417, 23ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 𝐷 ∈ (CMetβ€˜π‘‹)
25 cmetmet 25034 . . . . . . . . . . . . . . . . . . . . . 22 (𝐷 ∈ (CMetβ€˜π‘‹) β†’ 𝐷 ∈ (Metβ€˜π‘‹))
26 metxmet 24060 . . . . . . . . . . . . . . . . . . . . . 22 (𝐷 ∈ (Metβ€˜π‘‹) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
2724, 25, 26mp2b 10 . . . . . . . . . . . . . . . . . . . . 21 𝐷 ∈ (∞Metβ€˜π‘‹)
2814mopntopon 24165 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∈ (∞Metβ€˜π‘‹) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
2927, 28ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 𝐽 ∈ (TopOnβ€˜π‘‹)
30 eqid 2730 . . . . . . . . . . . . . . . . . . . . . . 23 (BaseSetβ€˜π‘Š) = (BaseSetβ€˜π‘Š)
3130, 13imsxmet 30212 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Š ∈ NrmCVec β†’ (IndMetβ€˜π‘Š) ∈ (∞Metβ€˜(BaseSetβ€˜π‘Š)))
3220, 31ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (IndMetβ€˜π‘Š) ∈ (∞Metβ€˜(BaseSetβ€˜π‘Š))
3315mopntopon 24165 . . . . . . . . . . . . . . . . . . . . 21 ((IndMetβ€˜π‘Š) ∈ (∞Metβ€˜(BaseSetβ€˜π‘Š)) β†’ (MetOpenβ€˜(IndMetβ€˜π‘Š)) ∈ (TopOnβ€˜(BaseSetβ€˜π‘Š)))
3432, 33ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (MetOpenβ€˜(IndMetβ€˜π‘Š)) ∈ (TopOnβ€˜(BaseSetβ€˜π‘Š))
35 iscncl 22993 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (MetOpenβ€˜(IndMetβ€˜π‘Š)) ∈ (TopOnβ€˜(BaseSetβ€˜π‘Š))) β†’ (𝑑 ∈ (𝐽 Cn (MetOpenβ€˜(IndMetβ€˜π‘Š))) ↔ (𝑑:π‘‹βŸΆ(BaseSetβ€˜π‘Š) ∧ βˆ€π‘₯ ∈ (Clsdβ€˜(MetOpenβ€˜(IndMetβ€˜π‘Š)))(◑𝑑 β€œ π‘₯) ∈ (Clsdβ€˜π½))))
3629, 34, 35mp2an 688 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ (𝐽 Cn (MetOpenβ€˜(IndMetβ€˜π‘Š))) ↔ (𝑑:π‘‹βŸΆ(BaseSetβ€˜π‘Š) ∧ βˆ€π‘₯ ∈ (Clsdβ€˜(MetOpenβ€˜(IndMetβ€˜π‘Š)))(◑𝑑 β€œ π‘₯) ∈ (Clsdβ€˜π½)))
3721, 36sylib 217 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ (π‘ˆ BLnOp π‘Š) β†’ (𝑑:π‘‹βŸΆ(BaseSetβ€˜π‘Š) ∧ βˆ€π‘₯ ∈ (Clsdβ€˜(MetOpenβ€˜(IndMetβ€˜π‘Š)))(◑𝑑 β€œ π‘₯) ∈ (Clsdβ€˜π½)))
3811, 37syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (𝑑:π‘‹βŸΆ(BaseSetβ€˜π‘Š) ∧ βˆ€π‘₯ ∈ (Clsdβ€˜(MetOpenβ€˜(IndMetβ€˜π‘Š)))(◑𝑑 β€œ π‘₯) ∈ (Clsdβ€˜π½)))
3938simpld 493 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ 𝑑:π‘‹βŸΆ(BaseSetβ€˜π‘Š))
4039adantlr 711 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑑 ∈ 𝑇) β†’ 𝑑:π‘‹βŸΆ(BaseSetβ€˜π‘Š))
4140ffvelcdmda 7085 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑑 ∈ 𝑇) ∧ π‘₯ ∈ 𝑋) β†’ (π‘‘β€˜π‘₯) ∈ (BaseSetβ€˜π‘Š))
4241biantrurd 531 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑑 ∈ 𝑇) ∧ π‘₯ ∈ 𝑋) β†’ ((π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜ ↔ ((π‘‘β€˜π‘₯) ∈ (BaseSetβ€˜π‘Š) ∧ (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜)))
43 fveq2 6890 . . . . . . . . . . . . . . 15 (𝑦 = (π‘‘β€˜π‘₯) β†’ (π‘β€˜π‘¦) = (π‘β€˜(π‘‘β€˜π‘₯)))
4443breq1d 5157 . . . . . . . . . . . . . 14 (𝑦 = (π‘‘β€˜π‘₯) β†’ ((π‘β€˜π‘¦) ≀ π‘˜ ↔ (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜))
4544elrab 3682 . . . . . . . . . . . . 13 ((π‘‘β€˜π‘₯) ∈ {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜} ↔ ((π‘‘β€˜π‘₯) ∈ (BaseSetβ€˜π‘Š) ∧ (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜))
4642, 45bitr4di 288 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑑 ∈ 𝑇) ∧ π‘₯ ∈ 𝑋) β†’ ((π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜ ↔ (π‘‘β€˜π‘₯) ∈ {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜}))
4746pm5.32da 577 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑑 ∈ 𝑇) β†’ ((π‘₯ ∈ 𝑋 ∧ (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜) ↔ (π‘₯ ∈ 𝑋 ∧ (π‘‘β€˜π‘₯) ∈ {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜})))
48 2fveq3 6895 . . . . . . . . . . . . . 14 (𝑧 = π‘₯ β†’ (π‘β€˜(π‘‘β€˜π‘§)) = (π‘β€˜(π‘‘β€˜π‘₯)))
4948breq1d 5157 . . . . . . . . . . . . 13 (𝑧 = π‘₯ β†’ ((π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜ ↔ (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜))
5049elrab 3682 . . . . . . . . . . . 12 (π‘₯ ∈ {𝑧 ∈ 𝑋 ∣ (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} ↔ (π‘₯ ∈ 𝑋 ∧ (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜))
5150a1i 11 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑑 ∈ 𝑇) β†’ (π‘₯ ∈ {𝑧 ∈ 𝑋 ∣ (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} ↔ (π‘₯ ∈ 𝑋 ∧ (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜)))
52 ffn 6716 . . . . . . . . . . . 12 (𝑑:π‘‹βŸΆ(BaseSetβ€˜π‘Š) β†’ 𝑑 Fn 𝑋)
53 elpreima 7058 . . . . . . . . . . . 12 (𝑑 Fn 𝑋 β†’ (π‘₯ ∈ (◑𝑑 β€œ {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜}) ↔ (π‘₯ ∈ 𝑋 ∧ (π‘‘β€˜π‘₯) ∈ {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜})))
5440, 52, 533syl 18 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑑 ∈ 𝑇) β†’ (π‘₯ ∈ (◑𝑑 β€œ {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜}) ↔ (π‘₯ ∈ 𝑋 ∧ (π‘‘β€˜π‘₯) ∈ {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜})))
5547, 51, 543bitr4d 310 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑑 ∈ 𝑇) β†’ (π‘₯ ∈ {𝑧 ∈ 𝑋 ∣ (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} ↔ π‘₯ ∈ (◑𝑑 β€œ {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜})))
5655eqrdv 2728 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑑 ∈ 𝑇) β†’ {𝑧 ∈ 𝑋 ∣ (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} = (◑𝑑 β€œ {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜}))
57 imaeq2 6054 . . . . . . . . . . 11 (π‘₯ = {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜} β†’ (◑𝑑 β€œ π‘₯) = (◑𝑑 β€œ {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜}))
5857eleq1d 2816 . . . . . . . . . 10 (π‘₯ = {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜} β†’ ((◑𝑑 β€œ π‘₯) ∈ (Clsdβ€˜π½) ↔ (◑𝑑 β€œ {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜}) ∈ (Clsdβ€˜π½)))
5938simprd 494 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ βˆ€π‘₯ ∈ (Clsdβ€˜(MetOpenβ€˜(IndMetβ€˜π‘Š)))(◑𝑑 β€œ π‘₯) ∈ (Clsdβ€˜π½))
6059adantlr 711 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑑 ∈ 𝑇) β†’ βˆ€π‘₯ ∈ (Clsdβ€˜(MetOpenβ€˜(IndMetβ€˜π‘Š)))(◑𝑑 β€œ π‘₯) ∈ (Clsdβ€˜π½))
61 nnre 12223 . . . . . . . . . . . . 13 (π‘˜ ∈ β„• β†’ π‘˜ ∈ ℝ)
6261ad2antlr 723 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑑 ∈ 𝑇) β†’ π‘˜ ∈ ℝ)
6362rexrd 11268 . . . . . . . . . . 11 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑑 ∈ 𝑇) β†’ π‘˜ ∈ ℝ*)
64 eqid 2730 . . . . . . . . . . . . . 14 (0vecβ€˜π‘Š) = (0vecβ€˜π‘Š)
6530, 64nvzcl 30154 . . . . . . . . . . . . 13 (π‘Š ∈ NrmCVec β†’ (0vecβ€˜π‘Š) ∈ (BaseSetβ€˜π‘Š))
6620, 65ax-mp 5 . . . . . . . . . . . 12 (0vecβ€˜π‘Š) ∈ (BaseSetβ€˜π‘Š)
67 ubth.2 . . . . . . . . . . . . . . . . . 18 𝑁 = (normCVβ€˜π‘Š)
6830, 64, 67, 13nvnd 30208 . . . . . . . . . . . . . . . . 17 ((π‘Š ∈ NrmCVec ∧ 𝑦 ∈ (BaseSetβ€˜π‘Š)) β†’ (π‘β€˜π‘¦) = (𝑦(IndMetβ€˜π‘Š)(0vecβ€˜π‘Š)))
6920, 68mpan 686 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (BaseSetβ€˜π‘Š) β†’ (π‘β€˜π‘¦) = (𝑦(IndMetβ€˜π‘Š)(0vecβ€˜π‘Š)))
70 xmetsym 24073 . . . . . . . . . . . . . . . . 17 (((IndMetβ€˜π‘Š) ∈ (∞Metβ€˜(BaseSetβ€˜π‘Š)) ∧ (0vecβ€˜π‘Š) ∈ (BaseSetβ€˜π‘Š) ∧ 𝑦 ∈ (BaseSetβ€˜π‘Š)) β†’ ((0vecβ€˜π‘Š)(IndMetβ€˜π‘Š)𝑦) = (𝑦(IndMetβ€˜π‘Š)(0vecβ€˜π‘Š)))
7132, 66, 70mp3an12 1449 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (BaseSetβ€˜π‘Š) β†’ ((0vecβ€˜π‘Š)(IndMetβ€˜π‘Š)𝑦) = (𝑦(IndMetβ€˜π‘Š)(0vecβ€˜π‘Š)))
7269, 71eqtr4d 2773 . . . . . . . . . . . . . . 15 (𝑦 ∈ (BaseSetβ€˜π‘Š) β†’ (π‘β€˜π‘¦) = ((0vecβ€˜π‘Š)(IndMetβ€˜π‘Š)𝑦))
7372breq1d 5157 . . . . . . . . . . . . . 14 (𝑦 ∈ (BaseSetβ€˜π‘Š) β†’ ((π‘β€˜π‘¦) ≀ π‘˜ ↔ ((0vecβ€˜π‘Š)(IndMetβ€˜π‘Š)𝑦) ≀ π‘˜))
7473rabbiia 3434 . . . . . . . . . . . . 13 {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜} = {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ ((0vecβ€˜π‘Š)(IndMetβ€˜π‘Š)𝑦) ≀ π‘˜}
7515, 74blcld 24234 . . . . . . . . . . . 12 (((IndMetβ€˜π‘Š) ∈ (∞Metβ€˜(BaseSetβ€˜π‘Š)) ∧ (0vecβ€˜π‘Š) ∈ (BaseSetβ€˜π‘Š) ∧ π‘˜ ∈ ℝ*) β†’ {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜} ∈ (Clsdβ€˜(MetOpenβ€˜(IndMetβ€˜π‘Š))))
7632, 66, 75mp3an12 1449 . . . . . . . . . . 11 (π‘˜ ∈ ℝ* β†’ {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜} ∈ (Clsdβ€˜(MetOpenβ€˜(IndMetβ€˜π‘Š))))
7763, 76syl 17 . . . . . . . . . 10 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑑 ∈ 𝑇) β†’ {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜} ∈ (Clsdβ€˜(MetOpenβ€˜(IndMetβ€˜π‘Š))))
7858, 60, 77rspcdva 3612 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑑 ∈ 𝑇) β†’ (◑𝑑 β€œ {𝑦 ∈ (BaseSetβ€˜π‘Š) ∣ (π‘β€˜π‘¦) ≀ π‘˜}) ∈ (Clsdβ€˜π½))
7956, 78eqeltrd 2831 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑑 ∈ 𝑇) β†’ {𝑧 ∈ 𝑋 ∣ (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} ∈ (Clsdβ€˜π½))
8079ralrimiva 3144 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ βˆ€π‘‘ ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} ∈ (Clsdβ€˜π½))
81 iincld 22763 . . . . . . 7 ((𝑇 β‰  βˆ… ∧ βˆ€π‘‘ ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} ∈ (Clsdβ€˜π½)) β†’ ∩ 𝑑 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} ∈ (Clsdβ€˜π½))
829, 80, 81syl2anr 595 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑇 β‰  βˆ…) β†’ ∩ 𝑑 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} ∈ (Clsdβ€˜π½))
838, 82eqeltrrd 2832 . . . . 5 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑇 β‰  βˆ…) β†’ {𝑧 ∈ 𝑋 ∣ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} ∈ (Clsdβ€˜π½))
8414mopntop 24166 . . . . . . . 8 (𝐷 ∈ (∞Metβ€˜π‘‹) β†’ 𝐽 ∈ Top)
8527, 84ax-mp 5 . . . . . . 7 𝐽 ∈ Top
8629toponunii 22638 . . . . . . . 8 𝑋 = βˆͺ 𝐽
8786topcld 22759 . . . . . . 7 (𝐽 ∈ Top β†’ 𝑋 ∈ (Clsdβ€˜π½))
8885, 87ax-mp 5 . . . . . 6 𝑋 ∈ (Clsdβ€˜π½)
8988a1i 11 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝑋 ∈ (Clsdβ€˜π½))
906, 83, 89pm2.61ne 3025 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ {𝑧 ∈ 𝑋 ∣ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} ∈ (Clsdβ€˜π½))
91 ubthlem.9 . . . 4 𝐴 = (π‘˜ ∈ β„• ↦ {𝑧 ∈ 𝑋 ∣ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜})
9290, 91fmptd 7114 . . 3 (πœ‘ β†’ 𝐴:β„•βŸΆ(Clsdβ€˜π½))
9392frnd 6724 . . . . . 6 (πœ‘ β†’ ran 𝐴 βŠ† (Clsdβ€˜π½))
9486cldss2 22754 . . . . . 6 (Clsdβ€˜π½) βŠ† 𝒫 𝑋
9593, 94sstrdi 3993 . . . . 5 (πœ‘ β†’ ran 𝐴 βŠ† 𝒫 𝑋)
96 sspwuni 5102 . . . . 5 (ran 𝐴 βŠ† 𝒫 𝑋 ↔ βˆͺ ran 𝐴 βŠ† 𝑋)
9795, 96sylib 217 . . . 4 (πœ‘ β†’ βˆͺ ran 𝐴 βŠ† 𝑋)
98 ubthlem.8 . . . . . 6 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘ ∈ ℝ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ 𝑐)
99 arch 12473 . . . . . . . . . 10 (𝑐 ∈ ℝ β†’ βˆƒπ‘˜ ∈ β„• 𝑐 < π‘˜)
10099adantl 480 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) β†’ βˆƒπ‘˜ ∈ β„• 𝑐 < π‘˜)
101 simpr 483 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) β†’ 𝑐 ∈ ℝ)
102 ltle 11306 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ ℝ ∧ π‘˜ ∈ ℝ) β†’ (𝑐 < π‘˜ β†’ 𝑐 ≀ π‘˜))
103101, 61, 102syl2an 594 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ π‘˜ ∈ β„•) β†’ (𝑐 < π‘˜ β†’ 𝑐 ≀ π‘˜))
104103impr 453 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (π‘˜ ∈ β„• ∧ 𝑐 < π‘˜)) β†’ 𝑐 ≀ π‘˜)
105104adantr 479 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (π‘˜ ∈ β„• ∧ 𝑐 < π‘˜)) ∧ 𝑑 ∈ 𝑇) β†’ 𝑐 ≀ π‘˜)
10639ffvelcdmda 7085 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑑 ∈ 𝑇) ∧ π‘₯ ∈ 𝑋) β†’ (π‘‘β€˜π‘₯) ∈ (BaseSetβ€˜π‘Š))
107106an32s 648 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑑 ∈ 𝑇) β†’ (π‘‘β€˜π‘₯) ∈ (BaseSetβ€˜π‘Š))
10830, 67nvcl 30181 . . . . . . . . . . . . . . . . . 18 ((π‘Š ∈ NrmCVec ∧ (π‘‘β€˜π‘₯) ∈ (BaseSetβ€˜π‘Š)) β†’ (π‘β€˜(π‘‘β€˜π‘₯)) ∈ ℝ)
10920, 107, 108sylancr 585 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑑 ∈ 𝑇) β†’ (π‘β€˜(π‘‘β€˜π‘₯)) ∈ ℝ)
110109adantlr 711 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑑 ∈ 𝑇) β†’ (π‘β€˜(π‘‘β€˜π‘₯)) ∈ ℝ)
111110adantlr 711 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (π‘˜ ∈ β„• ∧ 𝑐 < π‘˜)) ∧ 𝑑 ∈ 𝑇) β†’ (π‘β€˜(π‘‘β€˜π‘₯)) ∈ ℝ)
112 simpllr 772 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (π‘˜ ∈ β„• ∧ 𝑐 < π‘˜)) ∧ 𝑑 ∈ 𝑇) β†’ 𝑐 ∈ ℝ)
113 simplrl 773 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (π‘˜ ∈ β„• ∧ 𝑐 < π‘˜)) ∧ 𝑑 ∈ 𝑇) β†’ π‘˜ ∈ β„•)
114113, 61syl 17 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (π‘˜ ∈ β„• ∧ 𝑐 < π‘˜)) ∧ 𝑑 ∈ 𝑇) β†’ π‘˜ ∈ ℝ)
115 letr 11312 . . . . . . . . . . . . . . 15 (((π‘β€˜(π‘‘β€˜π‘₯)) ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ π‘˜ ∈ ℝ) β†’ (((π‘β€˜(π‘‘β€˜π‘₯)) ≀ 𝑐 ∧ 𝑐 ≀ π‘˜) β†’ (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜))
116111, 112, 114, 115syl3anc 1369 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (π‘˜ ∈ β„• ∧ 𝑐 < π‘˜)) ∧ 𝑑 ∈ 𝑇) β†’ (((π‘β€˜(π‘‘β€˜π‘₯)) ≀ 𝑐 ∧ 𝑐 ≀ π‘˜) β†’ (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜))
117105, 116mpan2d 690 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (π‘˜ ∈ β„• ∧ 𝑐 < π‘˜)) ∧ 𝑑 ∈ 𝑇) β†’ ((π‘β€˜(π‘‘β€˜π‘₯)) ≀ 𝑐 β†’ (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜))
118117ralimdva 3165 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (π‘˜ ∈ β„• ∧ 𝑐 < π‘˜)) β†’ (βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ 𝑐 β†’ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜))
119118expr 455 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ π‘˜ ∈ β„•) β†’ (𝑐 < π‘˜ β†’ (βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ 𝑐 β†’ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜)))
12022fvexi 6904 . . . . . . . . . . . . . . . . . 18 𝑋 ∈ V
121120rabex 5331 . . . . . . . . . . . . . . . . 17 {𝑧 ∈ 𝑋 ∣ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} ∈ V
12291fvmpt2 7008 . . . . . . . . . . . . . . . . 17 ((π‘˜ ∈ β„• ∧ {𝑧 ∈ 𝑋 ∣ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} ∈ V) β†’ (π΄β€˜π‘˜) = {𝑧 ∈ 𝑋 ∣ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜})
123121, 122mpan2 687 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„• β†’ (π΄β€˜π‘˜) = {𝑧 ∈ 𝑋 ∣ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜})
124123eleq2d 2817 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„• β†’ (π‘₯ ∈ (π΄β€˜π‘˜) ↔ π‘₯ ∈ {𝑧 ∈ 𝑋 ∣ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜}))
12549ralbidv 3175 . . . . . . . . . . . . . . . 16 (𝑧 = π‘₯ β†’ (βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜ ↔ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜))
126125elrab 3682 . . . . . . . . . . . . . . 15 (π‘₯ ∈ {𝑧 ∈ 𝑋 ∣ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘§)) ≀ π‘˜} ↔ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜))
127124, 126bitrdi 286 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„• β†’ (π‘₯ ∈ (π΄β€˜π‘˜) ↔ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜)))
128 simpr 483 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ π‘₯ ∈ 𝑋)
129128biantrurd 531 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜ ↔ (π‘₯ ∈ 𝑋 ∧ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜)))
130129bicomd 222 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ∧ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜) ↔ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜))
131127, 130sylan9bbr 509 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ π‘˜ ∈ β„•) β†’ (π‘₯ ∈ (π΄β€˜π‘˜) ↔ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜))
13292ffnd 6717 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐴 Fn β„•)
133132adantr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐴 Fn β„•)
134 fnfvelrn 7081 . . . . . . . . . . . . . . . 16 ((𝐴 Fn β„• ∧ π‘˜ ∈ β„•) β†’ (π΄β€˜π‘˜) ∈ ran 𝐴)
135 elssuni 4940 . . . . . . . . . . . . . . . 16 ((π΄β€˜π‘˜) ∈ ran 𝐴 β†’ (π΄β€˜π‘˜) βŠ† βˆͺ ran 𝐴)
136134, 135syl 17 . . . . . . . . . . . . . . 15 ((𝐴 Fn β„• ∧ π‘˜ ∈ β„•) β†’ (π΄β€˜π‘˜) βŠ† βˆͺ ran 𝐴)
137136sseld 3980 . . . . . . . . . . . . . 14 ((𝐴 Fn β„• ∧ π‘˜ ∈ β„•) β†’ (π‘₯ ∈ (π΄β€˜π‘˜) β†’ π‘₯ ∈ βˆͺ ran 𝐴))
138133, 137sylan 578 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ π‘˜ ∈ β„•) β†’ (π‘₯ ∈ (π΄β€˜π‘˜) β†’ π‘₯ ∈ βˆͺ ran 𝐴))
139131, 138sylbird 259 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ π‘˜ ∈ β„•) β†’ (βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜ β†’ π‘₯ ∈ βˆͺ ran 𝐴))
140139adantlr 711 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ π‘˜ ∈ β„•) β†’ (βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ π‘˜ β†’ π‘₯ ∈ βˆͺ ran 𝐴))
141119, 140syl6d 75 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ π‘˜ ∈ β„•) β†’ (𝑐 < π‘˜ β†’ (βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ 𝑐 β†’ π‘₯ ∈ βˆͺ ran 𝐴)))
142141rexlimdva 3153 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) β†’ (βˆƒπ‘˜ ∈ β„• 𝑐 < π‘˜ β†’ (βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ 𝑐 β†’ π‘₯ ∈ βˆͺ ran 𝐴)))
143100, 142mpd 15 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑐 ∈ ℝ) β†’ (βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ 𝑐 β†’ π‘₯ ∈ βˆͺ ran 𝐴))
144143rexlimdva 3153 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (βˆƒπ‘ ∈ ℝ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ 𝑐 β†’ π‘₯ ∈ βˆͺ ran 𝐴))
145144ralimdva 3165 . . . . . 6 (πœ‘ β†’ (βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘ ∈ ℝ βˆ€π‘‘ ∈ 𝑇 (π‘β€˜(π‘‘β€˜π‘₯)) ≀ 𝑐 β†’ βˆ€π‘₯ ∈ 𝑋 π‘₯ ∈ βˆͺ ran 𝐴))
14698, 145mpd 15 . . . . 5 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 π‘₯ ∈ βˆͺ ran 𝐴)
147 dfss3 3969 . . . . 5 (𝑋 βŠ† βˆͺ ran 𝐴 ↔ βˆ€π‘₯ ∈ 𝑋 π‘₯ ∈ βˆͺ ran 𝐴)
148146, 147sylibr 233 . . . 4 (πœ‘ β†’ 𝑋 βŠ† βˆͺ ran 𝐴)
14997, 148eqssd 3998 . . 3 (πœ‘ β†’ βˆͺ ran 𝐴 = 𝑋)
150 eqid 2730 . . . . . 6 (0vecβ€˜π‘ˆ) = (0vecβ€˜π‘ˆ)
15122, 150nvzcl 30154 . . . . 5 (π‘ˆ ∈ NrmCVec β†’ (0vecβ€˜π‘ˆ) ∈ 𝑋)
152 ne0i 4333 . . . . 5 ((0vecβ€˜π‘ˆ) ∈ 𝑋 β†’ 𝑋 β‰  βˆ…)
15319, 151, 152mp2b 10 . . . 4 𝑋 β‰  βˆ…
15414bcth2 25078 . . . 4 (((𝐷 ∈ (CMetβ€˜π‘‹) ∧ 𝑋 β‰  βˆ…) ∧ (𝐴:β„•βŸΆ(Clsdβ€˜π½) ∧ βˆͺ ran 𝐴 = 𝑋)) β†’ βˆƒπ‘› ∈ β„• ((intβ€˜π½)β€˜(π΄β€˜π‘›)) β‰  βˆ…)
15524, 153, 154mpanl12 698 . . 3 ((𝐴:β„•βŸΆ(Clsdβ€˜π½) ∧ βˆͺ ran 𝐴 = 𝑋) β†’ βˆƒπ‘› ∈ β„• ((intβ€˜π½)β€˜(π΄β€˜π‘›)) β‰  βˆ…)
15692, 149, 155syl2anc 582 . 2 (πœ‘ β†’ βˆƒπ‘› ∈ β„• ((intβ€˜π½)β€˜(π΄β€˜π‘›)) β‰  βˆ…)
157 ffvelcdm 7082 . . . . . . . . . . 11 ((𝐴:β„•βŸΆ(Clsdβ€˜π½) ∧ 𝑛 ∈ β„•) β†’ (π΄β€˜π‘›) ∈ (Clsdβ€˜π½))
15894, 157sselid 3979 . . . . . . . . . 10 ((𝐴:β„•βŸΆ(Clsdβ€˜π½) ∧ 𝑛 ∈ β„•) β†’ (π΄β€˜π‘›) ∈ 𝒫 𝑋)
159158elpwid 4610 . . . . . . . . 9 ((𝐴:β„•βŸΆ(Clsdβ€˜π½) ∧ 𝑛 ∈ β„•) β†’ (π΄β€˜π‘›) βŠ† 𝑋)
16092, 159sylan 578 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (π΄β€˜π‘›) βŠ† 𝑋)
16186ntrss3 22784 . . . . . . . 8 ((𝐽 ∈ Top ∧ (π΄β€˜π‘›) βŠ† 𝑋) β†’ ((intβ€˜π½)β€˜(π΄β€˜π‘›)) βŠ† 𝑋)
16285, 160, 161sylancr 585 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((intβ€˜π½)β€˜(π΄β€˜π‘›)) βŠ† 𝑋)
163162sseld 3980 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑦 ∈ ((intβ€˜π½)β€˜(π΄β€˜π‘›)) β†’ 𝑦 ∈ 𝑋))
16486ntropn 22773 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ (π΄β€˜π‘›) βŠ† 𝑋) β†’ ((intβ€˜π½)β€˜(π΄β€˜π‘›)) ∈ 𝐽)
16585, 160, 164sylancr 585 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((intβ€˜π½)β€˜(π΄β€˜π‘›)) ∈ 𝐽)
16614mopni2 24222 . . . . . . . . . 10 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ ((intβ€˜π½)β€˜(π΄β€˜π‘›)) ∈ 𝐽 ∧ 𝑦 ∈ ((intβ€˜π½)β€˜(π΄β€˜π‘›))) β†’ βˆƒπ‘₯ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘₯) βŠ† ((intβ€˜π½)β€˜(π΄β€˜π‘›)))
16727, 166mp3an1 1446 . . . . . . . . 9 ((((intβ€˜π½)β€˜(π΄β€˜π‘›)) ∈ 𝐽 ∧ 𝑦 ∈ ((intβ€˜π½)β€˜(π΄β€˜π‘›))) β†’ βˆƒπ‘₯ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘₯) βŠ† ((intβ€˜π½)β€˜(π΄β€˜π‘›)))
168165, 167sylan 578 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑦 ∈ ((intβ€˜π½)β€˜(π΄β€˜π‘›))) β†’ βˆƒπ‘₯ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘₯) βŠ† ((intβ€˜π½)β€˜(π΄β€˜π‘›)))
169 elssuni 4940 . . . . . . . . . . . 12 (((intβ€˜π½)β€˜(π΄β€˜π‘›)) ∈ 𝐽 β†’ ((intβ€˜π½)β€˜(π΄β€˜π‘›)) βŠ† βˆͺ 𝐽)
170169, 86sseqtrrdi 4032 . . . . . . . . . . 11 (((intβ€˜π½)β€˜(π΄β€˜π‘›)) ∈ 𝐽 β†’ ((intβ€˜π½)β€˜(π΄β€˜π‘›)) βŠ† 𝑋)
171165, 170syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((intβ€˜π½)β€˜(π΄β€˜π‘›)) βŠ† 𝑋)
172171sselda 3981 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑦 ∈ ((intβ€˜π½)β€˜(π΄β€˜π‘›))) β†’ 𝑦 ∈ 𝑋)
17386ntrss2 22781 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ (π΄β€˜π‘›) βŠ† 𝑋) β†’ ((intβ€˜π½)β€˜(π΄β€˜π‘›)) βŠ† (π΄β€˜π‘›))
17485, 160, 173sylancr 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((intβ€˜π½)β€˜(π΄β€˜π‘›)) βŠ† (π΄β€˜π‘›))
175 sstr2 3988 . . . . . . . . . . . . 13 ((𝑦(ballβ€˜π·)π‘₯) βŠ† ((intβ€˜π½)β€˜(π΄β€˜π‘›)) β†’ (((intβ€˜π½)β€˜(π΄β€˜π‘›)) βŠ† (π΄β€˜π‘›) β†’ (𝑦(ballβ€˜π·)π‘₯) βŠ† (π΄β€˜π‘›)))
176174, 175syl5com 31 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((𝑦(ballβ€˜π·)π‘₯) βŠ† ((intβ€˜π½)β€˜(π΄β€˜π‘›)) β†’ (𝑦(ballβ€˜π·)π‘₯) βŠ† (π΄β€˜π‘›)))
177176ad2antrr 722 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑦 ∈ 𝑋) ∧ π‘₯ ∈ ℝ+) β†’ ((𝑦(ballβ€˜π·)π‘₯) βŠ† ((intβ€˜π½)β€˜(π΄β€˜π‘›)) β†’ (𝑦(ballβ€˜π·)π‘₯) βŠ† (π΄β€˜π‘›)))
178 simpr 483 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑦 ∈ 𝑋) β†’ 𝑦 ∈ 𝑋)
179178, 27jctil 518 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑦 ∈ 𝑋) β†’ (𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋))
180 rphalfcl 13005 . . . . . . . . . . . . . . 15 (π‘₯ ∈ ℝ+ β†’ (π‘₯ / 2) ∈ ℝ+)
181180rpxrd 13021 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ+ β†’ (π‘₯ / 2) ∈ ℝ*)
182 rpxr 12987 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ+ β†’ π‘₯ ∈ ℝ*)
183 rphalflt 13007 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ+ β†’ (π‘₯ / 2) < π‘₯)
184181, 182, 1833jca 1126 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ+ β†’ ((π‘₯ / 2) ∈ ℝ* ∧ π‘₯ ∈ ℝ* ∧ (π‘₯ / 2) < π‘₯))
185 eqid 2730 . . . . . . . . . . . . . 14 {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ (π‘₯ / 2)} = {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ (π‘₯ / 2)}
18614, 185blsscls2 24233 . . . . . . . . . . . . 13 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋) ∧ ((π‘₯ / 2) ∈ ℝ* ∧ π‘₯ ∈ ℝ* ∧ (π‘₯ / 2) < π‘₯)) β†’ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ (π‘₯ / 2)} βŠ† (𝑦(ballβ€˜π·)π‘₯))
187179, 184, 186syl2an 594 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑦 ∈ 𝑋) ∧ π‘₯ ∈ ℝ+) β†’ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ (π‘₯ / 2)} βŠ† (𝑦(ballβ€˜π·)π‘₯))
188 sstr2 3988 . . . . . . . . . . . 12 ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ (π‘₯ / 2)} βŠ† (𝑦(ballβ€˜π·)π‘₯) β†’ ((𝑦(ballβ€˜π·)π‘₯) βŠ† (π΄β€˜π‘›) β†’ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ (π‘₯ / 2)} βŠ† (π΄β€˜π‘›)))
189187, 188syl 17 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑦 ∈ 𝑋) ∧ π‘₯ ∈ ℝ+) β†’ ((𝑦(ballβ€˜π·)π‘₯) βŠ† (π΄β€˜π‘›) β†’ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ (π‘₯ / 2)} βŠ† (π΄β€˜π‘›)))
190180adantl 480 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑦 ∈ 𝑋) ∧ π‘₯ ∈ ℝ+) β†’ (π‘₯ / 2) ∈ ℝ+)
191 breq2 5151 . . . . . . . . . . . . . . . 16 (π‘Ÿ = (π‘₯ / 2) β†’ ((𝑦𝐷𝑧) ≀ π‘Ÿ ↔ (𝑦𝐷𝑧) ≀ (π‘₯ / 2)))
192191rabbidv 3438 . . . . . . . . . . . . . . 15 (π‘Ÿ = (π‘₯ / 2) β†’ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} = {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ (π‘₯ / 2)})
193192sseq1d 4012 . . . . . . . . . . . . . 14 (π‘Ÿ = (π‘₯ / 2) β†’ ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›) ↔ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ (π‘₯ / 2)} βŠ† (π΄β€˜π‘›)))
194193rspcev 3611 . . . . . . . . . . . . 13 (((π‘₯ / 2) ∈ ℝ+ ∧ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ (π‘₯ / 2)} βŠ† (π΄β€˜π‘›)) β†’ βˆƒπ‘Ÿ ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›))
195194ex 411 . . . . . . . . . . . 12 ((π‘₯ / 2) ∈ ℝ+ β†’ ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ (π‘₯ / 2)} βŠ† (π΄β€˜π‘›) β†’ βˆƒπ‘Ÿ ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›)))
196190, 195syl 17 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑦 ∈ 𝑋) ∧ π‘₯ ∈ ℝ+) β†’ ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ (π‘₯ / 2)} βŠ† (π΄β€˜π‘›) β†’ βˆƒπ‘Ÿ ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›)))
197177, 189, 1963syld 60 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑦 ∈ 𝑋) ∧ π‘₯ ∈ ℝ+) β†’ ((𝑦(ballβ€˜π·)π‘₯) βŠ† ((intβ€˜π½)β€˜(π΄β€˜π‘›)) β†’ βˆƒπ‘Ÿ ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›)))
198197rexlimdva 3153 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑦 ∈ 𝑋) β†’ (βˆƒπ‘₯ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘₯) βŠ† ((intβ€˜π½)β€˜(π΄β€˜π‘›)) β†’ βˆƒπ‘Ÿ ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›)))
199172, 198syldan 589 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑦 ∈ ((intβ€˜π½)β€˜(π΄β€˜π‘›))) β†’ (βˆƒπ‘₯ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘₯) βŠ† ((intβ€˜π½)β€˜(π΄β€˜π‘›)) β†’ βˆƒπ‘Ÿ ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›)))
200168, 199mpd 15 . . . . . . 7 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑦 ∈ ((intβ€˜π½)β€˜(π΄β€˜π‘›))) β†’ βˆƒπ‘Ÿ ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›))
201200ex 411 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑦 ∈ ((intβ€˜π½)β€˜(π΄β€˜π‘›)) β†’ βˆƒπ‘Ÿ ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›)))
202163, 201jcad 511 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝑦 ∈ ((intβ€˜π½)β€˜(π΄β€˜π‘›)) β†’ (𝑦 ∈ 𝑋 ∧ βˆƒπ‘Ÿ ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›))))
203202eximdv 1918 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (βˆƒπ‘¦ 𝑦 ∈ ((intβ€˜π½)β€˜(π΄β€˜π‘›)) β†’ βˆƒπ‘¦(𝑦 ∈ 𝑋 ∧ βˆƒπ‘Ÿ ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›))))
204 n0 4345 . . . 4 (((intβ€˜π½)β€˜(π΄β€˜π‘›)) β‰  βˆ… ↔ βˆƒπ‘¦ 𝑦 ∈ ((intβ€˜π½)β€˜(π΄β€˜π‘›)))
205 df-rex 3069 . . . 4 (βˆƒπ‘¦ ∈ 𝑋 βˆƒπ‘Ÿ ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›) ↔ βˆƒπ‘¦(𝑦 ∈ 𝑋 ∧ βˆƒπ‘Ÿ ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›)))
206203, 204, 2053imtr4g 295 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((intβ€˜π½)β€˜(π΄β€˜π‘›)) β‰  βˆ… β†’ βˆƒπ‘¦ ∈ 𝑋 βˆƒπ‘Ÿ ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›)))
207206reximdva 3166 . 2 (πœ‘ β†’ (βˆƒπ‘› ∈ β„• ((intβ€˜π½)β€˜(π΄β€˜π‘›)) β‰  βˆ… β†’ βˆƒπ‘› ∈ β„• βˆƒπ‘¦ ∈ 𝑋 βˆƒπ‘Ÿ ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›)))
208156, 207mpd 15 1 (πœ‘ β†’ βˆƒπ‘› ∈ β„• βˆƒπ‘¦ ∈ 𝑋 βˆƒπ‘Ÿ ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≀ π‘Ÿ} βŠ† (π΄β€˜π‘›))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539  βˆƒwex 1779   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068  {crab 3430  Vcvv 3472   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  βˆͺ cuni 4907  βˆ© ciin 4997   class class class wbr 5147   ↦ cmpt 5230  β—‘ccnv 5674  ran crn 5676   β€œ cima 5678   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411  β„cr 11111  β„*cxr 11251   < clt 11252   ≀ cle 11253   / cdiv 11875  β„•cn 12216  2c2 12271  β„+crp 12978  βˆžMetcxmet 21129  Metcmet 21130  ballcbl 21131  MetOpencmopn 21134  Topctop 22615  TopOnctopon 22632  Clsdccld 22740  intcnt 22741   Cn ccn 22948  CMetccmet 25002  NrmCVeccnv 30104  BaseSetcba 30106  0veccn0v 30108  normCVcnmcv 30110  IndMetcims 30111   BLnOp cblo 30262  CBanccbn 30382
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-inf2 9638  ax-dc 10443  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191  ax-mulf 11192
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-map 8824  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-sup 9439  df-inf 9440  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-z 12563  df-uz 12827  df-q 12937  df-rp 12979  df-xneg 13096  df-xadd 13097  df-xmul 13098  df-ico 13334  df-seq 13971  df-exp 14032  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-rest 17372  df-topgen 17393  df-psmet 21136  df-xmet 21137  df-met 21138  df-bl 21139  df-mopn 21140  df-fbas 21141  df-fg 21142  df-top 22616  df-topon 22633  df-bases 22669  df-cld 22743  df-ntr 22744  df-cls 22745  df-nei 22822  df-cn 22951  df-cnp 22952  df-lm 22953  df-fil 23570  df-fm 23662  df-flim 23663  df-flf 23664  df-cfil 25003  df-cau 25004  df-cmet 25005  df-grpo 30013  df-gid 30014  df-ginv 30015  df-gdiv 30016  df-ablo 30065  df-vc 30079  df-nv 30112  df-va 30115  df-ba 30116  df-sm 30117  df-0v 30118  df-vs 30119  df-nmcv 30120  df-ims 30121  df-lno 30264  df-nmoo 30265  df-blo 30266  df-0o 30267  df-cbn 30383
This theorem is referenced by:  ubthlem3  30392
  Copyright terms: Public domain W3C validator