bcthlem4

Description: Lemma for bcth . Given any open ball ( C ( ballD ) R ) as starting point (and in particular, a ball in int ( U. ran M ) ), the limit point x of the centers of the induced sequence of balls g is outside U. ran M . Note that a set A has empty interior iff every nonempty open set U contains points outside A , i.e. ( U \ A ) =/= (/) . (Contributed by Mario Carneiro, 7-Jan-2014)

	Ref	Expression
Hypotheses	bcth.2	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	bcthlem.4	⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
	bcthlem.5	⊢ 𝐹 = ( 𝑘 ∈ ℕ , 𝑧 ∈ ( 𝑋 × ℝ⁺ ) ↦ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } )
	bcthlem.6	⊢ ( 𝜑 → 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) )
	bcthlem.7	⊢ ( 𝜑 → 𝑅 ∈ ℝ⁺ )
	bcthlem.8	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
	bcthlem.9	⊢ ( 𝜑 → 𝑔 : ℕ ⟶ ( 𝑋 × ℝ⁺ ) )
	bcthlem.10	⊢ ( 𝜑 → ( 𝑔 ‘ 1 ) = ⟨ 𝐶 , 𝑅 ⟩ )
	bcthlem.11	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) )
Assertion	bcthlem4	⊢ ( 𝜑 → ( ( 𝐶 ( ball ‘ 𝐷 ) 𝑅 ) ∖ ∪ ran 𝑀 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		bcth.2	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		bcthlem.4	⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
3		bcthlem.5	⊢ 𝐹 = ( 𝑘 ∈ ℕ , 𝑧 ∈ ( 𝑋 × ℝ⁺ ) ↦ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } )
4		bcthlem.6	⊢ ( 𝜑 → 𝑀 : ℕ ⟶ ( Clsd ‘ 𝐽 ) )
5		bcthlem.7	⊢ ( 𝜑 → 𝑅 ∈ ℝ⁺ )
6		bcthlem.8	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
7		bcthlem.9	⊢ ( 𝜑 → 𝑔 : ℕ ⟶ ( 𝑋 × ℝ⁺ ) )
8		bcthlem.10	⊢ ( 𝜑 → ( 𝑔 ‘ 1 ) = ⟨ 𝐶 , 𝑅 ⟩ )
9		bcthlem.11	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) )
10		cmetmet	⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
11	2 10	syl	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
12		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
13	11 12	syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
14	1 2 3 4 5 6 7 8 9	bcthlem2	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑛 ) ) )
15		elrp	⊢ ( 𝑟 ∈ ℝ⁺ ↔ ( 𝑟 ∈ ℝ ∧ 0 < 𝑟 ) )
16		nnrecl	⊢ ( ( 𝑟 ∈ ℝ ∧ 0 < 𝑟 ) → ∃ 𝑚 ∈ ℕ ( 1 / 𝑚 ) < 𝑟 )
17	15 16	sylbi	⊢ ( 𝑟 ∈ ℝ⁺ → ∃ 𝑚 ∈ ℕ ( 1 / 𝑚 ) < 𝑟 )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) → ∃ 𝑚 ∈ ℕ ( 1 / 𝑚 ) < 𝑟 )
19		peano2nn	⊢ ( 𝑚 ∈ ℕ → ( 𝑚 + 1 ) ∈ ℕ )
20	19	adantl	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℕ )
21		fvoveq1	⊢ ( 𝑘 = 𝑚 → ( 𝑔 ‘ ( 𝑘 + 1 ) ) = ( 𝑔 ‘ ( 𝑚 + 1 ) ) )
22		id	⊢ ( 𝑘 = 𝑚 → 𝑘 = 𝑚 )
23		fveq2	⊢ ( 𝑘 = 𝑚 → ( 𝑔 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑚 ) )
24	22 23	oveq12d	⊢ ( 𝑘 = 𝑚 → ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) = ( 𝑚 𝐹 ( 𝑔 ‘ 𝑚 ) ) )
25	21 24	eleq12d	⊢ ( 𝑘 = 𝑚 → ( ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ↔ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑔 ‘ 𝑚 ) ) ) )
26	25	rspccva	⊢ ( ( ∀ 𝑘 ∈ ℕ ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑔 ‘ 𝑚 ) ) )
27	9 26	sylan	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑔 ‘ 𝑚 ) ) )
28	7	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑔 ‘ 𝑚 ) ∈ ( 𝑋 × ℝ⁺ ) )
29	1 2 3	bcthlem1	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑔 ‘ 𝑚 ) ∈ ( 𝑋 × ℝ⁺ ) ) ) → ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑔 ‘ 𝑚 ) ) ↔ ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑋 × ℝ⁺ ) ∧ ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < ( 1 / 𝑚 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑚 ) ) ∖ ( 𝑀 ‘ 𝑚 ) ) ) ) )
30	29	expr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑚 ) ∈ ( 𝑋 × ℝ⁺ ) → ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑔 ‘ 𝑚 ) ) ↔ ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑋 × ℝ⁺ ) ∧ ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < ( 1 / 𝑚 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑚 ) ) ∖ ( 𝑀 ‘ 𝑚 ) ) ) ) ) )
31	28 30	mpd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑚 𝐹 ( 𝑔 ‘ 𝑚 ) ) ↔ ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑋 × ℝ⁺ ) ∧ ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < ( 1 / 𝑚 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑚 ) ) ∖ ( 𝑀 ‘ 𝑚 ) ) ) ) )
32	27 31	mpbid	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑋 × ℝ⁺ ) ∧ ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < ( 1 / 𝑚 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑚 ) ) ∖ ( 𝑀 ‘ 𝑚 ) ) ) )
33	32	simp2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < ( 1 / 𝑚 ) )
34	33	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < ( 1 / 𝑚 ) )
35	32	simp1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑋 × ℝ⁺ ) )
36		xp2nd	⊢ ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑋 × ℝ⁺ ) → ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ ℝ⁺ )
37	35 36	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ ℝ⁺ )
38	37	rpred	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ ℝ )
39	38	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ ℝ )
40		nnrecre	⊢ ( 𝑚 ∈ ℕ → ( 1 / 𝑚 ) ∈ ℝ )
41	40	adantl	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑚 ∈ ℕ ) → ( 1 / 𝑚 ) ∈ ℝ )
42		rpre	⊢ ( 𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ )
43	42	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑚 ∈ ℕ ) → 𝑟 ∈ ℝ )
44		lttr	⊢ ( ( ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ ℝ ∧ ( 1 / 𝑚 ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( ( ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < ( 1 / 𝑚 ) ∧ ( 1 / 𝑚 ) < 𝑟 ) → ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < 𝑟 ) )
45	39 41 43 44	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < ( 1 / 𝑚 ) ∧ ( 1 / 𝑚 ) < 𝑟 ) → ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < 𝑟 ) )
46	34 45	mpand	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑚 ∈ ℕ ) → ( ( 1 / 𝑚 ) < 𝑟 → ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < 𝑟 ) )
47		2fveq3	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 2^nd ‘ ( 𝑔 ‘ 𝑛 ) ) = ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) )
48	47	breq1d	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 2^nd ‘ ( 𝑔 ‘ 𝑛 ) ) < 𝑟 ↔ ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < 𝑟 ) )
49	48	rspcev	⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ ∧ ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) < 𝑟 ) → ∃ 𝑛 ∈ ℕ ( 2^nd ‘ ( 𝑔 ‘ 𝑛 ) ) < 𝑟 )
50	20 46 49	syl6an	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑚 ∈ ℕ ) → ( ( 1 / 𝑚 ) < 𝑟 → ∃ 𝑛 ∈ ℕ ( 2^nd ‘ ( 𝑔 ‘ 𝑛 ) ) < 𝑟 ) )
51	50	rexlimdva	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) → ( ∃ 𝑚 ∈ ℕ ( 1 / 𝑚 ) < 𝑟 → ∃ 𝑛 ∈ ℕ ( 2^nd ‘ ( 𝑔 ‘ 𝑛 ) ) < 𝑟 ) )
52	18 51	mpd	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) → ∃ 𝑛 ∈ ℕ ( 2^nd ‘ ( 𝑔 ‘ 𝑛 ) ) < 𝑟 )
53	52	ralrimiva	⊢ ( 𝜑 → ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑛 ∈ ℕ ( 2^nd ‘ ( 𝑔 ‘ 𝑛 ) ) < 𝑟 )
54	13 7 14 53	caubl	⊢ ( 𝜑 → ( 1^st ∘ 𝑔 ) ∈ ( Cau ‘ 𝐷 ) )
55	1	cmetcau	⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 1^st ∘ 𝑔 ) ∈ ( Cau ‘ 𝐷 ) ) → ( 1^st ∘ 𝑔 ) ∈ dom ( ⇝_𝑡 ‘ 𝐽 ) )
56	2 54 55	syl2anc	⊢ ( 𝜑 → ( 1^st ∘ 𝑔 ) ∈ dom ( ⇝_𝑡 ‘ 𝐽 ) )
57		fo1st	⊢ 1^st : V –onto→ V
58		fofun	⊢ ( 1^st : V –onto→ V → Fun 1^st )
59	57 58	ax-mp	⊢ Fun 1^st
60		vex	⊢ 𝑔 ∈ V
61		cofunexg	⊢ ( ( Fun 1^st ∧ 𝑔 ∈ V ) → ( 1^st ∘ 𝑔 ) ∈ V )
62	59 60 61	mp2an	⊢ ( 1^st ∘ 𝑔 ) ∈ V
63	62	eldm	⊢ ( ( 1^st ∘ 𝑔 ) ∈ dom ( ⇝_𝑡 ‘ 𝐽 ) ↔ ∃ 𝑥 ( 1^st ∘ 𝑔 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 )
64	56 63	sylib	⊢ ( 𝜑 → ∃ 𝑥 ( 1^st ∘ 𝑔 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 )
65		1nn	⊢ 1 ∈ ℕ
66	1 2 3 4 5 6 7 8 9	bcthlem3	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝑔 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ∧ 1 ∈ ℕ ) → 𝑥 ∈ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 1 ) ) )
67	65 66	mp3an3	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝑔 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 1 ) ) )
68	8	fveq2d	⊢ ( 𝜑 → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 1 ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ 𝐶 , 𝑅 ⟩ ) )
69		df-ov	⊢ ( 𝐶 ( ball ‘ 𝐷 ) 𝑅 ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ 𝐶 , 𝑅 ⟩ )
70	68 69	eqtr4di	⊢ ( 𝜑 → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 1 ) ) = ( 𝐶 ( ball ‘ 𝐷 ) 𝑅 ) )
71	70	adantr	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝑔 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 1 ) ) = ( 𝐶 ( ball ‘ 𝐷 ) 𝑅 ) )
72	67 71	eleqtrd	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝑔 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ ( 𝐶 ( ball ‘ 𝐷 ) 𝑅 ) )
73	1	mopntop	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
74	13 73	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
75	74	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐽 ∈ Top )
76	13	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
77		xp1st	⊢ ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑋 × ℝ⁺ ) → ( 1^st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ 𝑋 )
78	35 77	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 1^st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ 𝑋 )
79	37	rpxrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ ℝ^* )
80		blssm	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1^st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ 𝑋 ∧ ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ∈ ℝ^* ) → ( ( 1^st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) ⊆ 𝑋 )
81	76 78 79 80	syl3anc	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 1^st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) ⊆ 𝑋 )
82		df-ov	⊢ ( ( 1^st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) , ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⟩ )
83		1st2nd2	⊢ ( ( 𝑔 ‘ ( 𝑚 + 1 ) ) ∈ ( 𝑋 × ℝ⁺ ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) = ⟨ ( 1^st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) , ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⟩ )
84	35 83	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑔 ‘ ( 𝑚 + 1 ) ) = ⟨ ( 1^st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) , ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⟩ )
85	84	fveq2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) , ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⟩ ) )
86	82 85	eqtr4id	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 1^st ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) )
87	1	mopnuni	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
88	13 87	syl	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
89	88	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑋 = ∪ 𝐽 )
90	81 86 89	3sstr3d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⊆ ∪ 𝐽 )
91		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
92	91	sscls	⊢ ( ( 𝐽 ∈ Top ∧ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⊆ ∪ 𝐽 ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) )
93	75 90 92	syl2anc	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) )
94	32	simp3d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑚 ) ) ∖ ( 𝑀 ‘ 𝑚 ) ) )
95	93 94	sstrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑚 ) ) ∖ ( 𝑀 ‘ 𝑚 ) ) )
96	95	3adant2	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝑔 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ∧ 𝑚 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑚 ) ) ∖ ( 𝑀 ‘ 𝑚 ) ) )
97	1 2 3 4 5 6 7 8 9	bcthlem3	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝑔 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ∧ ( 𝑚 + 1 ) ∈ ℕ ) → 𝑥 ∈ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) )
98	19 97	syl3an3	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝑔 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ∧ 𝑚 ∈ ℕ ) → 𝑥 ∈ ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ ( 𝑚 + 1 ) ) ) )
99	96 98	sseldd	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝑔 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ∧ 𝑚 ∈ ℕ ) → 𝑥 ∈ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝑔 ‘ 𝑚 ) ) ∖ ( 𝑀 ‘ 𝑚 ) ) )
100	99	eldifbd	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝑔 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ∧ 𝑚 ∈ ℕ ) → ¬ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) )
101	100	3expa	⊢ ( ( ( 𝜑 ∧ ( 1^st ∘ 𝑔 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ) ∧ 𝑚 ∈ ℕ ) → ¬ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) )
102	101	ralrimiva	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝑔 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ) → ∀ 𝑚 ∈ ℕ ¬ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) )
103		eluni2	⊢ ( 𝑥 ∈ ∪ ran 𝑀 ↔ ∃ 𝑦 ∈ ran 𝑀 𝑥 ∈ 𝑦 )
104	4	ffnd	⊢ ( 𝜑 → 𝑀 Fn ℕ )
105		eleq2	⊢ ( 𝑦 = ( 𝑀 ‘ 𝑚 ) → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) ) )
106	105	rexrn	⊢ ( 𝑀 Fn ℕ → ( ∃ 𝑦 ∈ ran 𝑀 𝑥 ∈ 𝑦 ↔ ∃ 𝑚 ∈ ℕ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) ) )
107	104 106	syl	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ran 𝑀 𝑥 ∈ 𝑦 ↔ ∃ 𝑚 ∈ ℕ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) ) )
108	103 107	bitrid	⊢ ( 𝜑 → ( 𝑥 ∈ ∪ ran 𝑀 ↔ ∃ 𝑚 ∈ ℕ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) ) )
109	108	notbid	⊢ ( 𝜑 → ( ¬ 𝑥 ∈ ∪ ran 𝑀 ↔ ¬ ∃ 𝑚 ∈ ℕ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) ) )
110		ralnex	⊢ ( ∀ 𝑚 ∈ ℕ ¬ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) ↔ ¬ ∃ 𝑚 ∈ ℕ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) )
111	109 110	bitr4di	⊢ ( 𝜑 → ( ¬ 𝑥 ∈ ∪ ran 𝑀 ↔ ∀ 𝑚 ∈ ℕ ¬ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) ) )
112	111	biimpar	⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ ¬ 𝑥 ∈ ( 𝑀 ‘ 𝑚 ) ) → ¬ 𝑥 ∈ ∪ ran 𝑀 )
113	102 112	syldan	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝑔 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ) → ¬ 𝑥 ∈ ∪ ran 𝑀 )
114	72 113	eldifd	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝑔 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ ( ( 𝐶 ( ball ‘ 𝐷 ) 𝑅 ) ∖ ∪ ran 𝑀 ) )
115	114	ne0d	⊢ ( ( 𝜑 ∧ ( 1^st ∘ 𝑔 ) ( ⇝_𝑡 ‘ 𝐽 ) 𝑥 ) → ( ( 𝐶 ( ball ‘ 𝐷 ) 𝑅 ) ∖ ∪ ran 𝑀 ) ≠ ∅ )
116	64 115	exlimddv	⊢ ( 𝜑 → ( ( 𝐶 ( ball ‘ 𝐷 ) 𝑅 ) ∖ ∪ ran 𝑀 ) ≠ ∅ )

Metamath Proof Explorer

Theorem bcthlem4

Proof