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	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) → 𝑃 ∈ ( ( 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	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
7	4	mopntopon	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
8	6 7	syl	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
9		simp3	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) → 𝐴 ∈ ℕ )
10	9	nnzd	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) → 𝐴 ∈ ℤ )
11		simp2	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) → ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 )
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	⊢ ( ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝐴 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝐴 ) ) )
38	6	adantr	⊢ ( ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝐴 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
39		simpl1	⊢ ( ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝐴 ) ) → 𝜑 )
40	39 2	syl	⊢ ( ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝐴 ) ) → 𝐹 : ℕ ⟶ ( 𝑋 × ℝ⁺ ) )
41	23	3ad2antl3	⊢ ( ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝐴 ) ) → 𝑘 ∈ ℕ )
42	40 41	ffvelrnd	⊢ ( ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑋 × ℝ⁺ ) )
43		xp1st	⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑋 × ℝ⁺ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ 𝑋 )
44	42 43	syl	⊢ ( ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝐴 ) ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ 𝑋 )
45		xp2nd	⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑋 × ℝ⁺ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ⁺ )
46	42 45	syl	⊢ ( ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝐴 ) ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ⁺ )
47		blcntr	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ 𝑋 ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ⁺ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
48	38 44 46 47	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝐴 ) ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
49		fvco3	⊢ ( ( 𝐹 : ℕ ⟶ ( 𝑋 × ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) → ( ( 1^st ∘ 𝐹 ) ‘ 𝑘 ) = ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) )
50	40 41 49	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝐴 ) ) → ( ( 1^st ∘ 𝐹 ) ‘ 𝑘 ) = ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) )
51		1st2nd2	⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑋 × ℝ⁺ ) → ( 𝐹 ‘ 𝑘 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ )
52	42 51	syl	⊢ ( ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝑘 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ )
53	52	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝐴 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ ) )
54		df-ov	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ )
55	53 54	eqtr4di	⊢ ( ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝐴 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
56	48 50 55	3eltr4d	⊢ ( ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝐴 ) ) → ( ( 1^st ∘ 𝐹 ) ‘ 𝑘 ) ∈ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) )
57	37 56	sseldd	⊢ ( ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝐴 ) ) → ( ( 1^st ∘ 𝐹 ) ‘ 𝑘 ) ∈ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝐴 ) ) )
58	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝑋 × ℝ⁺ ) )
59	58	3adant2	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝑋 × ℝ⁺ ) )
60		1st2nd2	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝑋 × ℝ⁺ ) → ( 𝐹 ‘ 𝐴 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝐴 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝐴 ) ) ⟩ )
61	59 60	syl	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) → ( 𝐹 ‘ 𝐴 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝐴 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝐴 ) ) ⟩ )
62	61	fveq2d	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝐴 ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝐴 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝐴 ) ) ⟩ ) )
63		df-ov	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝐴 ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝐹 ‘ 𝐴 ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝐴 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝐴 ) ) ⟩ )
64	62 63	eqtr4di	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝐴 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝐴 ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝐹 ‘ 𝐴 ) ) ) )
65		xp1st	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝑋 × ℝ⁺ ) → ( 1^st ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ 𝑋 )
66	59 65	syl	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ 𝑋 )
67		xp2nd	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝑋 × ℝ⁺ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ⁺ )
68	59 67	syl	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ⁺ )
69	68	rpxrd	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ^* )
70		blssm	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1^st ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ 𝑋 ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ^* ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝐴 ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝐹 ‘ 𝐴 ) ) ) ⊆ 𝑋 )
71	6 66 69 70	syl3anc	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝐴 ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝐹 ‘ 𝐴 ) ) ) ⊆ 𝑋 )
72	64 71	eqsstrd	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝐴 ) ) ⊆ 𝑋 )
73	5 8 10 11 57 72	lmcls	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝐹 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑃 ∧ 𝐴 ∈ ℕ ) → 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝐴 ) ) ) )

Metamath Proof Explorer

Theorem caublcls

Proof