Metamath Proof Explorer

Theorem caublcls

Description: The convergent point of a sequence of nested balls is in the closures of any of the balls (i.e. it is in the intersection of the closures). Indeed, it is the only point in the intersection because a metric space is Hausdorff, but we don't prove this here. (Contributed by Mario Carneiro, 21-Jan-2014) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses caubl.2 ⊒ ( πœ‘ β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
caubl.3 ⊒ ( πœ‘ β†’ 𝐹 : β„• ⟢ ( 𝑋 Γ— ℝ+ ) )
caubl.4 ⊒ ( πœ‘ β†’ βˆ€ 𝑛 ∈ β„• ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( 𝑛 + 1 ) ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝑛 ) ) )
caublcls.6 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
Assertion caublcls ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) β†’ 𝑃 ∈ ( ( cls β€˜ 𝐽 ) β€˜ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 caubl.2 ⊒ ( πœ‘ β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
2 caubl.3 ⊒ ( πœ‘ β†’ 𝐹 : β„• ⟢ ( 𝑋 Γ— ℝ+ ) )
3 caubl.4 ⊒ ( πœ‘ β†’ βˆ€ 𝑛 ∈ β„• ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( 𝑛 + 1 ) ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝑛 ) ) )
4 caublcls.6 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
5 eqid ⊒ ( β„€β‰₯ β€˜ 𝐴 ) = ( β„€β‰₯ β€˜ 𝐴 )
6 1 3ad2ant1 ⊒ ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
7 4 mopntopon ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐽 ∈ ( TopOn β€˜ 𝑋 ) )
8 6 7 syl ⊒ ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) β†’ 𝐽 ∈ ( TopOn β€˜ 𝑋 ) )
9 simp3 ⊒ ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) β†’ 𝐴 ∈ β„• )
10 9 nnzd ⊒ ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) β†’ 𝐴 ∈ β„€ )
11 simp2 ⊒ ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) β†’ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 )
12 2fveq3 ⊒ ( π‘Ÿ = 𝐴 β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘Ÿ ) ) = ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) )
13 12 sseq1d ⊒ ( π‘Ÿ = 𝐴 β†’ ( ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘Ÿ ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ↔ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) )
14 13 imbi2d ⊒ ( π‘Ÿ = 𝐴 β†’ ( ( ( πœ‘ ∧ 𝐴 ∈ β„• ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘Ÿ ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) ↔ ( ( πœ‘ ∧ 𝐴 ∈ β„• ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) ) )
15 2fveq3 ⊒ ( π‘Ÿ = π‘˜ β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘Ÿ ) ) = ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) )
16 15 sseq1d ⊒ ( π‘Ÿ = π‘˜ β†’ ( ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘Ÿ ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ↔ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) )
17 16 imbi2d ⊒ ( π‘Ÿ = π‘˜ β†’ ( ( ( πœ‘ ∧ 𝐴 ∈ β„• ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘Ÿ ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) ↔ ( ( πœ‘ ∧ 𝐴 ∈ β„• ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) ) )
18 2fveq3 ⊒ ( π‘Ÿ = ( π‘˜ + 1 ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘Ÿ ) ) = ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( π‘˜ + 1 ) ) ) )
19 18 sseq1d ⊒ ( π‘Ÿ = ( π‘˜ + 1 ) β†’ ( ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘Ÿ ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ↔ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( π‘˜ + 1 ) ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) )
20 19 imbi2d ⊒ ( π‘Ÿ = ( π‘˜ + 1 ) β†’ ( ( ( πœ‘ ∧ 𝐴 ∈ β„• ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘Ÿ ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) ↔ ( ( πœ‘ ∧ 𝐴 ∈ β„• ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( π‘˜ + 1 ) ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) ) )
21 ssid ⊒ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) )
22 21 2a1i ⊒ ( 𝐴 ∈ β„€ β†’ ( ( πœ‘ ∧ 𝐴 ∈ β„• ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) )
23 eluznn ⊒ ( ( 𝐴 ∈ β„• ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ π‘˜ ∈ β„• )
24 fvoveq1 ⊒ ( 𝑛 = π‘˜ β†’ ( 𝐹 β€˜ ( 𝑛 + 1 ) ) = ( 𝐹 β€˜ ( π‘˜ + 1 ) ) )
25 24 fveq2d ⊒ ( 𝑛 = π‘˜ β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( 𝑛 + 1 ) ) ) = ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( π‘˜ + 1 ) ) ) )
26 2fveq3 ⊒ ( 𝑛 = π‘˜ β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝑛 ) ) = ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) )
27 25 26 sseq12d ⊒ ( 𝑛 = π‘˜ β†’ ( ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( 𝑛 + 1 ) ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝑛 ) ) ↔ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( π‘˜ + 1 ) ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) ) )
28 27 rspccva ⊒ ( ( βˆ€ 𝑛 ∈ β„• ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( 𝑛 + 1 ) ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝑛 ) ) ∧ π‘˜ ∈ β„• ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( π‘˜ + 1 ) ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) )
29 3 23 28 syl2an ⊒ ( ( πœ‘ ∧ ( 𝐴 ∈ β„• ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( π‘˜ + 1 ) ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) )
30 29 anassrs ⊒ ( ( ( πœ‘ ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( π‘˜ + 1 ) ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) )
31 sstr2 ⊒ ( ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( π‘˜ + 1 ) ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) β†’ ( ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( π‘˜ + 1 ) ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) )
32 30 31 syl ⊒ ( ( ( πœ‘ ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ ( ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( π‘˜ + 1 ) ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) )
33 32 expcom ⊒ ( π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) β†’ ( ( πœ‘ ∧ 𝐴 ∈ β„• ) β†’ ( ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( π‘˜ + 1 ) ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) ) )
34 33 a2d ⊒ ( π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) β†’ ( ( ( πœ‘ ∧ 𝐴 ∈ β„• ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) β†’ ( ( πœ‘ ∧ 𝐴 ∈ β„• ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ ( π‘˜ + 1 ) ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) ) )
35 14 17 20 17 22 34 uzind4 ⊒ ( π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) β†’ ( ( πœ‘ ∧ 𝐴 ∈ β„• ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) )
36 35 impcom ⊒ ( ( ( πœ‘ ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) )
37 36 3adantl2 ⊒ ( ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) βŠ† ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) )
38 6 adantr ⊒ ( ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
39 simpl1 ⊒ ( ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ πœ‘ )
40 39 2 syl ⊒ ( ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ 𝐹 : β„• ⟢ ( 𝑋 Γ— ℝ+ ) )
41 23 3ad2antl3 ⊒ ( ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ π‘˜ ∈ β„• )
42 40 41 ffvelcdmd ⊒ ( ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ ( 𝐹 β€˜ π‘˜ ) ∈ ( 𝑋 Γ— ℝ+ ) )
43 xp1st ⊒ ( ( 𝐹 β€˜ π‘˜ ) ∈ ( 𝑋 Γ— ℝ+ ) β†’ ( 1st β€˜ ( 𝐹 β€˜ π‘˜ ) ) ∈ 𝑋 )
44 42 43 syl ⊒ ( ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ ( 1st β€˜ ( 𝐹 β€˜ π‘˜ ) ) ∈ 𝑋 )
45 xp2nd ⊒ ( ( 𝐹 β€˜ π‘˜ ) ∈ ( 𝑋 Γ— ℝ+ ) β†’ ( 2nd β€˜ ( 𝐹 β€˜ π‘˜ ) ) ∈ ℝ+ )
46 42 45 syl ⊒ ( ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ ( 2nd β€˜ ( 𝐹 β€˜ π‘˜ ) ) ∈ ℝ+ )
47 blcntr ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 1st β€˜ ( 𝐹 β€˜ π‘˜ ) ) ∈ 𝑋 ∧ ( 2nd β€˜ ( 𝐹 β€˜ π‘˜ ) ) ∈ ℝ+ ) β†’ ( 1st β€˜ ( 𝐹 β€˜ π‘˜ ) ) ∈ ( ( 1st β€˜ ( 𝐹 β€˜ π‘˜ ) ) ( ball β€˜ 𝐷 ) ( 2nd β€˜ ( 𝐹 β€˜ π‘˜ ) ) ) )
48 38 44 46 47 syl3anc ⊒ ( ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ ( 1st β€˜ ( 𝐹 β€˜ π‘˜ ) ) ∈ ( ( 1st β€˜ ( 𝐹 β€˜ π‘˜ ) ) ( ball β€˜ 𝐷 ) ( 2nd β€˜ ( 𝐹 β€˜ π‘˜ ) ) ) )
49 fvco3 ⊒ ( ( 𝐹 : β„• ⟢ ( 𝑋 Γ— ℝ+ ) ∧ π‘˜ ∈ β„• ) β†’ ( ( 1st ∘ 𝐹 ) β€˜ π‘˜ ) = ( 1st β€˜ ( 𝐹 β€˜ π‘˜ ) ) )
50 40 41 49 syl2anc ⊒ ( ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ ( ( 1st ∘ 𝐹 ) β€˜ π‘˜ ) = ( 1st β€˜ ( 𝐹 β€˜ π‘˜ ) ) )
51 1st2nd2 ⊒ ( ( 𝐹 β€˜ π‘˜ ) ∈ ( 𝑋 Γ— ℝ+ ) β†’ ( 𝐹 β€˜ π‘˜ ) = ⟨ ( 1st β€˜ ( 𝐹 β€˜ π‘˜ ) ) , ( 2nd β€˜ ( 𝐹 β€˜ π‘˜ ) ) ⟩ )
52 42 51 syl ⊒ ( ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ ( 𝐹 β€˜ π‘˜ ) = ⟨ ( 1st β€˜ ( 𝐹 β€˜ π‘˜ ) ) , ( 2nd β€˜ ( 𝐹 β€˜ π‘˜ ) ) ⟩ )
53 52 fveq2d ⊒ ( ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( ball β€˜ 𝐷 ) β€˜ ⟨ ( 1st β€˜ ( 𝐹 β€˜ π‘˜ ) ) , ( 2nd β€˜ ( 𝐹 β€˜ π‘˜ ) ) ⟩ ) )
54 df-ov ⊒ ( ( 1st β€˜ ( 𝐹 β€˜ π‘˜ ) ) ( ball β€˜ 𝐷 ) ( 2nd β€˜ ( 𝐹 β€˜ π‘˜ ) ) ) = ( ( ball β€˜ 𝐷 ) β€˜ ⟨ ( 1st β€˜ ( 𝐹 β€˜ π‘˜ ) ) , ( 2nd β€˜ ( 𝐹 β€˜ π‘˜ ) ) ⟩ )
55 53 54 eqtr4di ⊒ ( ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) = ( ( 1st β€˜ ( 𝐹 β€˜ π‘˜ ) ) ( ball β€˜ 𝐷 ) ( 2nd β€˜ ( 𝐹 β€˜ π‘˜ ) ) ) )
56 48 50 55 3eltr4d ⊒ ( ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ ( ( 1st ∘ 𝐹 ) β€˜ π‘˜ ) ∈ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ π‘˜ ) ) )
57 37 56 sseldd ⊒ ( ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) ∧ π‘˜ ∈ ( β„€β‰₯ β€˜ 𝐴 ) ) β†’ ( ( 1st ∘ 𝐹 ) β€˜ π‘˜ ) ∈ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) )
58 2 ffvelcdmda ⊒ ( ( πœ‘ ∧ 𝐴 ∈ β„• ) β†’ ( 𝐹 β€˜ 𝐴 ) ∈ ( 𝑋 Γ— ℝ+ ) )
59 58 3adant2 ⊒ ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) β†’ ( 𝐹 β€˜ 𝐴 ) ∈ ( 𝑋 Γ— ℝ+ ) )
60 1st2nd2 ⊒ ( ( 𝐹 β€˜ 𝐴 ) ∈ ( 𝑋 Γ— ℝ+ ) β†’ ( 𝐹 β€˜ 𝐴 ) = ⟨ ( 1st β€˜ ( 𝐹 β€˜ 𝐴 ) ) , ( 2nd β€˜ ( 𝐹 β€˜ 𝐴 ) ) ⟩ )
61 59 60 syl ⊒ ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) β†’ ( 𝐹 β€˜ 𝐴 ) = ⟨ ( 1st β€˜ ( 𝐹 β€˜ 𝐴 ) ) , ( 2nd β€˜ ( 𝐹 β€˜ 𝐴 ) ) ⟩ )
62 61 fveq2d ⊒ ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) = ( ( ball β€˜ 𝐷 ) β€˜ ⟨ ( 1st β€˜ ( 𝐹 β€˜ 𝐴 ) ) , ( 2nd β€˜ ( 𝐹 β€˜ 𝐴 ) ) ⟩ ) )
63 df-ov ⊒ ( ( 1st β€˜ ( 𝐹 β€˜ 𝐴 ) ) ( ball β€˜ 𝐷 ) ( 2nd β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) = ( ( ball β€˜ 𝐷 ) β€˜ ⟨ ( 1st β€˜ ( 𝐹 β€˜ 𝐴 ) ) , ( 2nd β€˜ ( 𝐹 β€˜ 𝐴 ) ) ⟩ )
64 62 63 eqtr4di ⊒ ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) = ( ( 1st β€˜ ( 𝐹 β€˜ 𝐴 ) ) ( ball β€˜ 𝐷 ) ( 2nd β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) )
65 xp1st ⊒ ( ( 𝐹 β€˜ 𝐴 ) ∈ ( 𝑋 Γ— ℝ+ ) β†’ ( 1st β€˜ ( 𝐹 β€˜ 𝐴 ) ) ∈ 𝑋 )
66 59 65 syl ⊒ ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) β†’ ( 1st β€˜ ( 𝐹 β€˜ 𝐴 ) ) ∈ 𝑋 )
67 xp2nd ⊒ ( ( 𝐹 β€˜ 𝐴 ) ∈ ( 𝑋 Γ— ℝ+ ) β†’ ( 2nd β€˜ ( 𝐹 β€˜ 𝐴 ) ) ∈ ℝ+ )
68 59 67 syl ⊒ ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) β†’ ( 2nd β€˜ ( 𝐹 β€˜ 𝐴 ) ) ∈ ℝ+ )
69 68 rpxrd ⊒ ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) β†’ ( 2nd β€˜ ( 𝐹 β€˜ 𝐴 ) ) ∈ ℝ* )
70 blssm ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 1st β€˜ ( 𝐹 β€˜ 𝐴 ) ) ∈ 𝑋 ∧ ( 2nd β€˜ ( 𝐹 β€˜ 𝐴 ) ) ∈ ℝ* ) β†’ ( ( 1st β€˜ ( 𝐹 β€˜ 𝐴 ) ) ( ball β€˜ 𝐷 ) ( 2nd β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) βŠ† 𝑋 )
71 6 66 69 70 syl3anc ⊒ ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) β†’ ( ( 1st β€˜ ( 𝐹 β€˜ 𝐴 ) ) ( ball β€˜ 𝐷 ) ( 2nd β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) βŠ† 𝑋 )
72 64 71 eqsstrd ⊒ ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) β†’ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) βŠ† 𝑋 )
73 5 8 10 11 57 72 lmcls ⊒ ( ( πœ‘ ∧ ( 1st ∘ 𝐹 ) ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ∧ 𝐴 ∈ β„• ) β†’ 𝑃 ∈ ( ( cls β€˜ 𝐽 ) β€˜ ( ( ball β€˜ 𝐷 ) β€˜ ( 𝐹 β€˜ 𝐴 ) ) ) )