Metamath Proof Explorer

Theorem 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 syl5bi ⊢ ( 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 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( 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 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ ) ) ∧ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑦 ( 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 ( ⇝𝑡 ‘ 𝐽 ) )