Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  heibor1lem Structured version   Visualization version   GIF version

Theorem heibor1lem 36980
Description: Lemma for heibor1 36981. A compact metric space is complete. This proof works by considering the collection cls(𝐹 β€œ (β„€β‰₯β€˜π‘›)) for each 𝑛 ∈ β„•, 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 (𝐹 β€œ (β„€β‰₯β€˜π‘š)) for some π‘š. Thus, by compactness, the intersection contains a point 𝑦, which must then be the convergent point of 𝐹. (Contributed by Jeff Madsen, 17-Jan-2014.) (Revised by Mario Carneiro, 5-Jun-2014.)
Hypotheses
Ref Expression
heibor.1 𝐽 = (MetOpenβ€˜π·)
heibor1.3 (πœ‘ β†’ 𝐷 ∈ (Metβ€˜π‘‹))
heibor1.4 (πœ‘ β†’ 𝐽 ∈ Comp)
heibor1.5 (πœ‘ β†’ 𝐹 ∈ (Cauβ€˜π·))
heibor1.6 (πœ‘ β†’ 𝐹:β„•βŸΆπ‘‹)
Assertion
Ref Expression
heibor1lem (πœ‘ β†’ 𝐹 ∈ dom (β‡π‘‘β€˜π½))

Proof of Theorem heibor1lem
Dummy variables 𝑛 𝑦 π‘˜ π‘Ÿ 𝑒 π‘š are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 heibor1.4 . . 3 (πœ‘ β†’ 𝐽 ∈ Comp)
2 heibor1.3 . . . . . . . . . 10 (πœ‘ β†’ 𝐷 ∈ (Metβ€˜π‘‹))
3 metxmet 24060 . . . . . . . . . 10 (𝐷 ∈ (Metβ€˜π‘‹) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
42, 3syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
5 heibor.1 . . . . . . . . . 10 𝐽 = (MetOpenβ€˜π·)
65mopntop 24166 . . . . . . . . 9 (𝐷 ∈ (∞Metβ€˜π‘‹) β†’ 𝐽 ∈ Top)
74, 6syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐽 ∈ Top)
8 imassrn 6069 . . . . . . . . 9 (𝐹 β€œ 𝑒) βŠ† ran 𝐹
9 heibor1.6 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹:β„•βŸΆπ‘‹)
109frnd 6724 . . . . . . . . . 10 (πœ‘ β†’ ran 𝐹 βŠ† 𝑋)
115mopnuni 24167 . . . . . . . . . . 11 (𝐷 ∈ (∞Metβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
124, 11syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝑋 = βˆͺ 𝐽)
1310, 12sseqtrd 4021 . . . . . . . . 9 (πœ‘ β†’ ran 𝐹 βŠ† βˆͺ 𝐽)
148, 13sstrid 3992 . . . . . . . 8 (πœ‘ β†’ (𝐹 β€œ 𝑒) βŠ† βˆͺ 𝐽)
15 eqid 2730 . . . . . . . . 9 βˆͺ 𝐽 = βˆͺ 𝐽
1615clscld 22771 . . . . . . . 8 ((𝐽 ∈ Top ∧ (𝐹 β€œ 𝑒) βŠ† βˆͺ 𝐽) β†’ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∈ (Clsdβ€˜π½))
177, 14, 16syl2anc 582 . . . . . . 7 (πœ‘ β†’ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∈ (Clsdβ€˜π½))
18 eleq1a 2826 . . . . . . 7 (((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∈ (Clsdβ€˜π½) β†’ (π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ π‘˜ ∈ (Clsdβ€˜π½)))
1917, 18syl 17 . . . . . 6 (πœ‘ β†’ (π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ π‘˜ ∈ (Clsdβ€˜π½)))
2019rexlimdvw 3158 . . . . 5 (πœ‘ β†’ (βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ π‘˜ ∈ (Clsdβ€˜π½)))
2120abssdv 4064 . . . 4 (πœ‘ β†’ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} βŠ† (Clsdβ€˜π½))
22 fvex 6903 . . . . 5 (Clsdβ€˜π½) ∈ V
2322elpw2 5344 . . . 4 ({π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∈ 𝒫 (Clsdβ€˜π½) ↔ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} βŠ† (Clsdβ€˜π½))
2421, 23sylibr 233 . . 3 (πœ‘ β†’ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∈ 𝒫 (Clsdβ€˜π½))
25 elin 3963 . . . . . . 7 (π‘Ÿ ∈ (𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∩ Fin) ↔ (π‘Ÿ ∈ 𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∧ π‘Ÿ ∈ Fin))
26 velpw 4606 . . . . . . . . 9 (π‘Ÿ ∈ 𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ↔ π‘Ÿ βŠ† {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})
27 ssabral 4058 . . . . . . . . 9 (π‘Ÿ βŠ† {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ↔ βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
2826, 27bitri 274 . . . . . . . 8 (π‘Ÿ ∈ 𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ↔ βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
2928anbi1i 622 . . . . . . 7 ((π‘Ÿ ∈ 𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∧ π‘Ÿ ∈ Fin) ↔ (βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ π‘Ÿ ∈ Fin))
3025, 29bitri 274 . . . . . 6 (π‘Ÿ ∈ (𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∩ Fin) ↔ (βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ π‘Ÿ ∈ Fin))
31 raleq 3320 . . . . . . . . . . . . . 14 (π‘š = βˆ… β†’ (βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ βˆ€π‘˜ ∈ βˆ… βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
3231anbi2d 627 . . . . . . . . . . . . 13 (π‘š = βˆ… β†’ ((πœ‘ ∧ βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ↔ (πœ‘ ∧ βˆ€π‘˜ ∈ βˆ… βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))))
33 inteq 4952 . . . . . . . . . . . . . . 15 (π‘š = βˆ… β†’ ∩ π‘š = ∩ βˆ…)
3433sseq2d 4013 . . . . . . . . . . . . . 14 (π‘š = βˆ… β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ π‘š ↔ (𝐹 β€œ π‘˜) βŠ† ∩ βˆ…))
3534rexbidv 3176 . . . . . . . . . . . . 13 (π‘š = βˆ… β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘š ↔ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ βˆ…))
3632, 35imbi12d 343 . . . . . . . . . . . 12 (π‘š = βˆ… β†’ (((πœ‘ ∧ βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘š) ↔ ((πœ‘ ∧ βˆ€π‘˜ ∈ βˆ… βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ βˆ…)))
37 raleq 3320 . . . . . . . . . . . . . 14 (π‘š = 𝑦 β†’ (βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ βˆ€π‘˜ ∈ 𝑦 βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
3837anbi2d 627 . . . . . . . . . . . . 13 (π‘š = 𝑦 β†’ ((πœ‘ ∧ βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ↔ (πœ‘ ∧ βˆ€π‘˜ ∈ 𝑦 βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))))
39 inteq 4952 . . . . . . . . . . . . . . 15 (π‘š = 𝑦 β†’ ∩ π‘š = ∩ 𝑦)
4039sseq2d 4013 . . . . . . . . . . . . . 14 (π‘š = 𝑦 β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ π‘š ↔ (𝐹 β€œ π‘˜) βŠ† ∩ 𝑦))
4140rexbidv 3176 . . . . . . . . . . . . 13 (π‘š = 𝑦 β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘š ↔ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦))
4238, 41imbi12d 343 . . . . . . . . . . . 12 (π‘š = 𝑦 β†’ (((πœ‘ ∧ βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘š) ↔ ((πœ‘ ∧ βˆ€π‘˜ ∈ 𝑦 βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦)))
43 raleq 3320 . . . . . . . . . . . . . 14 (π‘š = (𝑦 βˆͺ {𝑛}) β†’ (βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
4443anbi2d 627 . . . . . . . . . . . . 13 (π‘š = (𝑦 βˆͺ {𝑛}) β†’ ((πœ‘ ∧ βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ↔ (πœ‘ ∧ βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))))
45 inteq 4952 . . . . . . . . . . . . . . 15 (π‘š = (𝑦 βˆͺ {𝑛}) β†’ ∩ π‘š = ∩ (𝑦 βˆͺ {𝑛}))
4645sseq2d 4013 . . . . . . . . . . . . . 14 (π‘š = (𝑦 βˆͺ {𝑛}) β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ π‘š ↔ (𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
4746rexbidv 3176 . . . . . . . . . . . . 13 (π‘š = (𝑦 βˆͺ {𝑛}) β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘š ↔ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
4844, 47imbi12d 343 . . . . . . . . . . . 12 (π‘š = (𝑦 βˆͺ {𝑛}) β†’ (((πœ‘ ∧ βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘š) ↔ ((πœ‘ ∧ βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛}))))
49 raleq 3320 . . . . . . . . . . . . . 14 (π‘š = π‘Ÿ β†’ (βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
5049anbi2d 627 . . . . . . . . . . . . 13 (π‘š = π‘Ÿ β†’ ((πœ‘ ∧ βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ↔ (πœ‘ ∧ βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))))
51 inteq 4952 . . . . . . . . . . . . . . 15 (π‘š = π‘Ÿ β†’ ∩ π‘š = ∩ π‘Ÿ)
5251sseq2d 4013 . . . . . . . . . . . . . 14 (π‘š = π‘Ÿ β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ π‘š ↔ (𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ))
5352rexbidv 3176 . . . . . . . . . . . . 13 (π‘š = π‘Ÿ β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘š ↔ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ))
5450, 53imbi12d 343 . . . . . . . . . . . 12 (π‘š = π‘Ÿ β†’ (((πœ‘ ∧ βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘š) ↔ ((πœ‘ ∧ βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ)))
55 uzf 12829 . . . . . . . . . . . . . . . 16 β„€β‰₯:β„€βŸΆπ’« β„€
56 ffn 6716 . . . . . . . . . . . . . . . 16 (β„€β‰₯:β„€βŸΆπ’« β„€ β†’ β„€β‰₯ Fn β„€)
5755, 56ax-mp 5 . . . . . . . . . . . . . . 15 β„€β‰₯ Fn β„€
58 0z 12573 . . . . . . . . . . . . . . 15 0 ∈ β„€
59 fnfvelrn 7081 . . . . . . . . . . . . . . 15 ((β„€β‰₯ Fn β„€ ∧ 0 ∈ β„€) β†’ (β„€β‰₯β€˜0) ∈ ran β„€β‰₯)
6057, 58, 59mp2an 688 . . . . . . . . . . . . . 14 (β„€β‰₯β€˜0) ∈ ran β„€β‰₯
61 ssv 4005 . . . . . . . . . . . . . . 15 (𝐹 β€œ (β„€β‰₯β€˜0)) βŠ† V
62 int0 4965 . . . . . . . . . . . . . . 15 ∩ βˆ… = V
6361, 62sseqtrri 4018 . . . . . . . . . . . . . 14 (𝐹 β€œ (β„€β‰₯β€˜0)) βŠ† ∩ βˆ…
64 imaeq2 6054 . . . . . . . . . . . . . . . 16 (π‘˜ = (β„€β‰₯β€˜0) β†’ (𝐹 β€œ π‘˜) = (𝐹 β€œ (β„€β‰₯β€˜0)))
6564sseq1d 4012 . . . . . . . . . . . . . . 15 (π‘˜ = (β„€β‰₯β€˜0) β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ βˆ… ↔ (𝐹 β€œ (β„€β‰₯β€˜0)) βŠ† ∩ βˆ…))
6665rspcev 3611 . . . . . . . . . . . . . 14 (((β„€β‰₯β€˜0) ∈ ran β„€β‰₯ ∧ (𝐹 β€œ (β„€β‰₯β€˜0)) βŠ† ∩ βˆ…) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ βˆ…)
6760, 63, 66mp2an 688 . . . . . . . . . . . . 13 βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ βˆ…
6867a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ βˆ€π‘˜ ∈ βˆ… βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ βˆ…)
69 ssun1 4171 . . . . . . . . . . . . . . . . 17 𝑦 βŠ† (𝑦 βˆͺ {𝑛})
70 ssralv 4049 . . . . . . . . . . . . . . . . 17 (𝑦 βŠ† (𝑦 βˆͺ {𝑛}) β†’ (βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ βˆ€π‘˜ ∈ 𝑦 βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
7169, 70ax-mp 5 . . . . . . . . . . . . . . . 16 (βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ βˆ€π‘˜ ∈ 𝑦 βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
7271anim2i 615 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ (πœ‘ ∧ βˆ€π‘˜ ∈ 𝑦 βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
7372imim1i 63 . . . . . . . . . . . . . 14 (((πœ‘ ∧ βˆ€π‘˜ ∈ 𝑦 βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦) β†’ ((πœ‘ ∧ βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦))
74 ssun2 4172 . . . . . . . . . . . . . . . . . 18 {𝑛} βŠ† (𝑦 βˆͺ {𝑛})
75 ssralv 4049 . . . . . . . . . . . . . . . . . 18 ({𝑛} βŠ† (𝑦 βˆͺ {𝑛}) β†’ (βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ βˆ€π‘˜ ∈ {𝑛}βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
7674, 75ax-mp 5 . . . . . . . . . . . . . . . . 17 (βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ βˆ€π‘˜ ∈ {𝑛}βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
77 vex 3476 . . . . . . . . . . . . . . . . . 18 𝑛 ∈ V
78 eqeq1 2734 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑛 β†’ (π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ 𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
7978rexbidv 3176 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑛 β†’ (βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ βˆƒπ‘’ ∈ ran β„€β‰₯𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
8077, 79ralsn 4684 . . . . . . . . . . . . . . . . 17 (βˆ€π‘˜ ∈ {𝑛}βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ βˆƒπ‘’ ∈ ran β„€β‰₯𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
8176, 80sylib 217 . . . . . . . . . . . . . . . 16 (βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ βˆƒπ‘’ ∈ ran β„€β‰₯𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
82 uzin2 15295 . . . . . . . . . . . . . . . . . . . 20 ((𝑒 ∈ ran β„€β‰₯ ∧ π‘˜ ∈ ran β„€β‰₯) β†’ (𝑒 ∩ π‘˜) ∈ ran β„€β‰₯)
838, 10sstrid 3992 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (𝐹 β€œ 𝑒) βŠ† 𝑋)
8483, 12sseqtrd 4021 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝐹 β€œ 𝑒) βŠ† βˆͺ 𝐽)
8515sscls 22780 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 ∈ Top ∧ (𝐹 β€œ 𝑒) βŠ† βˆͺ 𝐽) β†’ (𝐹 β€œ 𝑒) βŠ† ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
867, 84, 85syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (𝐹 β€œ 𝑒) βŠ† ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
87 sseq2 4007 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ ((𝐹 β€œ 𝑒) βŠ† 𝑛 ↔ (𝐹 β€œ 𝑒) βŠ† ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
8886, 87syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ (𝐹 β€œ 𝑒) βŠ† 𝑛))
89 inss2 4228 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑒 ∩ π‘˜) βŠ† π‘˜
90 inss1 4227 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑒 ∩ π‘˜) βŠ† 𝑒
91 imass2 6100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑒 ∩ π‘˜) βŠ† π‘˜ β†’ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† (𝐹 β€œ π‘˜))
92 imass2 6100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑒 ∩ π‘˜) βŠ† 𝑒 β†’ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† (𝐹 β€œ 𝑒))
9391, 92anim12i 611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑒 ∩ π‘˜) βŠ† π‘˜ ∧ (𝑒 ∩ π‘˜) βŠ† 𝑒) β†’ ((𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† (𝐹 β€œ π‘˜) ∧ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† (𝐹 β€œ 𝑒)))
94 ssin 4229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† (𝐹 β€œ π‘˜) ∧ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† (𝐹 β€œ 𝑒)) ↔ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ((𝐹 β€œ π‘˜) ∩ (𝐹 β€œ 𝑒)))
9593, 94sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑒 ∩ π‘˜) βŠ† π‘˜ ∧ (𝑒 ∩ π‘˜) βŠ† 𝑒) β†’ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ((𝐹 β€œ π‘˜) ∩ (𝐹 β€œ 𝑒)))
9689, 90, 95mp2an 688 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ((𝐹 β€œ π‘˜) ∩ (𝐹 β€œ 𝑒))
97 ss2in 4235 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐹 β€œ π‘˜) βŠ† ∩ 𝑦 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑛) β†’ ((𝐹 β€œ π‘˜) ∩ (𝐹 β€œ 𝑒)) βŠ† (∩ 𝑦 ∩ 𝑛))
9896, 97sstrid 3992 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹 β€œ π‘˜) βŠ† ∩ 𝑦 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑛) β†’ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† (∩ 𝑦 ∩ 𝑛))
9977intunsn 4992 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ∩ (𝑦 βˆͺ {𝑛}) = (∩ 𝑦 ∩ 𝑛)
10098, 99sseqtrrdi 4032 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 β€œ π‘˜) βŠ† ∩ 𝑦 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑛) β†’ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ∩ (𝑦 βˆͺ {𝑛}))
101100expcom 412 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 β€œ 𝑒) βŠ† 𝑛 β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ 𝑦 β†’ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
10288, 101syl6 35 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ 𝑦 β†’ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ∩ (𝑦 βˆͺ {𝑛}))))
103102impd 409 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ (𝐹 β€œ π‘˜) βŠ† ∩ 𝑦) β†’ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
104 imaeq2 6054 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘š = (𝑒 ∩ π‘˜) β†’ (𝐹 β€œ π‘š) = (𝐹 β€œ (𝑒 ∩ π‘˜)))
105104sseq1d 4012 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘š = (𝑒 ∩ π‘˜) β†’ ((𝐹 β€œ π‘š) βŠ† ∩ (𝑦 βˆͺ {𝑛}) ↔ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
106105rspcev 3611 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑒 ∩ π‘˜) ∈ ran β„€β‰₯ ∧ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ∩ (𝑦 βˆͺ {𝑛})) β†’ βˆƒπ‘š ∈ ran β„€β‰₯(𝐹 β€œ π‘š) βŠ† ∩ (𝑦 βˆͺ {𝑛}))
107106expcom 412 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ∩ (𝑦 βˆͺ {𝑛}) β†’ ((𝑒 ∩ π‘˜) ∈ ran β„€β‰₯ β†’ βˆƒπ‘š ∈ ran β„€β‰₯(𝐹 β€œ π‘š) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
108103, 107syl6 35 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ (𝐹 β€œ π‘˜) βŠ† ∩ 𝑦) β†’ ((𝑒 ∩ π‘˜) ∈ ran β„€β‰₯ β†’ βˆƒπ‘š ∈ ran β„€β‰₯(𝐹 β€œ π‘š) βŠ† ∩ (𝑦 βˆͺ {𝑛}))))
109108com23 86 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑒 ∩ π‘˜) ∈ ran β„€β‰₯ β†’ ((𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ (𝐹 β€œ π‘˜) βŠ† ∩ 𝑦) β†’ βˆƒπ‘š ∈ ran β„€β‰₯(𝐹 β€œ π‘š) βŠ† ∩ (𝑦 βˆͺ {𝑛}))))
11082, 109syl5 34 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((𝑒 ∈ ran β„€β‰₯ ∧ π‘˜ ∈ ran β„€β‰₯) β†’ ((𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ (𝐹 β€œ π‘˜) βŠ† ∩ 𝑦) β†’ βˆƒπ‘š ∈ ran β„€β‰₯(𝐹 β€œ π‘š) βŠ† ∩ (𝑦 βˆͺ {𝑛}))))
111110rexlimdvv 3208 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (βˆƒπ‘’ ∈ ran β„€β‰₯βˆƒπ‘˜ ∈ ran β„€β‰₯(𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ (𝐹 β€œ π‘˜) βŠ† ∩ 𝑦) β†’ βˆƒπ‘š ∈ ran β„€β‰₯(𝐹 β€œ π‘š) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
112 reeanv 3224 . . . . . . . . . . . . . . . . . 18 (βˆƒπ‘’ ∈ ran β„€β‰₯βˆƒπ‘˜ ∈ ran β„€β‰₯(𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ (𝐹 β€œ π‘˜) βŠ† ∩ 𝑦) ↔ (βˆƒπ‘’ ∈ ran β„€β‰₯𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦))
113 imaeq2 6054 . . . . . . . . . . . . . . . . . . . 20 (π‘š = π‘˜ β†’ (𝐹 β€œ π‘š) = (𝐹 β€œ π‘˜))
114113sseq1d 4012 . . . . . . . . . . . . . . . . . . 19 (π‘š = π‘˜ β†’ ((𝐹 β€œ π‘š) βŠ† ∩ (𝑦 βˆͺ {𝑛}) ↔ (𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
115114cbvrexvw 3233 . . . . . . . . . . . . . . . . . 18 (βˆƒπ‘š ∈ ran β„€β‰₯(𝐹 β€œ π‘š) βŠ† ∩ (𝑦 βˆͺ {𝑛}) ↔ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛}))
116111, 112, 1153imtr3g 294 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((βˆƒπ‘’ ∈ ran β„€β‰₯𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
117116expd 414 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βˆƒπ‘’ ∈ ran β„€β‰₯𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦 β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛}))))
11881, 117syl5 34 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦 β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛}))))
119118imp 405 . . . . . . . . . . . . . 14 ((πœ‘ ∧ βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦 β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
12073, 119sylcom 30 . . . . . . . . . . . . 13 (((πœ‘ ∧ βˆ€π‘˜ ∈ 𝑦 βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦) β†’ ((πœ‘ ∧ βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
121120a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ Fin β†’ (((πœ‘ ∧ βˆ€π‘˜ ∈ 𝑦 βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦) β†’ ((πœ‘ ∧ βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛}))))
12236, 42, 48, 54, 68, 121findcard2 9166 . . . . . . . . . . 11 (π‘Ÿ ∈ Fin β†’ ((πœ‘ ∧ βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ))
123122com12 32 . . . . . . . . . 10 ((πœ‘ ∧ βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ (π‘Ÿ ∈ Fin β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ))
124123impr 453 . . . . . . . . 9 ((πœ‘ ∧ (βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ π‘Ÿ ∈ Fin)) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ)
1259ffnd 6717 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹 Fn β„•)
126 inss1 4227 . . . . . . . . . . . . . . 15 (π‘˜ ∩ β„•) βŠ† π‘˜
127 imass2 6100 . . . . . . . . . . . . . . 15 ((π‘˜ ∩ β„•) βŠ† π‘˜ β†’ (𝐹 β€œ (π‘˜ ∩ β„•)) βŠ† (𝐹 β€œ π‘˜))
128126, 127ax-mp 5 . . . . . . . . . . . . . 14 (𝐹 β€œ (π‘˜ ∩ β„•)) βŠ† (𝐹 β€œ π‘˜)
129 nnuz 12869 . . . . . . . . . . . . . . . . . . . 20 β„• = (β„€β‰₯β€˜1)
130 1z 12596 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ β„€
131 fnfvelrn 7081 . . . . . . . . . . . . . . . . . . . . 21 ((β„€β‰₯ Fn β„€ ∧ 1 ∈ β„€) β†’ (β„€β‰₯β€˜1) ∈ ran β„€β‰₯)
13257, 130, 131mp2an 688 . . . . . . . . . . . . . . . . . . . 20 (β„€β‰₯β€˜1) ∈ ran β„€β‰₯
133129, 132eqeltri 2827 . . . . . . . . . . . . . . . . . . 19 β„• ∈ ran β„€β‰₯
134 uzin2 15295 . . . . . . . . . . . . . . . . . . 19 ((π‘˜ ∈ ran β„€β‰₯ ∧ β„• ∈ ran β„€β‰₯) β†’ (π‘˜ ∩ β„•) ∈ ran β„€β‰₯)
135133, 134mpan2 687 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ ran β„€β‰₯ β†’ (π‘˜ ∩ β„•) ∈ ran β„€β‰₯)
136 uzn0 12843 . . . . . . . . . . . . . . . . . 18 ((π‘˜ ∩ β„•) ∈ ran β„€β‰₯ β†’ (π‘˜ ∩ β„•) β‰  βˆ…)
137135, 136syl 17 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ ran β„€β‰₯ β†’ (π‘˜ ∩ β„•) β‰  βˆ…)
138 n0 4345 . . . . . . . . . . . . . . . . 17 ((π‘˜ ∩ β„•) β‰  βˆ… ↔ βˆƒπ‘¦ 𝑦 ∈ (π‘˜ ∩ β„•))
139137, 138sylib 217 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ ran β„€β‰₯ β†’ βˆƒπ‘¦ 𝑦 ∈ (π‘˜ ∩ β„•))
140 fnfun 6648 . . . . . . . . . . . . . . . . . . 19 (𝐹 Fn β„• β†’ Fun 𝐹)
141 inss2 4228 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ ∩ β„•) βŠ† β„•
142 fndm 6651 . . . . . . . . . . . . . . . . . . . 20 (𝐹 Fn β„• β†’ dom 𝐹 = β„•)
143141, 142sseqtrrid 4034 . . . . . . . . . . . . . . . . . . 19 (𝐹 Fn β„• β†’ (π‘˜ ∩ β„•) βŠ† dom 𝐹)
144 funfvima2 7234 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹 ∧ (π‘˜ ∩ β„•) βŠ† dom 𝐹) β†’ (𝑦 ∈ (π‘˜ ∩ β„•) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ (π‘˜ ∩ β„•))))
145140, 143, 144syl2anc 582 . . . . . . . . . . . . . . . . . 18 (𝐹 Fn β„• β†’ (𝑦 ∈ (π‘˜ ∩ β„•) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ (π‘˜ ∩ β„•))))
146 ne0i 4333 . . . . . . . . . . . . . . . . . 18 ((πΉβ€˜π‘¦) ∈ (𝐹 β€œ (π‘˜ ∩ β„•)) β†’ (𝐹 β€œ (π‘˜ ∩ β„•)) β‰  βˆ…)
147145, 146syl6 35 . . . . . . . . . . . . . . . . 17 (𝐹 Fn β„• β†’ (𝑦 ∈ (π‘˜ ∩ β„•) β†’ (𝐹 β€œ (π‘˜ ∩ β„•)) β‰  βˆ…))
148147exlimdv 1934 . . . . . . . . . . . . . . . 16 (𝐹 Fn β„• β†’ (βˆƒπ‘¦ 𝑦 ∈ (π‘˜ ∩ β„•) β†’ (𝐹 β€œ (π‘˜ ∩ β„•)) β‰  βˆ…))
149139, 148syl5 34 . . . . . . . . . . . . . . 15 (𝐹 Fn β„• β†’ (π‘˜ ∈ ran β„€β‰₯ β†’ (𝐹 β€œ (π‘˜ ∩ β„•)) β‰  βˆ…))
150149imp 405 . . . . . . . . . . . . . 14 ((𝐹 Fn β„• ∧ π‘˜ ∈ ran β„€β‰₯) β†’ (𝐹 β€œ (π‘˜ ∩ β„•)) β‰  βˆ…)
151 ssn0 4399 . . . . . . . . . . . . . 14 (((𝐹 β€œ (π‘˜ ∩ β„•)) βŠ† (𝐹 β€œ π‘˜) ∧ (𝐹 β€œ (π‘˜ ∩ β„•)) β‰  βˆ…) β†’ (𝐹 β€œ π‘˜) β‰  βˆ…)
152128, 150, 151sylancr 585 . . . . . . . . . . . . 13 ((𝐹 Fn β„• ∧ π‘˜ ∈ ran β„€β‰₯) β†’ (𝐹 β€œ π‘˜) β‰  βˆ…)
153 ssn0 4399 . . . . . . . . . . . . . 14 (((𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ ∧ (𝐹 β€œ π‘˜) β‰  βˆ…) β†’ ∩ π‘Ÿ β‰  βˆ…)
154153expcom 412 . . . . . . . . . . . . 13 ((𝐹 β€œ π‘˜) β‰  βˆ… β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ β†’ ∩ π‘Ÿ β‰  βˆ…))
155152, 154syl 17 . . . . . . . . . . . 12 ((𝐹 Fn β„• ∧ π‘˜ ∈ ran β„€β‰₯) β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ β†’ ∩ π‘Ÿ β‰  βˆ…))
156155rexlimdva 3153 . . . . . . . . . . 11 (𝐹 Fn β„• β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ β†’ ∩ π‘Ÿ β‰  βˆ…))
157125, 156syl 17 . . . . . . . . . 10 (πœ‘ β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ β†’ ∩ π‘Ÿ β‰  βˆ…))
158157adantr 479 . . . . . . . . 9 ((πœ‘ ∧ (βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ π‘Ÿ ∈ Fin)) β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ β†’ ∩ π‘Ÿ β‰  βˆ…))
159124, 158mpd 15 . . . . . . . 8 ((πœ‘ ∧ (βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ π‘Ÿ ∈ Fin)) β†’ ∩ π‘Ÿ β‰  βˆ…)
160159necomd 2994 . . . . . . 7 ((πœ‘ ∧ (βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ π‘Ÿ ∈ Fin)) β†’ βˆ… β‰  ∩ π‘Ÿ)
161160neneqd 2943 . . . . . 6 ((πœ‘ ∧ (βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ π‘Ÿ ∈ Fin)) β†’ Β¬ βˆ… = ∩ π‘Ÿ)
16230, 161sylan2b 592 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∩ Fin)) β†’ Β¬ βˆ… = ∩ π‘Ÿ)
163162nrexdv 3147 . . . 4 (πœ‘ β†’ Β¬ βˆƒπ‘Ÿ ∈ (𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∩ Fin)βˆ… = ∩ π‘Ÿ)
164 0ex 5306 . . . . 5 βˆ… ∈ V
165 zex 12571 . . . . . . . 8 β„€ ∈ V
166165pwex 5377 . . . . . . 7 𝒫 β„€ ∈ V
167 frn 6723 . . . . . . . 8 (β„€β‰₯:β„€βŸΆπ’« β„€ β†’ ran β„€β‰₯ βŠ† 𝒫 β„€)
16855, 167ax-mp 5 . . . . . . 7 ran β„€β‰₯ βŠ† 𝒫 β„€
169166, 168ssexi 5321 . . . . . 6 ran β„€β‰₯ ∈ V
170169abrexex 7951 . . . . 5 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∈ V
171 elfi 9410 . . . . 5 ((βˆ… ∈ V ∧ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∈ V) β†’ (βˆ… ∈ (fiβ€˜{π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}) ↔ βˆƒπ‘Ÿ ∈ (𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∩ Fin)βˆ… = ∩ π‘Ÿ))
172164, 170, 171mp2an 688 . . . 4 (βˆ… ∈ (fiβ€˜{π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}) ↔ βˆƒπ‘Ÿ ∈ (𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∩ Fin)βˆ… = ∩ π‘Ÿ)
173163, 172sylnibr 328 . . 3 (πœ‘ β†’ Β¬ βˆ… ∈ (fiβ€˜{π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}))
174 cmptop 23119 . . . . . 6 (𝐽 ∈ Comp β†’ 𝐽 ∈ Top)
175 cmpfi 23132 . . . . . 6 (𝐽 ∈ Top β†’ (𝐽 ∈ Comp ↔ βˆ€π‘š ∈ 𝒫 (Clsdβ€˜π½)(Β¬ βˆ… ∈ (fiβ€˜π‘š) β†’ ∩ π‘š β‰  βˆ…)))
176174, 175syl 17 . . . . 5 (𝐽 ∈ Comp β†’ (𝐽 ∈ Comp ↔ βˆ€π‘š ∈ 𝒫 (Clsdβ€˜π½)(Β¬ βˆ… ∈ (fiβ€˜π‘š) β†’ ∩ π‘š β‰  βˆ…)))
177176ibi 266 . . . 4 (𝐽 ∈ Comp β†’ βˆ€π‘š ∈ 𝒫 (Clsdβ€˜π½)(Β¬ βˆ… ∈ (fiβ€˜π‘š) β†’ ∩ π‘š β‰  βˆ…))
178 fveq2 6890 . . . . . . . 8 (π‘š = {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β†’ (fiβ€˜π‘š) = (fiβ€˜{π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}))
179178eleq2d 2817 . . . . . . 7 (π‘š = {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β†’ (βˆ… ∈ (fiβ€˜π‘š) ↔ βˆ… ∈ (fiβ€˜{π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})))
180179notbid 317 . . . . . 6 (π‘š = {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β†’ (Β¬ βˆ… ∈ (fiβ€˜π‘š) ↔ Β¬ βˆ… ∈ (fiβ€˜{π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})))
181 inteq 4952 . . . . . . . 8 (π‘š = {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β†’ ∩ π‘š = ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})
182181neeq1d 2998 . . . . . . 7 (π‘š = {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β†’ (∩ π‘š β‰  βˆ… ↔ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β‰  βˆ…))
183 n0 4345 . . . . . . 7 (∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β‰  βˆ… ↔ βˆƒπ‘¦ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})
184182, 183bitrdi 286 . . . . . 6 (π‘š = {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β†’ (∩ π‘š β‰  βˆ… ↔ βˆƒπ‘¦ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}))
185180, 184imbi12d 343 . . . . 5 (π‘š = {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β†’ ((Β¬ βˆ… ∈ (fiβ€˜π‘š) β†’ ∩ π‘š β‰  βˆ…) ↔ (Β¬ βˆ… ∈ (fiβ€˜{π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}) β†’ βˆƒπ‘¦ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})))
186185rspccv 3608 . . . 4 (βˆ€π‘š ∈ 𝒫 (Clsdβ€˜π½)(Β¬ βˆ… ∈ (fiβ€˜π‘š) β†’ ∩ π‘š β‰  βˆ…) β†’ ({π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∈ 𝒫 (Clsdβ€˜π½) β†’ (Β¬ βˆ… ∈ (fiβ€˜{π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}) β†’ βˆƒπ‘¦ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})))
187177, 186syl 17 . . 3 (𝐽 ∈ Comp β†’ ({π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∈ 𝒫 (Clsdβ€˜π½) β†’ (Β¬ βˆ… ∈ (fiβ€˜{π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}) β†’ βˆƒπ‘¦ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})))
1881, 24, 173, 187syl3c 66 . 2 (πœ‘ β†’ βˆƒπ‘¦ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})
189 lmrel 22954 . . 3 Rel (β‡π‘‘β€˜π½)
190 r19.23v 3180 . . . . . 6 (βˆ€π‘’ ∈ ran β„€β‰₯(π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜) ↔ (βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜))
191190albii 1819 . . . . 5 (βˆ€π‘˜βˆ€π‘’ ∈ ran β„€β‰₯(π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜) ↔ βˆ€π‘˜(βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜))
192 fvex 6903 . . . . . . . 8 ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∈ V
193 eleq2 2820 . . . . . . . 8 (π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ (𝑦 ∈ π‘˜ ↔ 𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
194192, 193ceqsalv 3510 . . . . . . 7 (βˆ€π‘˜(π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜) ↔ 𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
195194ralbii 3091 . . . . . 6 (βˆ€π‘’ ∈ ran β„€β‰₯βˆ€π‘˜(π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜) ↔ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
196 ralcom4 3281 . . . . . 6 (βˆ€π‘’ ∈ ran β„€β‰₯βˆ€π‘˜(π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜) ↔ βˆ€π‘˜βˆ€π‘’ ∈ ran β„€β‰₯(π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜))
197195, 196bitr3i 276 . . . . 5 (βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ βˆ€π‘˜βˆ€π‘’ ∈ ran β„€β‰₯(π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜))
198 vex 3476 . . . . . 6 𝑦 ∈ V
199198elintab 4961 . . . . 5 (𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ↔ βˆ€π‘˜(βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜))
200191, 197, 1993bitr4i 302 . . . 4 (βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})
201 eqid 2730 . . . . . . . . . . 11 ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) = ((clsβ€˜π½)β€˜(𝐹 β€œ β„•))
202 imaeq2 6054 . . . . . . . . . . . . 13 (𝑒 = β„• β†’ (𝐹 β€œ 𝑒) = (𝐹 β€œ β„•))
203202fveq2d 6894 . . . . . . . . . . . 12 (𝑒 = β„• β†’ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) = ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)))
204203rspceeqv 3632 . . . . . . . . . . 11 ((β„• ∈ ran β„€β‰₯ ∧ ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) = ((clsβ€˜π½)β€˜(𝐹 β€œ β„•))) β†’ βˆƒπ‘’ ∈ ran β„€β‰₯((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
205133, 201, 204mp2an 688 . . . . . . . . . 10 βˆƒπ‘’ ∈ ran β„€β‰₯((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))
206 fvex 6903 . . . . . . . . . . 11 ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) ∈ V
207 eqeq1 2734 . . . . . . . . . . . 12 (π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) β†’ (π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
208207rexbidv 3176 . . . . . . . . . . 11 (π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) β†’ (βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ βˆƒπ‘’ ∈ ran β„€β‰₯((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
209206, 208elab 3667 . . . . . . . . . 10 (((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) ∈ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ↔ βˆƒπ‘’ ∈ ran β„€β‰₯((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
210205, 209mpbir 230 . . . . . . . . 9 ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) ∈ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}
211 intss1 4966 . . . . . . . . 9 (((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) ∈ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β†’ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} βŠ† ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)))
212210, 211ax-mp 5 . . . . . . . 8 ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} βŠ† ((clsβ€˜π½)β€˜(𝐹 β€œ β„•))
213 imassrn 6069 . . . . . . . . . . 11 (𝐹 β€œ β„•) βŠ† ran 𝐹
214213, 13sstrid 3992 . . . . . . . . . 10 (πœ‘ β†’ (𝐹 β€œ β„•) βŠ† βˆͺ 𝐽)
21515clsss3 22783 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ (𝐹 β€œ β„•) βŠ† βˆͺ 𝐽) β†’ ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) βŠ† βˆͺ 𝐽)
2167, 214, 215syl2anc 582 . . . . . . . . 9 (πœ‘ β†’ ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) βŠ† βˆͺ 𝐽)
217216, 12sseqtrrd 4022 . . . . . . . 8 (πœ‘ β†’ ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) βŠ† 𝑋)
218212, 217sstrid 3992 . . . . . . 7 (πœ‘ β†’ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} βŠ† 𝑋)
219218sselda 3981 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}) β†’ 𝑦 ∈ 𝑋)
220200, 219sylan2b 592 . . . . 5 ((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ 𝑦 ∈ 𝑋)
221 heibor1.5 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹 ∈ (Cauβ€˜π·))
222 1zzd 12597 . . . . . . . . . . . . 13 (πœ‘ β†’ 1 ∈ β„€)
223129, 4, 222iscau3 25026 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐹 ∈ (Cauβ€˜π·) ↔ (𝐹 ∈ (𝑋 ↑pm β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)(π‘˜ ∈ dom 𝐹 ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦))))
224221, 223mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ (𝐹 ∈ (𝑋 ↑pm β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)(π‘˜ ∈ dom 𝐹 ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦)))
225224simprd 494 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)(π‘˜ ∈ dom 𝐹 ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦))
226 simp3 1136 . . . . . . . . . . . . 13 ((π‘˜ ∈ dom 𝐹 ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦) β†’ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦)
227226ralimi 3081 . . . . . . . . . . . 12 (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)(π‘˜ ∈ dom 𝐹 ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦) β†’ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦)
228227reximi 3082 . . . . . . . . . . 11 (βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)(π‘˜ ∈ dom 𝐹 ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦) β†’ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦)
229228ralimi 3081 . . . . . . . . . 10 (βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)(π‘˜ ∈ dom 𝐹 ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦) β†’ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦)
230225, 229syl 17 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦)
231230adantr 479 . . . . . . . 8 ((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦)
232 rphalfcl 13005 . . . . . . . 8 (π‘Ÿ ∈ ℝ+ β†’ (π‘Ÿ / 2) ∈ ℝ+)
233 breq2 5151 . . . . . . . . . . 11 (𝑦 = (π‘Ÿ / 2) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦 ↔ ((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2)))
2342332ralbidv 3216 . . . . . . . . . 10 (𝑦 = (π‘Ÿ / 2) β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦 ↔ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2)))
235234rexbidv 3176 . . . . . . . . 9 (𝑦 = (π‘Ÿ / 2) β†’ (βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦 ↔ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2)))
236235rspccva 3610 . . . . . . . 8 ((βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦 ∧ (π‘Ÿ / 2) ∈ ℝ+) β†’ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2))
237231, 232, 236syl2an 594 . . . . . . 7 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ π‘Ÿ ∈ ℝ+) β†’ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2))
2389ffund 6720 . . . . . . . . . . . 12 (πœ‘ β†’ Fun 𝐹)
239238ad2antrr 722 . . . . . . . . . . 11 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ Fun 𝐹)
2407ad2antrr 722 . . . . . . . . . . . 12 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ 𝐽 ∈ Top)
241 imassrn 6069 . . . . . . . . . . . . . 14 (𝐹 β€œ (β„€β‰₯β€˜π‘š)) βŠ† ran 𝐹
242241, 13sstrid 3992 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐹 β€œ (β„€β‰₯β€˜π‘š)) βŠ† βˆͺ 𝐽)
243242ad2antrr 722 . . . . . . . . . . . 12 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (𝐹 β€œ (β„€β‰₯β€˜π‘š)) βŠ† βˆͺ 𝐽)
244 nnz 12583 . . . . . . . . . . . . . . 15 (π‘š ∈ β„• β†’ π‘š ∈ β„€)
245 fnfvelrn 7081 . . . . . . . . . . . . . . 15 ((β„€β‰₯ Fn β„€ ∧ π‘š ∈ β„€) β†’ (β„€β‰₯β€˜π‘š) ∈ ran β„€β‰₯)
24657, 244, 245sylancr 585 . . . . . . . . . . . . . 14 (π‘š ∈ β„• β†’ (β„€β‰₯β€˜π‘š) ∈ ran β„€β‰₯)
247246ad2antll 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (β„€β‰₯β€˜π‘š) ∈ ran β„€β‰₯)
248 simplr 765 . . . . . . . . . . . . 13 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
249 imaeq2 6054 . . . . . . . . . . . . . . . 16 (𝑒 = (β„€β‰₯β€˜π‘š) β†’ (𝐹 β€œ 𝑒) = (𝐹 β€œ (β„€β‰₯β€˜π‘š)))
250249fveq2d 6894 . . . . . . . . . . . . . . 15 (𝑒 = (β„€β‰₯β€˜π‘š) β†’ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) = ((clsβ€˜π½)β€˜(𝐹 β€œ (β„€β‰₯β€˜π‘š))))
251250eleq2d 2817 . . . . . . . . . . . . . 14 (𝑒 = (β„€β‰₯β€˜π‘š) β†’ (𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ 𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ (β„€β‰₯β€˜π‘š)))))
252251rspcv 3607 . . . . . . . . . . . . 13 ((β„€β‰₯β€˜π‘š) ∈ ran β„€β‰₯ β†’ (βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ (β„€β‰₯β€˜π‘š)))))
253247, 248, 252sylc 65 . . . . . . . . . . . 12 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ 𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ (β„€β‰₯β€˜π‘š))))
2544ad2antrr 722 . . . . . . . . . . . . 13 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
255220adantr 479 . . . . . . . . . . . . 13 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ 𝑦 ∈ 𝑋)
256232ad2antrl 724 . . . . . . . . . . . . . 14 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (π‘Ÿ / 2) ∈ ℝ+)
257256rpxrd 13021 . . . . . . . . . . . . 13 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (π‘Ÿ / 2) ∈ ℝ*)
2585blopn 24229 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋 ∧ (π‘Ÿ / 2) ∈ ℝ*) β†’ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∈ 𝐽)
259254, 255, 257, 258syl3anc 1369 . . . . . . . . . . . 12 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∈ 𝐽)
260 blcntr 24139 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋 ∧ (π‘Ÿ / 2) ∈ ℝ+) β†’ 𝑦 ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))
261254, 255, 256, 260syl3anc 1369 . . . . . . . . . . . 12 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ 𝑦 ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))
26215clsndisj 22799 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ (𝐹 β€œ (β„€β‰₯β€˜π‘š)) βŠ† βˆͺ 𝐽 ∧ 𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ (β„€β‰₯β€˜π‘š)))) ∧ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∈ 𝐽 ∧ 𝑦 ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))) β†’ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) β‰  βˆ…)
263240, 243, 253, 259, 261, 262syl32anc 1376 . . . . . . . . . . 11 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) β‰  βˆ…)
264 n0 4345 . . . . . . . . . . . 12 (((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) β‰  βˆ… ↔ βˆƒπ‘› 𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))))
265 inss2 4228 . . . . . . . . . . . . . . . . 17 ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) βŠ† (𝐹 β€œ (β„€β‰₯β€˜π‘š))
266265sseli 3977 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) β†’ 𝑛 ∈ (𝐹 β€œ (β„€β‰₯β€˜π‘š)))
267 fvelima 6956 . . . . . . . . . . . . . . . 16 ((Fun 𝐹 ∧ 𝑛 ∈ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) = 𝑛)
268266, 267sylan2 591 . . . . . . . . . . . . . . 15 ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š)))) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) = 𝑛)
269 inss1 4227 . . . . . . . . . . . . . . . . . . 19 ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) βŠ† (𝑦(ballβ€˜π·)(π‘Ÿ / 2))
270269sseli 3977 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) β†’ 𝑛 ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))
271270adantl 480 . . . . . . . . . . . . . . . . 17 ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š)))) β†’ 𝑛 ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))
272 eleq1a 2826 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)) β†’ ((πΉβ€˜π‘˜) = 𝑛 β†’ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))))
273271, 272syl 17 . . . . . . . . . . . . . . . 16 ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š)))) β†’ ((πΉβ€˜π‘˜) = 𝑛 β†’ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))))
274273reximdv 3168 . . . . . . . . . . . . . . 15 ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š)))) β†’ (βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) = 𝑛 β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))))
275268, 274mpd 15 . . . . . . . . . . . . . 14 ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š)))) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))
276275ex 411 . . . . . . . . . . . . 13 (Fun 𝐹 β†’ (𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))))
277276exlimdv 1934 . . . . . . . . . . . 12 (Fun 𝐹 β†’ (βˆƒπ‘› 𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))))
278264, 277biimtrid 241 . . . . . . . . . . 11 (Fun 𝐹 β†’ (((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) β‰  βˆ… β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))))
279239, 263, 278sylc 65 . . . . . . . . . 10 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))
280 r19.29 3112 . . . . . . . . . . 11 ((βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))))
281 uznnssnn 12883 . . . . . . . . . . . . . 14 (π‘š ∈ β„• β†’ (β„€β‰₯β€˜π‘š) βŠ† β„•)
282281ad2antll 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (β„€β‰₯β€˜π‘š) βŠ† β„•)
283 simprlr 776 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))
2844ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
285 simplrl 773 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ π‘Ÿ ∈ ℝ+)
286285, 232syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (π‘Ÿ / 2) ∈ ℝ+)
287286rpxrd 13021 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (π‘Ÿ / 2) ∈ ℝ*)
288 simpllr 772 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ 𝑦 ∈ 𝑋)
2899ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ 𝐹:β„•βŸΆπ‘‹)
290 eluznn 12906 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘š ∈ β„• ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘š)) β†’ π‘˜ ∈ β„•)
291290ad2ant2lr 744 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•) ∧ (π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))) β†’ π‘˜ ∈ β„•)
292291ad2ant2lr 744 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ π‘˜ ∈ β„•)
293289, 292ffvelcdmd 7086 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (πΉβ€˜π‘˜) ∈ 𝑋)
294 elbl3 24118 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ (π‘Ÿ / 2) ∈ ℝ*) ∧ (𝑦 ∈ 𝑋 ∧ (πΉβ€˜π‘˜) ∈ 𝑋)) β†’ ((πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ↔ ((πΉβ€˜π‘˜)𝐷𝑦) < (π‘Ÿ / 2)))
295284, 287, 288, 293, 294syl22anc 835 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ↔ ((πΉβ€˜π‘˜)𝐷𝑦) < (π‘Ÿ / 2)))
296283, 295mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((πΉβ€˜π‘˜)𝐷𝑦) < (π‘Ÿ / 2))
2972ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ 𝐷 ∈ (Metβ€˜π‘‹))
298 simprr 769 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))
299 eluznn 12906 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘˜ ∈ β„• ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜)) β†’ 𝑛 ∈ β„•)
300292, 298, 299syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ 𝑛 ∈ β„•)
301289, 300ffvelcdmd 7086 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (πΉβ€˜π‘›) ∈ 𝑋)
302 metcl 24058 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ (πΉβ€˜π‘›) ∈ 𝑋) β†’ ((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) ∈ ℝ)
303297, 293, 301, 302syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) ∈ ℝ)
304 metcl 24058 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ((πΉβ€˜π‘˜)𝐷𝑦) ∈ ℝ)
305297, 293, 288, 304syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((πΉβ€˜π‘˜)𝐷𝑦) ∈ ℝ)
306286rpred 13020 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (π‘Ÿ / 2) ∈ ℝ)
307 lt2add 11703 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) ∈ ℝ ∧ ((πΉβ€˜π‘˜)𝐷𝑦) ∈ ℝ) ∧ ((π‘Ÿ / 2) ∈ ℝ ∧ (π‘Ÿ / 2) ∈ ℝ)) β†’ ((((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ ((πΉβ€˜π‘˜)𝐷𝑦) < (π‘Ÿ / 2)) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < ((π‘Ÿ / 2) + (π‘Ÿ / 2))))
308303, 305, 306, 306, 307syl22anc 835 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ ((πΉβ€˜π‘˜)𝐷𝑦) < (π‘Ÿ / 2)) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < ((π‘Ÿ / 2) + (π‘Ÿ / 2))))
309296, 308mpan2d 690 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < ((π‘Ÿ / 2) + (π‘Ÿ / 2))))
310285rpcnd 13022 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ π‘Ÿ ∈ β„‚)
3113102halvesd 12462 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((π‘Ÿ / 2) + (π‘Ÿ / 2)) = π‘Ÿ)
312311breq2d 5159 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < ((π‘Ÿ / 2) + (π‘Ÿ / 2)) ↔ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < π‘Ÿ))
313309, 312sylibd 238 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < π‘Ÿ))
314 mettri2 24067 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ ((πΉβ€˜π‘˜) ∈ 𝑋 ∧ (πΉβ€˜π‘›) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ ((πΉβ€˜π‘›)𝐷𝑦) ≀ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)))
315297, 293, 301, 288, 314syl13anc 1370 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((πΉβ€˜π‘›)𝐷𝑦) ≀ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)))
316 metcl 24058 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ (πΉβ€˜π‘›) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ((πΉβ€˜π‘›)𝐷𝑦) ∈ ℝ)
317297, 301, 288, 316syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((πΉβ€˜π‘›)𝐷𝑦) ∈ ℝ)
318303, 305readdcld 11247 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) ∈ ℝ)
319285rpred 13020 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ π‘Ÿ ∈ ℝ)
320 lelttr 11308 . . . . . . . . . . . . . . . . . . . . . 22 ((((πΉβ€˜π‘›)𝐷𝑦) ∈ ℝ ∧ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) ∈ ℝ ∧ π‘Ÿ ∈ ℝ) β†’ ((((πΉβ€˜π‘›)𝐷𝑦) ≀ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) ∧ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < π‘Ÿ) β†’ ((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
321317, 318, 319, 320syl3anc 1369 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((((πΉβ€˜π‘›)𝐷𝑦) ≀ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) ∧ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < π‘Ÿ) β†’ ((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
322315, 321mpand 691 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < π‘Ÿ β†’ ((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
323313, 322syld 47 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ ((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
324323anassrs 466 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ (π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜)) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ ((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
325324ralimdva 3165 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ (π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))) β†’ (βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
326325expr 455 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘š)) β†’ ((πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)) β†’ (βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ)))
327326com23 86 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘š)) β†’ (βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ ((πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)) β†’ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ)))
328327impd 409 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘š)) β†’ ((βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) β†’ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
329328reximdva 3166 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
330 ssrexv 4050 . . . . . . . . . . . . 13 ((β„€β‰₯β€˜π‘š) βŠ† β„• β†’ (βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ β†’ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
331282, 329, 330sylsyld 61 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) β†’ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
332220, 331syldanl 600 . . . . . . . . . . 11 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) β†’ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
333280, 332syl5 34 . . . . . . . . . 10 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ ((βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) β†’ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
334279, 333mpan2d 690 . . . . . . . . 9 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
335334anassrs 466 . . . . . . . 8 ((((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ π‘Ÿ ∈ ℝ+) ∧ π‘š ∈ β„•) β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
336335rexlimdva 3153 . . . . . . 7 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ π‘Ÿ ∈ ℝ+) β†’ (βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
337237, 336mpd 15 . . . . . 6 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ π‘Ÿ ∈ ℝ+) β†’ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ)
338337ralrimiva 3144 . . . . 5 ((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ)
339 eqidd 2731 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) = (πΉβ€˜π‘›))
3405, 4, 129, 222, 339, 9lmmbrf 25010 . . . . . 6 (πœ‘ β†’ (𝐹(β‡π‘‘β€˜π½)𝑦 ↔ (𝑦 ∈ 𝑋 ∧ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ)))
341340adantr 479 . . . . 5 ((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ (𝐹(β‡π‘‘β€˜π½)𝑦 ↔ (𝑦 ∈ 𝑋 ∧ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ)))
342220, 338, 341mpbir2and 709 . . . 4 ((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ 𝐹(β‡π‘‘β€˜π½)𝑦)
343200, 342sylan2br 593 . . 3 ((πœ‘ ∧ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}) β†’ 𝐹(β‡π‘‘β€˜π½)𝑦)
344 releldm 5942 . . 3 ((Rel (β‡π‘‘β€˜π½) ∧ 𝐹(β‡π‘‘β€˜π½)𝑦) β†’ 𝐹 ∈ dom (β‡π‘‘β€˜π½))
345189, 343, 344sylancr 585 . 2 ((πœ‘ ∧ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}) β†’ 𝐹 ∈ dom (β‡π‘‘β€˜π½))
346188, 345exlimddv 1936 1 (πœ‘ β†’ 𝐹 ∈ dom (β‡π‘‘β€˜π½))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085  βˆ€wal 1537   = wceq 1539  βˆƒwex 1779   ∈ wcel 2104  {cab 2707   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068  Vcvv 3472   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  {csn 4627  βˆͺ cuni 4907  βˆ© cint 4949   class class class wbr 5147  dom cdm 5675  ran crn 5676   β€œ cima 5678  Rel wrel 5680  Fun wfun 6536   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411   ↑pm cpm 8823  Fincfn 8941  ficfi 9407  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115  β„*cxr 11251   < clt 11252   ≀ cle 11253   / cdiv 11875  β„•cn 12216  2c2 12271  β„€cz 12562  β„€β‰₯cuz 12826  β„+crp 12978  βˆžMetcxmet 21129  Metcmet 21130  ballcbl 21131  MetOpencmopn 21134  Topctop 22615  Clsdccld 22740  clsccl 22742  β‡π‘‘clm 22950  Compccmp 23110  Cauccau 25001
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-map 8824  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fi 9408  df-sup 9439  df-inf 9440  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-n0 12477  df-z 12563  df-uz 12827  df-q 12937  df-rp 12979  df-xneg 13096  df-xadd 13097  df-xmul 13098  df-topgen 17393  df-psmet 21136  df-xmet 21137  df-met 21138  df-bl 21139  df-mopn 21140  df-top 22616  df-topon 22633  df-bases 22669  df-cld 22743  df-ntr 22744  df-cls 22745  df-lm 22953  df-cmp 23111  df-cau 25004
This theorem is referenced by:  heibor1  36981
  Copyright terms: Public domain W3C validator