heibor1lem

Description: Lemma for heibor1 . A compact metric space is complete. This proof works by considering the collection cls ( F " ( ZZ>=n ) ) for each n e. NN , which has the finite intersection property because any finite intersection of upper integer sets is another upper integer set, so any finite intersection of the image closures will contain ( F " ( ZZ>=m ) ) for some m . Thus, by compactness, the intersection contains a point y , which must then be the convergent point of F . (Contributed by Jeff Madsen, 17-Jan-2014) (Revised by Mario Carneiro, 5-Jun-2014)

	Ref	Expression
Hypotheses	heibor.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	heibor1.3	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
	heibor1.4	⊢ ( 𝜑 → 𝐽 ∈ Comp )
	heibor1.5	⊢ ( 𝜑 → 𝐹 ∈ ( Cau ‘ 𝐷 ) )
	heibor1.6	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑋 )
Assertion	heibor1lem	⊢ ( 𝜑 → 𝐹 ∈ dom ( ⇝_𝑡 ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		heibor.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		heibor1.3	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
3		heibor1.4	⊢ ( 𝜑 → 𝐽 ∈ Comp )
4		heibor1.5	⊢ ( 𝜑 → 𝐹 ∈ ( Cau ‘ 𝐷 ) )
5		heibor1.6	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑋 )
6		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
7	2 6	syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
8	1	mopntop	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
9	7 8	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
10		imassrn	⊢ ( 𝐹 “ 𝑢 ) ⊆ ran 𝐹
11	5	frnd	⊢ ( 𝜑 → ran 𝐹 ⊆ 𝑋 )
12	1	mopnuni	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
13	7 12	syl	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
14	11 13	sseqtrd	⊢ ( 𝜑 → ran 𝐹 ⊆ ∪ 𝐽 )
15	10 14	sstrid	⊢ ( 𝜑 → ( 𝐹 “ 𝑢 ) ⊆ ∪ 𝐽 )
16		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
17	16	clscld	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐹 “ 𝑢 ) ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∈ ( Clsd ‘ 𝐽 ) )
18	9 15 17	syl2anc	⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∈ ( Clsd ‘ 𝐽 ) )
19		eleq1a	⊢ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∈ ( Clsd ‘ 𝐽 ) → ( 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → 𝑘 ∈ ( Clsd ‘ 𝐽 ) ) )
20	18 19	syl	⊢ ( 𝜑 → ( 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → 𝑘 ∈ ( Clsd ‘ 𝐽 ) ) )
21	20	rexlimdvw	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → 𝑘 ∈ ( Clsd ‘ 𝐽 ) ) )
22	21	abssdv	⊢ ( 𝜑 → { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ⊆ ( Clsd ‘ 𝐽 ) )
23		fvex	⊢ ( Clsd ‘ 𝐽 ) ∈ V
24	23	elpw2	⊢ ( { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ∈ 𝒫 ( Clsd ‘ 𝐽 ) ↔ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ⊆ ( Clsd ‘ 𝐽 ) )
25	22 24	sylibr	⊢ ( 𝜑 → { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ∈ 𝒫 ( Clsd ‘ 𝐽 ) )
26		elin	⊢ ( 𝑟 ∈ ( 𝒫 { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ∩ Fin ) ↔ ( 𝑟 ∈ 𝒫 { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ∧ 𝑟 ∈ Fin ) )
27		velpw	⊢ ( 𝑟 ∈ 𝒫 { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ↔ 𝑟 ⊆ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } )
28		ssabral	⊢ ( 𝑟 ⊆ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ↔ ∀ 𝑘 ∈ 𝑟 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) )
29	27 28	bitri	⊢ ( 𝑟 ∈ 𝒫 { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ↔ ∀ 𝑘 ∈ 𝑟 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) )
30	29	anbi1i	⊢ ( ( 𝑟 ∈ 𝒫 { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ∧ 𝑟 ∈ Fin ) ↔ ( ∀ 𝑘 ∈ 𝑟 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∧ 𝑟 ∈ Fin ) )
31	26 30	bitri	⊢ ( 𝑟 ∈ ( 𝒫 { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ∩ Fin ) ↔ ( ∀ 𝑘 ∈ 𝑟 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∧ 𝑟 ∈ Fin ) )
32		raleq	⊢ ( 𝑚 = ∅ → ( ∀ 𝑘 ∈ 𝑚 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ↔ ∀ 𝑘 ∈ ∅ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) )
33	32	anbi2d	⊢ ( 𝑚 = ∅ → ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑚 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ↔ ( 𝜑 ∧ ∀ 𝑘 ∈ ∅ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ) )
34		inteq	⊢ ( 𝑚 = ∅ → ∩ 𝑚 = ∩ ∅ )
35	34	sseq2d	⊢ ( 𝑚 = ∅ → ( ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑚 ↔ ( 𝐹 “ 𝑘 ) ⊆ ∩ ∅ ) )
36	35	rexbidv	⊢ ( 𝑚 = ∅ → ( ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑚 ↔ ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ ∅ ) )
37	33 36	imbi12d	⊢ ( 𝑚 = ∅ → ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑚 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑚 ) ↔ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ∅ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ ∅ ) ) )
38		raleq	⊢ ( 𝑚 = 𝑦 → ( ∀ 𝑘 ∈ 𝑚 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ↔ ∀ 𝑘 ∈ 𝑦 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) )
39	38	anbi2d	⊢ ( 𝑚 = 𝑦 → ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑚 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ↔ ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑦 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ) )
40		inteq	⊢ ( 𝑚 = 𝑦 → ∩ 𝑚 = ∩ 𝑦 )
41	40	sseq2d	⊢ ( 𝑚 = 𝑦 → ( ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑚 ↔ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ) )
42	41	rexbidv	⊢ ( 𝑚 = 𝑦 → ( ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑚 ↔ ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ) )
43	39 42	imbi12d	⊢ ( 𝑚 = 𝑦 → ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑚 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑚 ) ↔ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑦 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ) ) )
44		raleq	⊢ ( 𝑚 = ( 𝑦 ∪ { 𝑛 } ) → ( ∀ 𝑘 ∈ 𝑚 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ↔ ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑛 } ) ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) )
45	44	anbi2d	⊢ ( 𝑚 = ( 𝑦 ∪ { 𝑛 } ) → ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑚 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ↔ ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑛 } ) ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ) )
46		inteq	⊢ ( 𝑚 = ( 𝑦 ∪ { 𝑛 } ) → ∩ 𝑚 = ∩ ( 𝑦 ∪ { 𝑛 } ) )
47	46	sseq2d	⊢ ( 𝑚 = ( 𝑦 ∪ { 𝑛 } ) → ( ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑚 ↔ ( 𝐹 “ 𝑘 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) )
48	47	rexbidv	⊢ ( 𝑚 = ( 𝑦 ∪ { 𝑛 } ) → ( ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑚 ↔ ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) )
49	45 48	imbi12d	⊢ ( 𝑚 = ( 𝑦 ∪ { 𝑛 } ) → ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑚 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑚 ) ↔ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑛 } ) ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) ) )
50		raleq	⊢ ( 𝑚 = 𝑟 → ( ∀ 𝑘 ∈ 𝑚 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ↔ ∀ 𝑘 ∈ 𝑟 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) )
51	50	anbi2d	⊢ ( 𝑚 = 𝑟 → ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑚 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ↔ ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑟 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ) )
52		inteq	⊢ ( 𝑚 = 𝑟 → ∩ 𝑚 = ∩ 𝑟 )
53	52	sseq2d	⊢ ( 𝑚 = 𝑟 → ( ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑚 ↔ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑟 ) )
54	53	rexbidv	⊢ ( 𝑚 = 𝑟 → ( ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑚 ↔ ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑟 ) )
55	51 54	imbi12d	⊢ ( 𝑚 = 𝑟 → ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑚 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑚 ) ↔ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑟 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑟 ) ) )
56		uzf	⊢ ℤ_≥ : ℤ ⟶ 𝒫 ℤ
57		ffn	⊢ ( ℤ_≥ : ℤ ⟶ 𝒫 ℤ → ℤ_≥ Fn ℤ )
58	56 57	ax-mp	⊢ ℤ_≥ Fn ℤ
59		0z	⊢ 0 ∈ ℤ
60		fnfvelrn	⊢ ( ( ℤ_≥ Fn ℤ ∧ 0 ∈ ℤ ) → ( ℤ_≥ ‘ 0 ) ∈ ran ℤ_≥ )
61	58 59 60	mp2an	⊢ ( ℤ_≥ ‘ 0 ) ∈ ran ℤ_≥
62		ssv	⊢ ( 𝐹 “ ( ℤ_≥ ‘ 0 ) ) ⊆ V
63		int0	⊢ ∩ ∅ = V
64	62 63	sseqtrri	⊢ ( 𝐹 “ ( ℤ_≥ ‘ 0 ) ) ⊆ ∩ ∅
65		imaeq2	⊢ ( 𝑘 = ( ℤ_≥ ‘ 0 ) → ( 𝐹 “ 𝑘 ) = ( 𝐹 “ ( ℤ_≥ ‘ 0 ) ) )
66	65	sseq1d	⊢ ( 𝑘 = ( ℤ_≥ ‘ 0 ) → ( ( 𝐹 “ 𝑘 ) ⊆ ∩ ∅ ↔ ( 𝐹 “ ( ℤ_≥ ‘ 0 ) ) ⊆ ∩ ∅ ) )
67	66	rspcev	⊢ ( ( ( ℤ_≥ ‘ 0 ) ∈ ran ℤ_≥ ∧ ( 𝐹 “ ( ℤ_≥ ‘ 0 ) ) ⊆ ∩ ∅ ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ ∅ )
68	61 64 67	mp2an	⊢ ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ ∅
69	68	a1i	⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ∅ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ ∅ )
70		ssun1	⊢ 𝑦 ⊆ ( 𝑦 ∪ { 𝑛 } )
71		ssralv	⊢ ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑛 } ) → ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑛 } ) ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → ∀ 𝑘 ∈ 𝑦 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) )
72	70 71	ax-mp	⊢ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑛 } ) ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → ∀ 𝑘 ∈ 𝑦 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) )
73	72	anim2i	⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑛 } ) ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑦 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) )
74	73	imim1i	⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑦 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ) → ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑛 } ) ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ) )
75		ssun2	⊢ { 𝑛 } ⊆ ( 𝑦 ∪ { 𝑛 } )
76		ssralv	⊢ ( { 𝑛 } ⊆ ( 𝑦 ∪ { 𝑛 } ) → ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑛 } ) ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → ∀ 𝑘 ∈ { 𝑛 } ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) )
77	75 76	ax-mp	⊢ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑛 } ) ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → ∀ 𝑘 ∈ { 𝑛 } ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) )
78		vex	⊢ 𝑛 ∈ V
79		eqeq1	⊢ ( 𝑘 = 𝑛 → ( 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ↔ 𝑛 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) )
80	79	rexbidv	⊢ ( 𝑘 = 𝑛 → ( ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ↔ ∃ 𝑢 ∈ ran ℤ_≥ 𝑛 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) )
81	78 80	ralsn	⊢ ( ∀ 𝑘 ∈ { 𝑛 } ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ↔ ∃ 𝑢 ∈ ran ℤ_≥ 𝑛 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) )
82	77 81	sylib	⊢ ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑛 } ) ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → ∃ 𝑢 ∈ ran ℤ_≥ 𝑛 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) )
83		uzin2	⊢ ( ( 𝑢 ∈ ran ℤ_≥ ∧ 𝑘 ∈ ran ℤ_≥ ) → ( 𝑢 ∩ 𝑘 ) ∈ ran ℤ_≥ )
84	10 11	sstrid	⊢ ( 𝜑 → ( 𝐹 “ 𝑢 ) ⊆ 𝑋 )
85	84 13	sseqtrd	⊢ ( 𝜑 → ( 𝐹 “ 𝑢 ) ⊆ ∪ 𝐽 )
86	16	sscls	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐹 “ 𝑢 ) ⊆ ∪ 𝐽 ) → ( 𝐹 “ 𝑢 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) )
87	9 85 86	syl2anc	⊢ ( 𝜑 → ( 𝐹 “ 𝑢 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) )
88		sseq2	⊢ ( 𝑛 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → ( ( 𝐹 “ 𝑢 ) ⊆ 𝑛 ↔ ( 𝐹 “ 𝑢 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) )
89	87 88	syl5ibrcom	⊢ ( 𝜑 → ( 𝑛 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → ( 𝐹 “ 𝑢 ) ⊆ 𝑛 ) )
90		inss2	⊢ ( 𝑢 ∩ 𝑘 ) ⊆ 𝑘
91		inss1	⊢ ( 𝑢 ∩ 𝑘 ) ⊆ 𝑢
92		imass2	⊢ ( ( 𝑢 ∩ 𝑘 ) ⊆ 𝑘 → ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑘 ) )
93		imass2	⊢ ( ( 𝑢 ∩ 𝑘 ) ⊆ 𝑢 → ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑢 ) )
94	92 93	anim12i	⊢ ( ( ( 𝑢 ∩ 𝑘 ) ⊆ 𝑘 ∧ ( 𝑢 ∩ 𝑘 ) ⊆ 𝑢 ) → ( ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑘 ) ∧ ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑢 ) ) )
95		ssin	⊢ ( ( ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑘 ) ∧ ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑢 ) ) ↔ ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ( ( 𝐹 “ 𝑘 ) ∩ ( 𝐹 “ 𝑢 ) ) )
96	94 95	sylib	⊢ ( ( ( 𝑢 ∩ 𝑘 ) ⊆ 𝑘 ∧ ( 𝑢 ∩ 𝑘 ) ⊆ 𝑢 ) → ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ( ( 𝐹 “ 𝑘 ) ∩ ( 𝐹 “ 𝑢 ) ) )
97	90 91 96	mp2an	⊢ ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ( ( 𝐹 “ 𝑘 ) ∩ ( 𝐹 “ 𝑢 ) )
98		ss2in	⊢ ( ( ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ∧ ( 𝐹 “ 𝑢 ) ⊆ 𝑛 ) → ( ( 𝐹 “ 𝑘 ) ∩ ( 𝐹 “ 𝑢 ) ) ⊆ ( ∩ 𝑦 ∩ 𝑛 ) )
99	97 98	sstrid	⊢ ( ( ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ∧ ( 𝐹 “ 𝑢 ) ⊆ 𝑛 ) → ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ( ∩ 𝑦 ∩ 𝑛 ) )
100	78	intunsn	⊢ ∩ ( 𝑦 ∪ { 𝑛 } ) = ( ∩ 𝑦 ∩ 𝑛 )
101	99 100	sseqtrrdi	⊢ ( ( ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ∧ ( 𝐹 “ 𝑢 ) ⊆ 𝑛 ) → ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) )
102	101	expcom	⊢ ( ( 𝐹 “ 𝑢 ) ⊆ 𝑛 → ( ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 → ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) )
103	89 102	syl6	⊢ ( 𝜑 → ( 𝑛 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → ( ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 → ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) ) )
104	103	impd	⊢ ( 𝜑 → ( ( 𝑛 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∧ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ) → ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) )
105		imaeq2	⊢ ( 𝑚 = ( 𝑢 ∩ 𝑘 ) → ( 𝐹 “ 𝑚 ) = ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) )
106	105	sseq1d	⊢ ( 𝑚 = ( 𝑢 ∩ 𝑘 ) → ( ( 𝐹 “ 𝑚 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ↔ ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) )
107	106	rspcev	⊢ ( ( ( 𝑢 ∩ 𝑘 ) ∈ ran ℤ_≥ ∧ ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) → ∃ 𝑚 ∈ ran ℤ_≥ ( 𝐹 “ 𝑚 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) )
108	107	expcom	⊢ ( ( 𝐹 “ ( 𝑢 ∩ 𝑘 ) ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) → ( ( 𝑢 ∩ 𝑘 ) ∈ ran ℤ_≥ → ∃ 𝑚 ∈ ran ℤ_≥ ( 𝐹 “ 𝑚 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) )
109	104 108	syl6	⊢ ( 𝜑 → ( ( 𝑛 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∧ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ) → ( ( 𝑢 ∩ 𝑘 ) ∈ ran ℤ_≥ → ∃ 𝑚 ∈ ran ℤ_≥ ( 𝐹 “ 𝑚 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) ) )
110	109	com23	⊢ ( 𝜑 → ( ( 𝑢 ∩ 𝑘 ) ∈ ran ℤ_≥ → ( ( 𝑛 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∧ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ) → ∃ 𝑚 ∈ ran ℤ_≥ ( 𝐹 “ 𝑚 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) ) )
111	83 110	syl5	⊢ ( 𝜑 → ( ( 𝑢 ∈ ran ℤ_≥ ∧ 𝑘 ∈ ran ℤ_≥ ) → ( ( 𝑛 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∧ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ) → ∃ 𝑚 ∈ ran ℤ_≥ ( 𝐹 “ 𝑚 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) ) )
112	111	rexlimdvv	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ran ℤ_≥ ∃ 𝑘 ∈ ran ℤ_≥ ( 𝑛 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∧ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ) → ∃ 𝑚 ∈ ran ℤ_≥ ( 𝐹 “ 𝑚 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) )
113		reeanv	⊢ ( ∃ 𝑢 ∈ ran ℤ_≥ ∃ 𝑘 ∈ ran ℤ_≥ ( 𝑛 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∧ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ) ↔ ( ∃ 𝑢 ∈ ran ℤ_≥ 𝑛 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∧ ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ) )
114		imaeq2	⊢ ( 𝑚 = 𝑘 → ( 𝐹 “ 𝑚 ) = ( 𝐹 “ 𝑘 ) )
115	114	sseq1d	⊢ ( 𝑚 = 𝑘 → ( ( 𝐹 “ 𝑚 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ↔ ( 𝐹 “ 𝑘 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) )
116	115	cbvrexvw	⊢ ( ∃ 𝑚 ∈ ran ℤ_≥ ( 𝐹 “ 𝑚 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ↔ ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) )
117	112 113 116	3imtr3g	⊢ ( 𝜑 → ( ( ∃ 𝑢 ∈ ran ℤ_≥ 𝑛 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∧ ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) )
118	117	expd	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ran ℤ_≥ 𝑛 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → ( ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) ) )
119	82 118	syl5	⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑛 } ) ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → ( ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) ) )
120	119	imp	⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑛 } ) ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ( ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) )
121	74 120	sylcom	⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑦 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ) → ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑛 } ) ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) )
122	121	a1i	⊢ ( 𝑦 ∈ Fin → ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑦 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑦 ) → ( ( 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑦 ∪ { 𝑛 } ) ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ ( 𝑦 ∪ { 𝑛 } ) ) ) )
123	37 43 49 55 69 122	findcard2	⊢ ( 𝑟 ∈ Fin → ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑟 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑟 ) )
124	123	com12	⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝑟 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ( 𝑟 ∈ Fin → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑟 ) )
125	124	impr	⊢ ( ( 𝜑 ∧ ( ∀ 𝑘 ∈ 𝑟 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∧ 𝑟 ∈ Fin ) ) → ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑟 )
126	5	ffnd	⊢ ( 𝜑 → 𝐹 Fn ℕ )
127		inss1	⊢ ( 𝑘 ∩ ℕ ) ⊆ 𝑘
128		imass2	⊢ ( ( 𝑘 ∩ ℕ ) ⊆ 𝑘 → ( 𝐹 “ ( 𝑘 ∩ ℕ ) ) ⊆ ( 𝐹 “ 𝑘 ) )
129	127 128	ax-mp	⊢ ( 𝐹 “ ( 𝑘 ∩ ℕ ) ) ⊆ ( 𝐹 “ 𝑘 )
130		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
131		1z	⊢ 1 ∈ ℤ
132		fnfvelrn	⊢ ( ( ℤ_≥ Fn ℤ ∧ 1 ∈ ℤ ) → ( ℤ_≥ ‘ 1 ) ∈ ran ℤ_≥ )
133	58 131 132	mp2an	⊢ ( ℤ_≥ ‘ 1 ) ∈ ran ℤ_≥
134	130 133	eqeltri	⊢ ℕ ∈ ran ℤ_≥
135		uzin2	⊢ ( ( 𝑘 ∈ ran ℤ_≥ ∧ ℕ ∈ ran ℤ_≥ ) → ( 𝑘 ∩ ℕ ) ∈ ran ℤ_≥ )
136	134 135	mpan2	⊢ ( 𝑘 ∈ ran ℤ_≥ → ( 𝑘 ∩ ℕ ) ∈ ran ℤ_≥ )
137		uzn0	⊢ ( ( 𝑘 ∩ ℕ ) ∈ ran ℤ_≥ → ( 𝑘 ∩ ℕ ) ≠ ∅ )
138	136 137	syl	⊢ ( 𝑘 ∈ ran ℤ_≥ → ( 𝑘 ∩ ℕ ) ≠ ∅ )
139		n0	⊢ ( ( 𝑘 ∩ ℕ ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( 𝑘 ∩ ℕ ) )
140	138 139	sylib	⊢ ( 𝑘 ∈ ran ℤ_≥ → ∃ 𝑦 𝑦 ∈ ( 𝑘 ∩ ℕ ) )
141		fnfun	⊢ ( 𝐹 Fn ℕ → Fun 𝐹 )
142		inss2	⊢ ( 𝑘 ∩ ℕ ) ⊆ ℕ
143		fndm	⊢ ( 𝐹 Fn ℕ → dom 𝐹 = ℕ )
144	142 143	sseqtrrid	⊢ ( 𝐹 Fn ℕ → ( 𝑘 ∩ ℕ ) ⊆ dom 𝐹 )
145		funfvima2	⊢ ( ( Fun 𝐹 ∧ ( 𝑘 ∩ ℕ ) ⊆ dom 𝐹 ) → ( 𝑦 ∈ ( 𝑘 ∩ ℕ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑘 ∩ ℕ ) ) ) )
146	141 144 145	syl2anc	⊢ ( 𝐹 Fn ℕ → ( 𝑦 ∈ ( 𝑘 ∩ ℕ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑘 ∩ ℕ ) ) ) )
147		ne0i	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 “ ( 𝑘 ∩ ℕ ) ) → ( 𝐹 “ ( 𝑘 ∩ ℕ ) ) ≠ ∅ )
148	146 147	syl6	⊢ ( 𝐹 Fn ℕ → ( 𝑦 ∈ ( 𝑘 ∩ ℕ ) → ( 𝐹 “ ( 𝑘 ∩ ℕ ) ) ≠ ∅ ) )
149	148	exlimdv	⊢ ( 𝐹 Fn ℕ → ( ∃ 𝑦 𝑦 ∈ ( 𝑘 ∩ ℕ ) → ( 𝐹 “ ( 𝑘 ∩ ℕ ) ) ≠ ∅ ) )
150	140 149	syl5	⊢ ( 𝐹 Fn ℕ → ( 𝑘 ∈ ran ℤ_≥ → ( 𝐹 “ ( 𝑘 ∩ ℕ ) ) ≠ ∅ ) )
151	150	imp	⊢ ( ( 𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ_≥ ) → ( 𝐹 “ ( 𝑘 ∩ ℕ ) ) ≠ ∅ )
152		ssn0	⊢ ( ( ( 𝐹 “ ( 𝑘 ∩ ℕ ) ) ⊆ ( 𝐹 “ 𝑘 ) ∧ ( 𝐹 “ ( 𝑘 ∩ ℕ ) ) ≠ ∅ ) → ( 𝐹 “ 𝑘 ) ≠ ∅ )
153	129 151 152	sylancr	⊢ ( ( 𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ_≥ ) → ( 𝐹 “ 𝑘 ) ≠ ∅ )
154		ssn0	⊢ ( ( ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑟 ∧ ( 𝐹 “ 𝑘 ) ≠ ∅ ) → ∩ 𝑟 ≠ ∅ )
155	154	expcom	⊢ ( ( 𝐹 “ 𝑘 ) ≠ ∅ → ( ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅ ) )
156	153 155	syl	⊢ ( ( 𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ_≥ ) → ( ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅ ) )
157	156	rexlimdva	⊢ ( 𝐹 Fn ℕ → ( ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅ ) )
158	126 157	syl	⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅ ) )
159	158	adantr	⊢ ( ( 𝜑 ∧ ( ∀ 𝑘 ∈ 𝑟 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∧ 𝑟 ∈ Fin ) ) → ( ∃ 𝑘 ∈ ran ℤ_≥ ( 𝐹 “ 𝑘 ) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅ ) )
160	125 159	mpd	⊢ ( ( 𝜑 ∧ ( ∀ 𝑘 ∈ 𝑟 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∧ 𝑟 ∈ Fin ) ) → ∩ 𝑟 ≠ ∅ )
161	160	necomd	⊢ ( ( 𝜑 ∧ ( ∀ 𝑘 ∈ 𝑟 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∧ 𝑟 ∈ Fin ) ) → ∅ ≠ ∩ 𝑟 )
162	161	neneqd	⊢ ( ( 𝜑 ∧ ( ∀ 𝑘 ∈ 𝑟 ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∧ 𝑟 ∈ Fin ) ) → ¬ ∅ = ∩ 𝑟 )
163	31 162	sylan2b	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝒫 { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ∩ Fin ) ) → ¬ ∅ = ∩ 𝑟 )
164	163	nrexdv	⊢ ( 𝜑 → ¬ ∃ 𝑟 ∈ ( 𝒫 { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ∩ Fin ) ∅ = ∩ 𝑟 )
165		0ex	⊢ ∅ ∈ V
166		zex	⊢ ℤ ∈ V
167	166	pwex	⊢ 𝒫 ℤ ∈ V
168		frn	⊢ ( ℤ_≥ : ℤ ⟶ 𝒫 ℤ → ran ℤ_≥ ⊆ 𝒫 ℤ )
169	56 168	ax-mp	⊢ ran ℤ_≥ ⊆ 𝒫 ℤ
170	167 169	ssexi	⊢ ran ℤ_≥ ∈ V
171	170	abrexex	⊢ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ∈ V
172		elfi	⊢ ( ( ∅ ∈ V ∧ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ∈ V ) → ( ∅ ∈ ( fi ‘ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ) ↔ ∃ 𝑟 ∈ ( 𝒫 { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ∩ Fin ) ∅ = ∩ 𝑟 ) )
173	165 171 172	mp2an	⊢ ( ∅ ∈ ( fi ‘ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ) ↔ ∃ 𝑟 ∈ ( 𝒫 { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ∩ Fin ) ∅ = ∩ 𝑟 )
174	164 173	sylnibr	⊢ ( 𝜑 → ¬ ∅ ∈ ( fi ‘ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ) )
175		cmptop	⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
176		cmpfi	⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Comp ↔ ∀ 𝑚 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ( ¬ ∅ ∈ ( fi ‘ 𝑚 ) → ∩ 𝑚 ≠ ∅ ) ) )
177	175 176	syl	⊢ ( 𝐽 ∈ Comp → ( 𝐽 ∈ Comp ↔ ∀ 𝑚 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ( ¬ ∅ ∈ ( fi ‘ 𝑚 ) → ∩ 𝑚 ≠ ∅ ) ) )
178	177	ibi	⊢ ( 𝐽 ∈ Comp → ∀ 𝑚 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ( ¬ ∅ ∈ ( fi ‘ 𝑚 ) → ∩ 𝑚 ≠ ∅ ) )
179		fveq2	⊢ ( 𝑚 = { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } → ( fi ‘ 𝑚 ) = ( fi ‘ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ) )
180	179	eleq2d	⊢ ( 𝑚 = { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } → ( ∅ ∈ ( fi ‘ 𝑚 ) ↔ ∅ ∈ ( fi ‘ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ) ) )
181	180	notbid	⊢ ( 𝑚 = { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } → ( ¬ ∅ ∈ ( fi ‘ 𝑚 ) ↔ ¬ ∅ ∈ ( fi ‘ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ) ) )
182		inteq	⊢ ( 𝑚 = { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } → ∩ 𝑚 = ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } )
183	182	neeq1d	⊢ ( 𝑚 = { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } → ( ∩ 𝑚 ≠ ∅ ↔ ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ≠ ∅ ) )
184		n0	⊢ ( ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } )
185	183 184	bitrdi	⊢ ( 𝑚 = { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } → ( ∩ 𝑚 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ) )
186	181 185	imbi12d	⊢ ( 𝑚 = { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } → ( ( ¬ ∅ ∈ ( fi ‘ 𝑚 ) → ∩ 𝑚 ≠ ∅ ) ↔ ( ¬ ∅ ∈ ( fi ‘ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ) → ∃ 𝑦 𝑦 ∈ ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ) ) )
187	186	rspccv	⊢ ( ∀ 𝑚 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ( ¬ ∅ ∈ ( fi ‘ 𝑚 ) → ∩ 𝑚 ≠ ∅ ) → ( { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ∈ 𝒫 ( Clsd ‘ 𝐽 ) → ( ¬ ∅ ∈ ( fi ‘ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ) → ∃ 𝑦 𝑦 ∈ ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ) ) )
188	178 187	syl	⊢ ( 𝐽 ∈ Comp → ( { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ∈ 𝒫 ( Clsd ‘ 𝐽 ) → ( ¬ ∅ ∈ ( fi ‘ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ) → ∃ 𝑦 𝑦 ∈ ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ) ) )
189	3 25 174 188	syl3c	⊢ ( 𝜑 → ∃ 𝑦 𝑦 ∈ ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } )
190		lmrel	⊢ Rel ( ⇝_𝑡 ‘ 𝐽 )
191		r19.23v	⊢ ( ∀ 𝑢 ∈ ran ℤ_≥ ( 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → 𝑦 ∈ 𝑘 ) ↔ ( ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → 𝑦 ∈ 𝑘 ) )
192	191	albii	⊢ ( ∀ 𝑘 ∀ 𝑢 ∈ ran ℤ_≥ ( 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → 𝑦 ∈ 𝑘 ) ↔ ∀ 𝑘 ( ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → 𝑦 ∈ 𝑘 ) )
193		fvex	⊢ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ∈ V
194		eleq2	⊢ ( 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → ( 𝑦 ∈ 𝑘 ↔ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) )
195	193 194	ceqsalv	⊢ ( ∀ 𝑘 ( 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → 𝑦 ∈ 𝑘 ) ↔ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) )
196	195	ralbii	⊢ ( ∀ 𝑢 ∈ ran ℤ_≥ ∀ 𝑘 ( 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → 𝑦 ∈ 𝑘 ) ↔ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) )
197		ralcom4	⊢ ( ∀ 𝑢 ∈ ran ℤ_≥ ∀ 𝑘 ( 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → 𝑦 ∈ 𝑘 ) ↔ ∀ 𝑘 ∀ 𝑢 ∈ ran ℤ_≥ ( 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → 𝑦 ∈ 𝑘 ) )
198	196 197	bitr3i	⊢ ( ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ↔ ∀ 𝑘 ∀ 𝑢 ∈ ran ℤ_≥ ( 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → 𝑦 ∈ 𝑘 ) )
199		vex	⊢ 𝑦 ∈ V
200	199	elintab	⊢ ( 𝑦 ∈ ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ↔ ∀ 𝑘 ( ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → 𝑦 ∈ 𝑘 ) )
201	192 198 200	3bitr4i	⊢ ( ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ↔ 𝑦 ∈ ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } )
202		eqid	⊢ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) )
203		imaeq2	⊢ ( 𝑢 = ℕ → ( 𝐹 “ 𝑢 ) = ( 𝐹 “ ℕ ) )
204	203	fveq2d	⊢ ( 𝑢 = ℕ → ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) )
205	204	rspceeqv	⊢ ( ( ℕ ∈ ran ℤ_≥ ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) ) → ∃ 𝑢 ∈ ran ℤ_≥ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) )
206	134 202 205	mp2an	⊢ ∃ 𝑢 ∈ ran ℤ_≥ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) )
207		fvex	⊢ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) ∈ V
208		eqeq1	⊢ ( 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) → ( 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ↔ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) )
209	208	rexbidv	⊢ ( 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) → ( ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ↔ ∃ 𝑢 ∈ ran ℤ_≥ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) )
210	207 209	elab	⊢ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) ∈ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ↔ ∃ 𝑢 ∈ ran ℤ_≥ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) )
211	206 210	mpbir	⊢ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) ∈ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) }
212		intss1	⊢ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) ∈ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } → ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) )
213	211 212	ax-mp	⊢ ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) )
214		imassrn	⊢ ( 𝐹 “ ℕ ) ⊆ ran 𝐹
215	214 14	sstrid	⊢ ( 𝜑 → ( 𝐹 “ ℕ ) ⊆ ∪ 𝐽 )
216	16	clsss3	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐹 “ ℕ ) ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) ⊆ ∪ 𝐽 )
217	9 215 216	syl2anc	⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) ⊆ ∪ 𝐽 )
218	217 13	sseqtrrd	⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ℕ ) ) ⊆ 𝑋 )
219	213 218	sstrid	⊢ ( 𝜑 → ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ⊆ 𝑋 )
220	219	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ) → 𝑦 ∈ 𝑋 )
221	201 220	sylan2b	⊢ ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → 𝑦 ∈ 𝑋 )
222		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
223	130 7 222	iscau3	⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑_pm ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑚 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 ) ) ) )
224	4 223	mpbid	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 ↑_pm ℂ ) ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑚 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 ) ) )
225	224	simprd	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑚 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 ) )
226		simp3	⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 ) → ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 )
227	226	ralimi	⊢ ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 ) → ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 )
228	227	reximi	⊢ ( ∃ 𝑚 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 ) → ∃ 𝑚 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 )
229	228	ralimi	⊢ ( ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑚 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 ) → ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑚 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 )
230	225 229	syl	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑚 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 )
231	230	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑚 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 )
232		rphalfcl	⊢ ( 𝑟 ∈ ℝ⁺ → ( 𝑟 / 2 ) ∈ ℝ⁺ )
233		breq2	⊢ ( 𝑦 = ( 𝑟 / 2 ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) ) )
234	233	2ralbidv	⊢ ( 𝑦 = ( 𝑟 / 2 ) → ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 ↔ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) ) )
235	234	rexbidv	⊢ ( 𝑦 = ( 𝑟 / 2 ) → ( ∃ 𝑚 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 ↔ ∃ 𝑚 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) ) )
236	235	rspccva	⊢ ( ( ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑚 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑦 ∧ ( 𝑟 / 2 ) ∈ ℝ⁺ ) → ∃ 𝑚 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) )
237	231 232 236	syl2an	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ 𝑟 ∈ ℝ⁺ ) → ∃ 𝑚 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) )
238	5	ffund	⊢ ( 𝜑 → Fun 𝐹 )
239	238	ad2antrr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → Fun 𝐹 )
240	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → 𝐽 ∈ Top )
241		imassrn	⊢ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ⊆ ran 𝐹
242	241 14	sstrid	⊢ ( 𝜑 → ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ⊆ ∪ 𝐽 )
243	242	ad2antrr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ⊆ ∪ 𝐽 )
244		nnz	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℤ )
245		fnfvelrn	⊢ ( ( ℤ_≥ Fn ℤ ∧ 𝑚 ∈ ℤ ) → ( ℤ_≥ ‘ 𝑚 ) ∈ ran ℤ_≥ )
246	58 244 245	sylancr	⊢ ( 𝑚 ∈ ℕ → ( ℤ_≥ ‘ 𝑚 ) ∈ ran ℤ_≥ )
247	246	ad2antll	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → ( ℤ_≥ ‘ 𝑚 ) ∈ ran ℤ_≥ )
248		simplr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) )
249		imaeq2	⊢ ( 𝑢 = ( ℤ_≥ ‘ 𝑚 ) → ( 𝐹 “ 𝑢 ) = ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) )
250	249	fveq2d	⊢ ( 𝑢 = ( ℤ_≥ ‘ 𝑚 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) )
251	250	eleq2d	⊢ ( 𝑢 = ( ℤ_≥ ‘ 𝑚 ) → ( 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ↔ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) ) )
252	251	rspcv	⊢ ( ( ℤ_≥ ‘ 𝑚 ) ∈ ran ℤ_≥ → ( ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) → 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) ) )
253	247 248 252	sylc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) )
254	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
255	221	adantr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → 𝑦 ∈ 𝑋 )
256	232	ad2antrl	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → ( 𝑟 / 2 ) ∈ ℝ⁺ )
257	256	rpxrd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → ( 𝑟 / 2 ) ∈ ℝ^* )
258	1	blopn	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ ( 𝑟 / 2 ) ∈ ℝ^* ) → ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∈ 𝐽 )
259	254 255 257 258	syl3anc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∈ 𝐽 )
260		blcntr	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ ( 𝑟 / 2 ) ∈ ℝ⁺ ) → 𝑦 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
261	254 255 256 260	syl3anc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → 𝑦 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
262	16	clsndisj	⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ⊆ ∪ 𝐽 ∧ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) ) ∧ ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ) → ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) ≠ ∅ )
263	240 243 253 259 261 262	syl32anc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) ≠ ∅ )
264		n0	⊢ ( ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) ≠ ∅ ↔ ∃ 𝑛 𝑛 ∈ ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) )
265		inss2	⊢ ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) ⊆ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) )
266	265	sseli	⊢ ( 𝑛 ∈ ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) → 𝑛 ∈ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) )
267		fvelima	⊢ ( ( Fun 𝐹 ∧ 𝑛 ∈ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) → ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝐹 ‘ 𝑘 ) = 𝑛 )
268	266 267	sylan2	⊢ ( ( Fun 𝐹 ∧ 𝑛 ∈ ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) ) → ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝐹 ‘ 𝑘 ) = 𝑛 )
269		inss1	⊢ ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) ⊆ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) )
270	269	sseli	⊢ ( 𝑛 ∈ ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) → 𝑛 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
271	270	adantl	⊢ ( ( Fun 𝐹 ∧ 𝑛 ∈ ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) ) → 𝑛 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
272		eleq1a	⊢ ( 𝑛 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) → ( ( 𝐹 ‘ 𝑘 ) = 𝑛 → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
273	271 272	syl	⊢ ( ( Fun 𝐹 ∧ 𝑛 ∈ ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) ) → ( ( 𝐹 ‘ 𝑘 ) = 𝑛 → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
274	273	reximdv	⊢ ( ( Fun 𝐹 ∧ 𝑛 ∈ ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) ) → ( ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝐹 ‘ 𝑘 ) = 𝑛 → ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
275	268 274	mpd	⊢ ( ( Fun 𝐹 ∧ 𝑛 ∈ ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) ) → ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
276	275	ex	⊢ ( Fun 𝐹 → ( 𝑛 ∈ ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) → ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
277	276	exlimdv	⊢ ( Fun 𝐹 → ( ∃ 𝑛 𝑛 ∈ ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) → ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
278	264 277	biimtrid	⊢ ( Fun 𝐹 → ( ( ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝐹 “ ( ℤ_≥ ‘ 𝑚 ) ) ) ≠ ∅ → ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
279	239 263 278	sylc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
280		r19.29	⊢ ( ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) ∧ ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) → ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
281		uznnssnn	⊢ ( 𝑚 ∈ ℕ → ( ℤ_≥ ‘ 𝑚 ) ⊆ ℕ )
282	281	ad2antll	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → ( ℤ_≥ ‘ 𝑚 ) ⊆ ℕ )
283		simprlr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
284	7	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
285		simplrl	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → 𝑟 ∈ ℝ⁺ )
286	285 232	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( 𝑟 / 2 ) ∈ ℝ⁺ )
287	286	rpxrd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( 𝑟 / 2 ) ∈ ℝ^* )
288		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → 𝑦 ∈ 𝑋 )
289	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → 𝐹 : ℕ ⟶ 𝑋 )
290		eluznn	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ) → 𝑘 ∈ ℕ )
291	290	ad2ant2lr	⊢ ( ( ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ) → 𝑘 ∈ ℕ )
292	291	ad2ant2lr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → 𝑘 ∈ ℕ )
293	289 292	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
294		elbl3	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑟 / 2 ) ∈ ℝ^* ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < ( 𝑟 / 2 ) ) )
295	284 287 288 293 294	syl22anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < ( 𝑟 / 2 ) ) )
296	283 295	mpbid	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < ( 𝑟 / 2 ) )
297	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
298		simprr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) )
299		eluznn	⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) → 𝑛 ∈ ℕ )
300	292 298 299	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → 𝑛 ∈ ℕ )
301	289 300	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 )
302		metcl	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
303	297 293 301 302	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
304		metcl	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ∈ ℝ )
305	297 293 288 304	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ∈ ℝ )
306	286	rpred	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( 𝑟 / 2 ) ∈ ℝ )
307		lt2add	⊢ ( ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ∈ ℝ ) ∧ ( ( 𝑟 / 2 ) ∈ ℝ ∧ ( 𝑟 / 2 ) ∈ ℝ ) ) → ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < ( 𝑟 / 2 ) ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ) < ( ( 𝑟 / 2 ) + ( 𝑟 / 2 ) ) ) )
308	303 305 306 306 307	syl22anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) < ( 𝑟 / 2 ) ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ) < ( ( 𝑟 / 2 ) + ( 𝑟 / 2 ) ) ) )
309	296 308	mpan2d	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ) < ( ( 𝑟 / 2 ) + ( 𝑟 / 2 ) ) ) )
310	285	rpcnd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → 𝑟 ∈ ℂ )
311	310	2halvesd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( ( 𝑟 / 2 ) + ( 𝑟 / 2 ) ) = 𝑟 )
312	311	breq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ) < ( ( 𝑟 / 2 ) + ( 𝑟 / 2 ) ) ↔ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ) < 𝑟 ) )
313	309 312	sylibd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ) < 𝑟 ) )
314		mettri2	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) ≤ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ) )
315	297 293 301 288 314	syl13anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) ≤ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ) )
316		metcl	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) ∈ ℝ )
317	297 301 288 316	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) ∈ ℝ )
318	303 305	readdcld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ) ∈ ℝ )
319	285	rpred	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → 𝑟 ∈ ℝ )
320		lelttr	⊢ ( ( ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) ∈ ℝ ∧ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( ( ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) ≤ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ) ∧ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ) < 𝑟 ) → ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) )
321	317 318 319 320	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( ( ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) ≤ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ) ∧ ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ) < 𝑟 ) → ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) )
322	315 321	mpand	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑦 ) ) < 𝑟 → ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) )
323	313 322	syld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) → ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) )
324	323	anassrs	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ) ∧ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) → ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) )
325	324	ralimdva	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ) → ( ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) → ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) )
326	325	expr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) → ( ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) → ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) ) )
327	326	com23	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ) → ( ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) → ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) ) )
328	327	impd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ) → ( ( ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) → ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) )
329	328	reximdva	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → ( ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) → ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) )
330		ssrexv	⊢ ( ( ℤ_≥ ‘ 𝑚 ) ⊆ ℕ → ( ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 → ∃ 𝑘 ∈ ℕ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) )
331	282 329 330	sylsyld	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → ( ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) → ∃ 𝑘 ∈ ℕ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) )
332	221 331	syldanl	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → ( ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) → ∃ 𝑘 ∈ ℕ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) )
333	280 332	syl5	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → ( ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) ∧ ∃ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) → ∃ 𝑘 ∈ ℕ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) )
334	279 333	mpan2d	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ⁺ ∧ 𝑚 ∈ ℕ ) ) → ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) → ∃ 𝑘 ∈ ℕ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) )
335	334	anassrs	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑚 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) → ∃ 𝑘 ∈ ℕ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) )
336	335	rexlimdva	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ 𝑟 ∈ ℝ⁺ ) → ( ∃ 𝑚 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑚 ) ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < ( 𝑟 / 2 ) → ∃ 𝑘 ∈ ℕ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) )
337	237 336	mpd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) ∧ 𝑟 ∈ ℝ⁺ ) → ∃ 𝑘 ∈ ℕ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 )
338	337	ralrimiva	⊢ ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑘 ∈ ℕ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 )
339		eqidd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
340	1 7 130 222 339 5	lmmbrf	⊢ ( 𝜑 → ( 𝐹 ( ⇝_𝑡 ‘ 𝐽 ) 𝑦 ↔ ( 𝑦 ∈ 𝑋 ∧ ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑘 ∈ ℕ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) ) )
341	340	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → ( 𝐹 ( ⇝_𝑡 ‘ 𝐽 ) 𝑦 ↔ ( 𝑦 ∈ 𝑋 ∧ ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑘 ∈ ℕ ∀ 𝑛 ∈ ( ℤ_≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑛 ) 𝐷 𝑦 ) < 𝑟 ) ) )
342	221 338 341	mpbir2and	⊢ ( ( 𝜑 ∧ ∀ 𝑢 ∈ ran ℤ_≥ 𝑦 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) ) → 𝐹 ( ⇝_𝑡 ‘ 𝐽 ) 𝑦 )
343	201 342	sylan2br	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ) → 𝐹 ( ⇝_𝑡 ‘ 𝐽 ) 𝑦 )
344		releldm	⊢ ( ( Rel ( ⇝_𝑡 ‘ 𝐽 ) ∧ 𝐹 ( ⇝_𝑡 ‘ 𝐽 ) 𝑦 ) → 𝐹 ∈ dom ( ⇝_𝑡 ‘ 𝐽 ) )
345	190 343 344	sylancr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∩ { 𝑘 ∣ ∃ 𝑢 ∈ ran ℤ_≥ 𝑘 = ( ( cls ‘ 𝐽 ) ‘ ( 𝐹 “ 𝑢 ) ) } ) → 𝐹 ∈ dom ( ⇝_𝑡 ‘ 𝐽 ) )
346	189 345	exlimddv	⊢ ( 𝜑 → 𝐹 ∈ dom ( ⇝_𝑡 ‘ 𝐽 ) )

Metamath Proof Explorer

Theorem heibor1lem

Proof