Theorem heiborlem8

Description: Lemma for heibor . The previous lemmas establish that the sequence M is Cauchy, so using completeness we now consider the convergent point Y . By assumption, U is an open cover, so Y is an element of some Z e. U , and some ball centered at Y is contained in Z . But the sequence contains arbitrarily small balls close to Y , so some element ball ( Mn ) of the sequence is contained in Z . And finally we arrive at a contradiction, because { Z } is a finite subcover of U that covers ball ( Mn ) , yet ball ( Mn ) e. K . For convenience, we write this contradiction as ph -> ps where ph is all the accumulated hypotheses and ps is anything at all. (Contributed by Jeff Madsen, 22-Jan-2014)

	Ref	Expression
Hypotheses	heibor.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	heibor.3	⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
	heibor.4	⊢ 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
	heibor.5	⊢ 𝐵 = ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
	heibor.6	⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
	heibor.7	⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) )
	heibor.8	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) )
	heibor.9	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐺 ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
	heibor.10	⊢ ( 𝜑 → 𝐶 𝐺 0 )
	heibor.11	⊢ 𝑆 = seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) )
	heibor.12	⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ )
	heibor.13	⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
	heibor.14	⊢ 𝑌 ∈ V
	heibor.15	⊢ ( 𝜑 → 𝑌 ∈ 𝑍 )
	heibor.16	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
	heibor.17	⊢ ( 𝜑 → ( 1st ∘ 𝑀 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑌 )
Assertion	heiborlem8	⊢ ( 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		heibor.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		heibor.3	⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
3		heibor.4	⊢ 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
4		heibor.5	⊢ 𝐵 = ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
5		heibor.6	⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
6		heibor.7	⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) )
7		heibor.8	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) )
8		heibor.9	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐺 ( ( 𝑇 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑇 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
9		heibor.10	⊢ ( 𝜑 → 𝐶 𝐺 0 )
10		heibor.11	⊢ 𝑆 = seq 0 ( 𝑇 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝐶 , ( 𝑚 − 1 ) ) ) )
11		heibor.12	⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ )
12		heibor.13	⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
13		heibor.14	⊢ 𝑌 ∈ V
14		heibor.15	⊢ ( 𝜑 → 𝑌 ∈ 𝑍 )
15		heibor.16	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
16		heibor.17	⊢ ( 𝜑 → ( 1st ∘ 𝑀 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑌 )
17		cmetmet	⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
18		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
19	5 17 18	3syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
20	12 15	sseldd	⊢ ( 𝜑 → 𝑍 ∈ 𝐽 )
21	1	mopni2	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑍 ∈ 𝐽 ∧ 𝑌 ∈ 𝑍 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑌 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑍 )
22	19 20 14 21	syl3anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ( 𝑌 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑍 )
23		rphalfcl	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 / 2 ) ∈ ℝ+ )
24		breq2	⊢ ( 𝑟 = ( 𝑥 / 2 ) → ( ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < 𝑟 ↔ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) )
25	24	rexbidv	⊢ ( 𝑟 = ( 𝑥 / 2 ) → ( ∃ 𝑘 ∈ ℕ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < 𝑟 ↔ ∃ 𝑘 ∈ ℕ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) )
26	1 2 3 4 5 6 7 8 9 10 11	heiborlem7	⊢ ∀ 𝑟 ∈ ℝ+ ∃ 𝑘 ∈ ℕ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < 𝑟
27	25 26	vtoclri	⊢ ( ( 𝑥 / 2 ) ∈ ℝ+ → ∃ 𝑘 ∈ ℕ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) )
28	23 27	syl	⊢ ( 𝑥 ∈ ℝ+ → ∃ 𝑘 ∈ ℕ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) )
29	28	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑘 ∈ ℕ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) )
30		nnnn0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
31	1 2 3 4 5 6 7 8 9 10	heiborlem4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 )
32		fvex	⊢ ( 𝑆 ‘ 𝑘 ) ∈ V
33		vex	⊢ 𝑘 ∈ V
34	1 2 3 32 33	heiborlem2	⊢ ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 ↔ ( 𝑘 ∈ ℕ0 ∧ ( 𝑆 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ∧ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∈ 𝐾 ) )
35	34	simp3bi	⊢ ( ( 𝑆 ‘ 𝑘 ) 𝐺 𝑘 → ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∈ 𝐾 )
36	31 35	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∈ 𝐾 )
37	30 36	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∈ 𝐾 )
38	37	ad2ant2r	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∈ 𝐾 )
39	19	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
40	1 2 3 4 5 6 7 8 9 10 11	heiborlem5	⊢ ( 𝜑 → 𝑀 : ℕ ⟶ ( 𝑋 × ℝ+ ) )
41	40	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑀 ‘ 𝑘 ) ∈ ( 𝑋 × ℝ+ ) )
42	41	ad2ant2r	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( 𝑀 ‘ 𝑘 ) ∈ ( 𝑋 × ℝ+ ) )
43		xp1st	⊢ ( ( 𝑀 ‘ 𝑘 ) ∈ ( 𝑋 × ℝ+ ) → ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ∈ 𝑋 )
44	42 43	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ∈ 𝑋 )
45		2nn	⊢ 2 ∈ ℕ
46		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ 𝑘 ) ∈ ℕ )
47	45 30 46	sylancr	⊢ ( 𝑘 ∈ ℕ → ( 2 ↑ 𝑘 ) ∈ ℕ )
48	47	nnrpd	⊢ ( 𝑘 ∈ ℕ → ( 2 ↑ 𝑘 ) ∈ ℝ+ )
49	48	rpreccld	⊢ ( 𝑘 ∈ ℕ → ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ+ )
50	49	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ+ )
51	50	rpxrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ* )
52		xp2nd	⊢ ( ( 𝑀 ‘ 𝑘 ) ∈ ( 𝑋 × ℝ+ ) → ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ∈ ℝ+ )
53	42 52	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ∈ ℝ+ )
54	53	rpxrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ∈ ℝ* )
55		1le3	⊢ 1 ≤ 3
56		elrp	⊢ ( ( 2 ↑ 𝑘 ) ∈ ℝ+ ↔ ( ( 2 ↑ 𝑘 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝑘 ) ) )
57		1re	⊢ 1 ∈ ℝ
58		3re	⊢ 3 ∈ ℝ
59		lediv1	⊢ ( ( 1 ∈ ℝ ∧ 3 ∈ ℝ ∧ ( ( 2 ↑ 𝑘 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝑘 ) ) ) → ( 1 ≤ 3 ↔ ( 1 / ( 2 ↑ 𝑘 ) ) ≤ ( 3 / ( 2 ↑ 𝑘 ) ) ) )
60	57 58 59	mp3an12	⊢ ( ( ( 2 ↑ 𝑘 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝑘 ) ) → ( 1 ≤ 3 ↔ ( 1 / ( 2 ↑ 𝑘 ) ) ≤ ( 3 / ( 2 ↑ 𝑘 ) ) ) )
61	56 60	sylbi	⊢ ( ( 2 ↑ 𝑘 ) ∈ ℝ+ → ( 1 ≤ 3 ↔ ( 1 / ( 2 ↑ 𝑘 ) ) ≤ ( 3 / ( 2 ↑ 𝑘 ) ) ) )
62	55 61	mpbii	⊢ ( ( 2 ↑ 𝑘 ) ∈ ℝ+ → ( 1 / ( 2 ↑ 𝑘 ) ) ≤ ( 3 / ( 2 ↑ 𝑘 ) ) )
63	48 62	syl	⊢ ( 𝑘 ∈ ℕ → ( 1 / ( 2 ↑ 𝑘 ) ) ≤ ( 3 / ( 2 ↑ 𝑘 ) ) )
64	63	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( 1 / ( 2 ↑ 𝑘 ) ) ≤ ( 3 / ( 2 ↑ 𝑘 ) ) )
65		fveq2	⊢ ( 𝑛 = 𝑘 → ( 𝑆 ‘ 𝑛 ) = ( 𝑆 ‘ 𝑘 ) )
66		oveq2	⊢ ( 𝑛 = 𝑘 → ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑘 ) )
67	66	oveq2d	⊢ ( 𝑛 = 𝑘 → ( 3 / ( 2 ↑ 𝑛 ) ) = ( 3 / ( 2 ↑ 𝑘 ) ) )
68	65 67	opeq12d	⊢ ( 𝑛 = 𝑘 → ⟨ ( 𝑆 ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ = ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ )
69		opex	⊢ ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ ∈ V
70	68 11 69	fvmpt	⊢ ( 𝑘 ∈ ℕ → ( 𝑀 ‘ 𝑘 ) = ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ )
71	70	fveq2d	⊢ ( 𝑘 ∈ ℕ → ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) = ( 2nd ‘ ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ ) )
72		ovex	⊢ ( 3 / ( 2 ↑ 𝑘 ) ) ∈ V
73	32 72	op2nd	⊢ ( 2nd ‘ ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ ) = ( 3 / ( 2 ↑ 𝑘 ) )
74	71 73	eqtrdi	⊢ ( 𝑘 ∈ ℕ → ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) = ( 3 / ( 2 ↑ 𝑘 ) ) )
75	74	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) = ( 3 / ( 2 ↑ 𝑘 ) ) )
76	64 75	breqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( 1 / ( 2 ↑ 𝑘 ) ) ≤ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) )
77		ssbl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ∈ 𝑋 ) ∧ ( ( 1 / ( 2 ↑ 𝑘 ) ) ∈ ℝ* ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ∈ ℝ* ) ∧ ( 1 / ( 2 ↑ 𝑘 ) ) ≤ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ) → ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ⊆ ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ) )
78	39 44 51 54 76 77	syl221anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ⊆ ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ) )
79	30	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → 𝑘 ∈ ℕ0 )
80		oveq1	⊢ ( 𝑧 = ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) → ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) = ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
81		oveq2	⊢ ( 𝑚 = 𝑘 → ( 2 ↑ 𝑚 ) = ( 2 ↑ 𝑘 ) )
82	81	oveq2d	⊢ ( 𝑚 = 𝑘 → ( 1 / ( 2 ↑ 𝑚 ) ) = ( 1 / ( 2 ↑ 𝑘 ) ) )
83	82	oveq2d	⊢ ( 𝑚 = 𝑘 → ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) = ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) )
84		ovex	⊢ ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) ∈ V
85	80 83 4 84	ovmpo	⊢ ( ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ∈ 𝑋 ∧ 𝑘 ∈ ℕ0 ) → ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) 𝐵 𝑘 ) = ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) )
86	44 79 85	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) 𝐵 𝑘 ) = ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) )
87	70	fveq2d	⊢ ( 𝑘 ∈ ℕ → ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) = ( 1st ‘ ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ ) )
88	32 72	op1st	⊢ ( 1st ‘ ⟨ ( 𝑆 ‘ 𝑘 ) , ( 3 / ( 2 ↑ 𝑘 ) ) ⟩ ) = ( 𝑆 ‘ 𝑘 )
89	87 88	eqtrdi	⊢ ( 𝑘 ∈ ℕ → ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) = ( 𝑆 ‘ 𝑘 ) )
90	89	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) = ( 𝑆 ‘ 𝑘 ) )
91	90	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) 𝐵 𝑘 ) = ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) )
92	86 91	eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑘 ) ) ) = ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) )
93		df-ov	⊢ ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) , ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ⟩ )
94		1st2nd2	⊢ ( ( 𝑀 ‘ 𝑘 ) ∈ ( 𝑋 × ℝ+ ) → ( 𝑀 ‘ 𝑘 ) = ⟨ ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) , ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ⟩ )
95	42 94	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( 𝑀 ‘ 𝑘 ) = ⟨ ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) , ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ⟩ )
96	95	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) , ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ⟩ ) )
97	93 96	eqtr4id	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) )
98	78 92 97	3sstr3d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) )
99	1	mopntop	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
100	39 99	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → 𝐽 ∈ Top )
101		blssm	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ∈ 𝑋 ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ∈ ℝ* ) → ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ) ⊆ 𝑋 )
102	39 44 54 101	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ) ⊆ 𝑋 )
103	1	mopnuni	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
104	39 103	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → 𝑋 = ∪ 𝐽 )
105	102 97 104	3sstr3d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ⊆ ∪ 𝐽 )
106		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
107	106	sscls	⊢ ( ( 𝐽 ∈ Top ∧ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ⊆ ∪ 𝐽 ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ) )
108	100 105 107	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ) )
109	97	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ) ) = ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ) )
110	23	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( 𝑥 / 2 ) ∈ ℝ+ )
111	110	rpxrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( 𝑥 / 2 ) ∈ ℝ* )
112		simprr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) )
113	1	blsscls	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ∈ 𝑋 ) ∧ ( ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ∈ ℝ* ∧ ( 𝑥 / 2 ) ∈ ℝ* ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ) ) ⊆ ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) )
114	39 44 54 111 112 113	syl23anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) ) ) ⊆ ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) )
115	109 114	eqsstrrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ) ⊆ ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) )
116		rpre	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
117	116	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → 𝑥 ∈ ℝ )
118	1 2 3 4 5 6 7 8 9 10 11	heiborlem6	⊢ ( 𝜑 → ∀ 𝑡 ∈ ℕ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ ( 𝑡 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑡 ) ) )
119	19 40 118 1	caublcls	⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑀 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑌 ∧ 𝑘 ∈ ℕ ) → 𝑌 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ) )
120	119	3expia	⊢ ( ( 𝜑 ∧ ( 1st ∘ 𝑀 ) ( ⇝𝑡 ‘ 𝐽 ) 𝑌 ) → ( 𝑘 ∈ ℕ → 𝑌 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ) ) )
121	16 120	mpdan	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ → 𝑌 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ) ) )
122	121	imp	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑌 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ) )
123	122	ad2ant2r	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → 𝑌 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ) )
124	115 123	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → 𝑌 ∈ ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) )
125		blhalf	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ∈ 𝑋 ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑌 ∈ ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ) ) → ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ⊆ ( 𝑌 ( ball ‘ 𝐷 ) 𝑥 ) )
126	39 44 117 124 125	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( 1st ‘ ( 𝑀 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 𝑥 / 2 ) ) ⊆ ( 𝑌 ( ball ‘ 𝐷 ) 𝑥 ) )
127	115 126	sstrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ) ⊆ ( 𝑌 ( ball ‘ 𝐷 ) 𝑥 ) )
128	108 127	sstrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝑀 ‘ 𝑘 ) ) ⊆ ( 𝑌 ( ball ‘ 𝐷 ) 𝑥 ) )
129	98 128	sstrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ( 𝑌 ( ball ‘ 𝐷 ) 𝑥 ) )
130		sstr2	⊢ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ( 𝑌 ( ball ‘ 𝐷 ) 𝑥 ) → ( ( 𝑌 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑍 → ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ 𝑍 ) )
131	129 130	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( 𝑌 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑍 → ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ 𝑍 ) )
132		unisng	⊢ ( 𝑍 ∈ 𝑈 → ∪ { 𝑍 } = 𝑍 )
133	15 132	syl	⊢ ( 𝜑 → ∪ { 𝑍 } = 𝑍 )
134	133	sseq2d	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ∪ { 𝑍 } ↔ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ 𝑍 ) )
135	134	biimpar	⊢ ( ( 𝜑 ∧ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ 𝑍 ) → ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ∪ { 𝑍 } )
136	15	snssd	⊢ ( 𝜑 → { 𝑍 } ⊆ 𝑈 )
137		snex	⊢ { 𝑍 } ∈ V
138	137	elpw	⊢ ( { 𝑍 } ∈ 𝒫 𝑈 ↔ { 𝑍 } ⊆ 𝑈 )
139	136 138	sylibr	⊢ ( 𝜑 → { 𝑍 } ∈ 𝒫 𝑈 )
140		snfi	⊢ { 𝑍 } ∈ Fin
141	140	a1i	⊢ ( 𝜑 → { 𝑍 } ∈ Fin )
142	139 141	elind	⊢ ( 𝜑 → { 𝑍 } ∈ ( 𝒫 𝑈 ∩ Fin ) )
143		unieq	⊢ ( 𝑣 = { 𝑍 } → ∪ 𝑣 = ∪ { 𝑍 } )
144	143	sseq2d	⊢ ( 𝑣 = { 𝑍 } → ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ∪ 𝑣 ↔ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ∪ { 𝑍 } ) )
145	144	rspcev	⊢ ( ( { 𝑍 } ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ∪ { 𝑍 } ) → ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ∪ 𝑣 )
146	142 145	sylan	⊢ ( ( 𝜑 ∧ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ∪ { 𝑍 } ) → ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ∪ 𝑣 )
147	135 146	syldan	⊢ ( ( 𝜑 ∧ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ 𝑍 ) → ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ∪ 𝑣 )
148		ovex	⊢ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∈ V
149		sseq1	⊢ ( 𝑢 = ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) → ( 𝑢 ⊆ ∪ 𝑣 ↔ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ∪ 𝑣 ) )
150	149	rexbidv	⊢ ( 𝑢 = ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 ↔ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ∪ 𝑣 ) )
151	150	notbid	⊢ ( 𝑢 = ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) → ( ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 ↔ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ∪ 𝑣 ) )
152	148 151 2	elab2	⊢ ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∈ 𝐾 ↔ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ∪ 𝑣 )
153	152	con2bii	⊢ ( ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ ∪ 𝑣 ↔ ¬ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∈ 𝐾 )
154	147 153	sylib	⊢ ( ( 𝜑 ∧ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ 𝑍 ) → ¬ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∈ 𝐾 )
155	154	ex	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ 𝑍 → ¬ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∈ 𝐾 ) )
156	155	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ⊆ 𝑍 → ¬ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∈ 𝐾 ) )
157	131 156	syld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ( ( 𝑌 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑍 → ¬ ( ( 𝑆 ‘ 𝑘 ) 𝐵 𝑘 ) ∈ 𝐾 ) )
158	38 157	mt2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℕ ∧ ( 2nd ‘ ( 𝑀 ‘ 𝑘 ) ) < ( 𝑥 / 2 ) ) ) → ¬ ( 𝑌 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑍 )
159	29 158	rexlimddv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ¬ ( 𝑌 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑍 )
160	159	nrexdv	⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ ℝ+ ( 𝑌 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑍 )
161	22 160	pm2.21dd	⊢ ( 𝜑 → 𝜓 )