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 36677
Description: Lemma for heibor1 36678. 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 23840 . . . . . . . . . 10 (𝐷 ∈ (Metβ€˜π‘‹) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
42, 3syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
5 heibor.1 . . . . . . . . . 10 𝐽 = (MetOpenβ€˜π·)
65mopntop 23946 . . . . . . . . 9 (𝐷 ∈ (∞Metβ€˜π‘‹) β†’ 𝐽 ∈ Top)
74, 6syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐽 ∈ Top)
8 imassrn 6071 . . . . . . . . 9 (𝐹 β€œ 𝑒) βŠ† ran 𝐹
9 heibor1.6 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹:β„•βŸΆπ‘‹)
109frnd 6726 . . . . . . . . . 10 (πœ‘ β†’ ran 𝐹 βŠ† 𝑋)
115mopnuni 23947 . . . . . . . . . . 11 (𝐷 ∈ (∞Metβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
124, 11syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝑋 = βˆͺ 𝐽)
1310, 12sseqtrd 4023 . . . . . . . . 9 (πœ‘ β†’ ran 𝐹 βŠ† βˆͺ 𝐽)
148, 13sstrid 3994 . . . . . . . 8 (πœ‘ β†’ (𝐹 β€œ 𝑒) βŠ† βˆͺ 𝐽)
15 eqid 2733 . . . . . . . . 9 βˆͺ 𝐽 = βˆͺ 𝐽
1615clscld 22551 . . . . . . . 8 ((𝐽 ∈ Top ∧ (𝐹 β€œ 𝑒) βŠ† βˆͺ 𝐽) β†’ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∈ (Clsdβ€˜π½))
177, 14, 16syl2anc 585 . . . . . . 7 (πœ‘ β†’ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∈ (Clsdβ€˜π½))
18 eleq1a 2829 . . . . . . 7 (((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∈ (Clsdβ€˜π½) β†’ (π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ π‘˜ ∈ (Clsdβ€˜π½)))
1917, 18syl 17 . . . . . 6 (πœ‘ β†’ (π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ π‘˜ ∈ (Clsdβ€˜π½)))
2019rexlimdvw 3161 . . . . 5 (πœ‘ β†’ (βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ π‘˜ ∈ (Clsdβ€˜π½)))
2120abssdv 4066 . . . 4 (πœ‘ β†’ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} βŠ† (Clsdβ€˜π½))
22 fvex 6905 . . . . 5 (Clsdβ€˜π½) ∈ V
2322elpw2 5346 . . . 4 ({π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∈ 𝒫 (Clsdβ€˜π½) ↔ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} βŠ† (Clsdβ€˜π½))
2421, 23sylibr 233 . . 3 (πœ‘ β†’ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∈ 𝒫 (Clsdβ€˜π½))
25 elin 3965 . . . . . . 7 (π‘Ÿ ∈ (𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∩ Fin) ↔ (π‘Ÿ ∈ 𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∧ π‘Ÿ ∈ Fin))
26 velpw 4608 . . . . . . . . 9 (π‘Ÿ ∈ 𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ↔ π‘Ÿ βŠ† {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})
27 ssabral 4060 . . . . . . . . 9 (π‘Ÿ βŠ† {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ↔ βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
2826, 27bitri 275 . . . . . . . 8 (π‘Ÿ ∈ 𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ↔ βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
2928anbi1i 625 . . . . . . 7 ((π‘Ÿ ∈ 𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∧ π‘Ÿ ∈ Fin) ↔ (βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ π‘Ÿ ∈ Fin))
3025, 29bitri 275 . . . . . 6 (π‘Ÿ ∈ (𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∩ Fin) ↔ (βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ π‘Ÿ ∈ Fin))
31 raleq 3323 . . . . . . . . . . . . . 14 (π‘š = βˆ… β†’ (βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ βˆ€π‘˜ ∈ βˆ… βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
3231anbi2d 630 . . . . . . . . . . . . 13 (π‘š = βˆ… β†’ ((πœ‘ ∧ βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ↔ (πœ‘ ∧ βˆ€π‘˜ ∈ βˆ… βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))))
33 inteq 4954 . . . . . . . . . . . . . . 15 (π‘š = βˆ… β†’ ∩ π‘š = ∩ βˆ…)
3433sseq2d 4015 . . . . . . . . . . . . . 14 (π‘š = βˆ… β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ π‘š ↔ (𝐹 β€œ π‘˜) βŠ† ∩ βˆ…))
3534rexbidv 3179 . . . . . . . . . . . . 13 (π‘š = βˆ… β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘š ↔ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ βˆ…))
3632, 35imbi12d 345 . . . . . . . . . . . 12 (π‘š = βˆ… β†’ (((πœ‘ ∧ βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘š) ↔ ((πœ‘ ∧ βˆ€π‘˜ ∈ βˆ… βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ βˆ…)))
37 raleq 3323 . . . . . . . . . . . . . 14 (π‘š = 𝑦 β†’ (βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ βˆ€π‘˜ ∈ 𝑦 βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
3837anbi2d 630 . . . . . . . . . . . . 13 (π‘š = 𝑦 β†’ ((πœ‘ ∧ βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ↔ (πœ‘ ∧ βˆ€π‘˜ ∈ 𝑦 βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))))
39 inteq 4954 . . . . . . . . . . . . . . 15 (π‘š = 𝑦 β†’ ∩ π‘š = ∩ 𝑦)
4039sseq2d 4015 . . . . . . . . . . . . . 14 (π‘š = 𝑦 β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ π‘š ↔ (𝐹 β€œ π‘˜) βŠ† ∩ 𝑦))
4140rexbidv 3179 . . . . . . . . . . . . 13 (π‘š = 𝑦 β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘š ↔ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦))
4238, 41imbi12d 345 . . . . . . . . . . . 12 (π‘š = 𝑦 β†’ (((πœ‘ ∧ βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘š) ↔ ((πœ‘ ∧ βˆ€π‘˜ ∈ 𝑦 βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦)))
43 raleq 3323 . . . . . . . . . . . . . 14 (π‘š = (𝑦 βˆͺ {𝑛}) β†’ (βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
4443anbi2d 630 . . . . . . . . . . . . 13 (π‘š = (𝑦 βˆͺ {𝑛}) β†’ ((πœ‘ ∧ βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ↔ (πœ‘ ∧ βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))))
45 inteq 4954 . . . . . . . . . . . . . . 15 (π‘š = (𝑦 βˆͺ {𝑛}) β†’ ∩ π‘š = ∩ (𝑦 βˆͺ {𝑛}))
4645sseq2d 4015 . . . . . . . . . . . . . 14 (π‘š = (𝑦 βˆͺ {𝑛}) β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ π‘š ↔ (𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
4746rexbidv 3179 . . . . . . . . . . . . 13 (π‘š = (𝑦 βˆͺ {𝑛}) β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘š ↔ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
4844, 47imbi12d 345 . . . . . . . . . . . 12 (π‘š = (𝑦 βˆͺ {𝑛}) β†’ (((πœ‘ ∧ βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘š) ↔ ((πœ‘ ∧ βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛}))))
49 raleq 3323 . . . . . . . . . . . . . 14 (π‘š = π‘Ÿ β†’ (βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
5049anbi2d 630 . . . . . . . . . . . . 13 (π‘š = π‘Ÿ β†’ ((πœ‘ ∧ βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ↔ (πœ‘ ∧ βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))))
51 inteq 4954 . . . . . . . . . . . . . . 15 (π‘š = π‘Ÿ β†’ ∩ π‘š = ∩ π‘Ÿ)
5251sseq2d 4015 . . . . . . . . . . . . . 14 (π‘š = π‘Ÿ β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ π‘š ↔ (𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ))
5352rexbidv 3179 . . . . . . . . . . . . 13 (π‘š = π‘Ÿ β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘š ↔ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ))
5450, 53imbi12d 345 . . . . . . . . . . . 12 (π‘š = π‘Ÿ β†’ (((πœ‘ ∧ βˆ€π‘˜ ∈ π‘š βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘š) ↔ ((πœ‘ ∧ βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ)))
55 uzf 12825 . . . . . . . . . . . . . . . 16 β„€β‰₯:β„€βŸΆπ’« β„€
56 ffn 6718 . . . . . . . . . . . . . . . 16 (β„€β‰₯:β„€βŸΆπ’« β„€ β†’ β„€β‰₯ Fn β„€)
5755, 56ax-mp 5 . . . . . . . . . . . . . . 15 β„€β‰₯ Fn β„€
58 0z 12569 . . . . . . . . . . . . . . 15 0 ∈ β„€
59 fnfvelrn 7083 . . . . . . . . . . . . . . 15 ((β„€β‰₯ Fn β„€ ∧ 0 ∈ β„€) β†’ (β„€β‰₯β€˜0) ∈ ran β„€β‰₯)
6057, 58, 59mp2an 691 . . . . . . . . . . . . . 14 (β„€β‰₯β€˜0) ∈ ran β„€β‰₯
61 ssv 4007 . . . . . . . . . . . . . . 15 (𝐹 β€œ (β„€β‰₯β€˜0)) βŠ† V
62 int0 4967 . . . . . . . . . . . . . . 15 ∩ βˆ… = V
6361, 62sseqtrri 4020 . . . . . . . . . . . . . 14 (𝐹 β€œ (β„€β‰₯β€˜0)) βŠ† ∩ βˆ…
64 imaeq2 6056 . . . . . . . . . . . . . . . 16 (π‘˜ = (β„€β‰₯β€˜0) β†’ (𝐹 β€œ π‘˜) = (𝐹 β€œ (β„€β‰₯β€˜0)))
6564sseq1d 4014 . . . . . . . . . . . . . . 15 (π‘˜ = (β„€β‰₯β€˜0) β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ βˆ… ↔ (𝐹 β€œ (β„€β‰₯β€˜0)) βŠ† ∩ βˆ…))
6665rspcev 3613 . . . . . . . . . . . . . 14 (((β„€β‰₯β€˜0) ∈ ran β„€β‰₯ ∧ (𝐹 β€œ (β„€β‰₯β€˜0)) βŠ† ∩ βˆ…) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ βˆ…)
6760, 63, 66mp2an 691 . . . . . . . . . . . . 13 βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ βˆ…
6867a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ βˆ€π‘˜ ∈ βˆ… βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ βˆ…)
69 ssun1 4173 . . . . . . . . . . . . . . . . 17 𝑦 βŠ† (𝑦 βˆͺ {𝑛})
70 ssralv 4051 . . . . . . . . . . . . . . . . 17 (𝑦 βŠ† (𝑦 βˆͺ {𝑛}) β†’ (βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ βˆ€π‘˜ ∈ 𝑦 βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
7169, 70ax-mp 5 . . . . . . . . . . . . . . . 16 (βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ βˆ€π‘˜ ∈ 𝑦 βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
7271anim2i 618 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ (πœ‘ ∧ βˆ€π‘˜ ∈ 𝑦 βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
7372imim1i 63 . . . . . . . . . . . . . 14 (((πœ‘ ∧ βˆ€π‘˜ ∈ 𝑦 βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦) β†’ ((πœ‘ ∧ βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦))
74 ssun2 4174 . . . . . . . . . . . . . . . . . 18 {𝑛} βŠ† (𝑦 βˆͺ {𝑛})
75 ssralv 4051 . . . . . . . . . . . . . . . . . 18 ({𝑛} βŠ† (𝑦 βˆͺ {𝑛}) β†’ (βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ βˆ€π‘˜ ∈ {𝑛}βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
7674, 75ax-mp 5 . . . . . . . . . . . . . . . . 17 (βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ βˆ€π‘˜ ∈ {𝑛}βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
77 vex 3479 . . . . . . . . . . . . . . . . . 18 𝑛 ∈ V
78 eqeq1 2737 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = 𝑛 β†’ (π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ 𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
7978rexbidv 3179 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑛 β†’ (βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ βˆƒπ‘’ ∈ ran β„€β‰₯𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
8077, 79ralsn 4686 . . . . . . . . . . . . . . . . 17 (βˆ€π‘˜ ∈ {𝑛}βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ βˆƒπ‘’ ∈ ran β„€β‰₯𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
8176, 80sylib 217 . . . . . . . . . . . . . . . 16 (βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ βˆƒπ‘’ ∈ ran β„€β‰₯𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
82 uzin2 15291 . . . . . . . . . . . . . . . . . . . 20 ((𝑒 ∈ ran β„€β‰₯ ∧ π‘˜ ∈ ran β„€β‰₯) β†’ (𝑒 ∩ π‘˜) ∈ ran β„€β‰₯)
838, 10sstrid 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (𝐹 β€œ 𝑒) βŠ† 𝑋)
8483, 12sseqtrd 4023 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝐹 β€œ 𝑒) βŠ† βˆͺ 𝐽)
8515sscls 22560 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 ∈ Top ∧ (𝐹 β€œ 𝑒) βŠ† βˆͺ 𝐽) β†’ (𝐹 β€œ 𝑒) βŠ† ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
867, 84, 85syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (𝐹 β€œ 𝑒) βŠ† ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
87 sseq2 4009 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ ((𝐹 β€œ 𝑒) βŠ† 𝑛 ↔ (𝐹 β€œ 𝑒) βŠ† ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
8886, 87syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ (𝐹 β€œ 𝑒) βŠ† 𝑛))
89 inss2 4230 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑒 ∩ π‘˜) βŠ† π‘˜
90 inss1 4229 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑒 ∩ π‘˜) βŠ† 𝑒
91 imass2 6102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑒 ∩ π‘˜) βŠ† π‘˜ β†’ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† (𝐹 β€œ π‘˜))
92 imass2 6102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑒 ∩ π‘˜) βŠ† 𝑒 β†’ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† (𝐹 β€œ 𝑒))
9391, 92anim12i 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑒 ∩ π‘˜) βŠ† π‘˜ ∧ (𝑒 ∩ π‘˜) βŠ† 𝑒) β†’ ((𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† (𝐹 β€œ π‘˜) ∧ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† (𝐹 β€œ 𝑒)))
94 ssin 4231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† (𝐹 β€œ π‘˜) ∧ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† (𝐹 β€œ 𝑒)) ↔ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ((𝐹 β€œ π‘˜) ∩ (𝐹 β€œ 𝑒)))
9593, 94sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑒 ∩ π‘˜) βŠ† π‘˜ ∧ (𝑒 ∩ π‘˜) βŠ† 𝑒) β†’ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ((𝐹 β€œ π‘˜) ∩ (𝐹 β€œ 𝑒)))
9689, 90, 95mp2an 691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ((𝐹 β€œ π‘˜) ∩ (𝐹 β€œ 𝑒))
97 ss2in 4237 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐹 β€œ π‘˜) βŠ† ∩ 𝑦 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑛) β†’ ((𝐹 β€œ π‘˜) ∩ (𝐹 β€œ 𝑒)) βŠ† (∩ 𝑦 ∩ 𝑛))
9896, 97sstrid 3994 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹 β€œ π‘˜) βŠ† ∩ 𝑦 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑛) β†’ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† (∩ 𝑦 ∩ 𝑛))
9977intunsn 4994 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ∩ (𝑦 βˆͺ {𝑛}) = (∩ 𝑦 ∩ 𝑛)
10098, 99sseqtrrdi 4034 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹 β€œ π‘˜) βŠ† ∩ 𝑦 ∧ (𝐹 β€œ 𝑒) βŠ† 𝑛) β†’ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ∩ (𝑦 βˆͺ {𝑛}))
101100expcom 415 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 β€œ 𝑒) βŠ† 𝑛 β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ 𝑦 β†’ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
10288, 101syl6 35 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ 𝑦 β†’ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ∩ (𝑦 βˆͺ {𝑛}))))
103102impd 412 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ (𝐹 β€œ π‘˜) βŠ† ∩ 𝑦) β†’ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
104 imaeq2 6056 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘š = (𝑒 ∩ π‘˜) β†’ (𝐹 β€œ π‘š) = (𝐹 β€œ (𝑒 ∩ π‘˜)))
105104sseq1d 4014 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘š = (𝑒 ∩ π‘˜) β†’ ((𝐹 β€œ π‘š) βŠ† ∩ (𝑦 βˆͺ {𝑛}) ↔ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
106105rspcev 3613 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑒 ∩ π‘˜) ∈ ran β„€β‰₯ ∧ (𝐹 β€œ (𝑒 ∩ π‘˜)) βŠ† ∩ (𝑦 βˆͺ {𝑛})) β†’ βˆƒπ‘š ∈ ran β„€β‰₯(𝐹 β€œ π‘š) βŠ† ∩ (𝑦 βˆͺ {𝑛}))
107106expcom 415 . . . . . . . . . . . . . . . . . . . . . 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 3211 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (βˆƒπ‘’ ∈ ran β„€β‰₯βˆƒπ‘˜ ∈ ran β„€β‰₯(𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ (𝐹 β€œ π‘˜) βŠ† ∩ 𝑦) β†’ βˆƒπ‘š ∈ ran β„€β‰₯(𝐹 β€œ π‘š) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
112 reeanv 3227 . . . . . . . . . . . . . . . . . 18 (βˆƒπ‘’ ∈ ran β„€β‰₯βˆƒπ‘˜ ∈ ran β„€β‰₯(𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ (𝐹 β€œ π‘˜) βŠ† ∩ 𝑦) ↔ (βˆƒπ‘’ ∈ ran β„€β‰₯𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦))
113 imaeq2 6056 . . . . . . . . . . . . . . . . . . . 20 (π‘š = π‘˜ β†’ (𝐹 β€œ π‘š) = (𝐹 β€œ π‘˜))
114113sseq1d 4014 . . . . . . . . . . . . . . . . . . 19 (π‘š = π‘˜ β†’ ((𝐹 β€œ π‘š) βŠ† ∩ (𝑦 βˆͺ {𝑛}) ↔ (𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
115114cbvrexvw 3236 . . . . . . . . . . . . . . . . . 18 (βˆƒπ‘š ∈ ran β„€β‰₯(𝐹 β€œ π‘š) βŠ† ∩ (𝑦 βˆͺ {𝑛}) ↔ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛}))
116111, 112, 1153imtr3g 295 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((βˆƒπ‘’ ∈ ran β„€β‰₯𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛})))
117116expd 417 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βˆƒπ‘’ ∈ ran β„€β‰₯𝑛 = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦 β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛}))))
11881, 117syl5 34 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (βˆ€π‘˜ ∈ (𝑦 βˆͺ {𝑛})βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ 𝑦 β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ (𝑦 βˆͺ {𝑛}))))
119118imp 408 . . . . . . . . . . . . . 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 9164 . . . . . . . . . . 11 (π‘Ÿ ∈ Fin β†’ ((πœ‘ ∧ βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ))
123122com12 32 . . . . . . . . . 10 ((πœ‘ ∧ βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ (π‘Ÿ ∈ Fin β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ))
124123impr 456 . . . . . . . . 9 ((πœ‘ ∧ (βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ π‘Ÿ ∈ Fin)) β†’ βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ)
1259ffnd 6719 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹 Fn β„•)
126 inss1 4229 . . . . . . . . . . . . . . 15 (π‘˜ ∩ β„•) βŠ† π‘˜
127 imass2 6102 . . . . . . . . . . . . . . 15 ((π‘˜ ∩ β„•) βŠ† π‘˜ β†’ (𝐹 β€œ (π‘˜ ∩ β„•)) βŠ† (𝐹 β€œ π‘˜))
128126, 127ax-mp 5 . . . . . . . . . . . . . 14 (𝐹 β€œ (π‘˜ ∩ β„•)) βŠ† (𝐹 β€œ π‘˜)
129 nnuz 12865 . . . . . . . . . . . . . . . . . . . 20 β„• = (β„€β‰₯β€˜1)
130 1z 12592 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ β„€
131 fnfvelrn 7083 . . . . . . . . . . . . . . . . . . . . 21 ((β„€β‰₯ Fn β„€ ∧ 1 ∈ β„€) β†’ (β„€β‰₯β€˜1) ∈ ran β„€β‰₯)
13257, 130, 131mp2an 691 . . . . . . . . . . . . . . . . . . . 20 (β„€β‰₯β€˜1) ∈ ran β„€β‰₯
133129, 132eqeltri 2830 . . . . . . . . . . . . . . . . . . 19 β„• ∈ ran β„€β‰₯
134 uzin2 15291 . . . . . . . . . . . . . . . . . . 19 ((π‘˜ ∈ ran β„€β‰₯ ∧ β„• ∈ ran β„€β‰₯) β†’ (π‘˜ ∩ β„•) ∈ ran β„€β‰₯)
135133, 134mpan2 690 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ ran β„€β‰₯ β†’ (π‘˜ ∩ β„•) ∈ ran β„€β‰₯)
136 uzn0 12839 . . . . . . . . . . . . . . . . . 18 ((π‘˜ ∩ β„•) ∈ ran β„€β‰₯ β†’ (π‘˜ ∩ β„•) β‰  βˆ…)
137135, 136syl 17 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ ran β„€β‰₯ β†’ (π‘˜ ∩ β„•) β‰  βˆ…)
138 n0 4347 . . . . . . . . . . . . . . . . 17 ((π‘˜ ∩ β„•) β‰  βˆ… ↔ βˆƒπ‘¦ 𝑦 ∈ (π‘˜ ∩ β„•))
139137, 138sylib 217 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ ran β„€β‰₯ β†’ βˆƒπ‘¦ 𝑦 ∈ (π‘˜ ∩ β„•))
140 fnfun 6650 . . . . . . . . . . . . . . . . . . 19 (𝐹 Fn β„• β†’ Fun 𝐹)
141 inss2 4230 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ ∩ β„•) βŠ† β„•
142 fndm 6653 . . . . . . . . . . . . . . . . . . . 20 (𝐹 Fn β„• β†’ dom 𝐹 = β„•)
143141, 142sseqtrrid 4036 . . . . . . . . . . . . . . . . . . 19 (𝐹 Fn β„• β†’ (π‘˜ ∩ β„•) βŠ† dom 𝐹)
144 funfvima2 7233 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹 ∧ (π‘˜ ∩ β„•) βŠ† dom 𝐹) β†’ (𝑦 ∈ (π‘˜ ∩ β„•) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ (π‘˜ ∩ β„•))))
145140, 143, 144syl2anc 585 . . . . . . . . . . . . . . . . . 18 (𝐹 Fn β„• β†’ (𝑦 ∈ (π‘˜ ∩ β„•) β†’ (πΉβ€˜π‘¦) ∈ (𝐹 β€œ (π‘˜ ∩ β„•))))
146 ne0i 4335 . . . . . . . . . . . . . . . . . 18 ((πΉβ€˜π‘¦) ∈ (𝐹 β€œ (π‘˜ ∩ β„•)) β†’ (𝐹 β€œ (π‘˜ ∩ β„•)) β‰  βˆ…)
147145, 146syl6 35 . . . . . . . . . . . . . . . . 17 (𝐹 Fn β„• β†’ (𝑦 ∈ (π‘˜ ∩ β„•) β†’ (𝐹 β€œ (π‘˜ ∩ β„•)) β‰  βˆ…))
148147exlimdv 1937 . . . . . . . . . . . . . . . 16 (𝐹 Fn β„• β†’ (βˆƒπ‘¦ 𝑦 ∈ (π‘˜ ∩ β„•) β†’ (𝐹 β€œ (π‘˜ ∩ β„•)) β‰  βˆ…))
149139, 148syl5 34 . . . . . . . . . . . . . . 15 (𝐹 Fn β„• β†’ (π‘˜ ∈ ran β„€β‰₯ β†’ (𝐹 β€œ (π‘˜ ∩ β„•)) β‰  βˆ…))
150149imp 408 . . . . . . . . . . . . . 14 ((𝐹 Fn β„• ∧ π‘˜ ∈ ran β„€β‰₯) β†’ (𝐹 β€œ (π‘˜ ∩ β„•)) β‰  βˆ…)
151 ssn0 4401 . . . . . . . . . . . . . 14 (((𝐹 β€œ (π‘˜ ∩ β„•)) βŠ† (𝐹 β€œ π‘˜) ∧ (𝐹 β€œ (π‘˜ ∩ β„•)) β‰  βˆ…) β†’ (𝐹 β€œ π‘˜) β‰  βˆ…)
152128, 150, 151sylancr 588 . . . . . . . . . . . . 13 ((𝐹 Fn β„• ∧ π‘˜ ∈ ran β„€β‰₯) β†’ (𝐹 β€œ π‘˜) β‰  βˆ…)
153 ssn0 4401 . . . . . . . . . . . . . 14 (((𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ ∧ (𝐹 β€œ π‘˜) β‰  βˆ…) β†’ ∩ π‘Ÿ β‰  βˆ…)
154153expcom 415 . . . . . . . . . . . . 13 ((𝐹 β€œ π‘˜) β‰  βˆ… β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ β†’ ∩ π‘Ÿ β‰  βˆ…))
155152, 154syl 17 . . . . . . . . . . . 12 ((𝐹 Fn β„• ∧ π‘˜ ∈ ran β„€β‰₯) β†’ ((𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ β†’ ∩ π‘Ÿ β‰  βˆ…))
156155rexlimdva 3156 . . . . . . . . . . 11 (𝐹 Fn β„• β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ β†’ ∩ π‘Ÿ β‰  βˆ…))
157125, 156syl 17 . . . . . . . . . 10 (πœ‘ β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ β†’ ∩ π‘Ÿ β‰  βˆ…))
158157adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ π‘Ÿ ∈ Fin)) β†’ (βˆƒπ‘˜ ∈ ran β„€β‰₯(𝐹 β€œ π‘˜) βŠ† ∩ π‘Ÿ β†’ ∩ π‘Ÿ β‰  βˆ…))
159124, 158mpd 15 . . . . . . . 8 ((πœ‘ ∧ (βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ π‘Ÿ ∈ Fin)) β†’ ∩ π‘Ÿ β‰  βˆ…)
160159necomd 2997 . . . . . . 7 ((πœ‘ ∧ (βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ π‘Ÿ ∈ Fin)) β†’ βˆ… β‰  ∩ π‘Ÿ)
161160neneqd 2946 . . . . . 6 ((πœ‘ ∧ (βˆ€π‘˜ ∈ π‘Ÿ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∧ π‘Ÿ ∈ Fin)) β†’ Β¬ βˆ… = ∩ π‘Ÿ)
16230, 161sylan2b 595 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ (𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∩ Fin)) β†’ Β¬ βˆ… = ∩ π‘Ÿ)
163162nrexdv 3150 . . . 4 (πœ‘ β†’ Β¬ βˆƒπ‘Ÿ ∈ (𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∩ Fin)βˆ… = ∩ π‘Ÿ)
164 0ex 5308 . . . . 5 βˆ… ∈ V
165 zex 12567 . . . . . . . 8 β„€ ∈ V
166165pwex 5379 . . . . . . 7 𝒫 β„€ ∈ V
167 frn 6725 . . . . . . . 8 (β„€β‰₯:β„€βŸΆπ’« β„€ β†’ ran β„€β‰₯ βŠ† 𝒫 β„€)
16855, 167ax-mp 5 . . . . . . 7 ran β„€β‰₯ βŠ† 𝒫 β„€
169166, 168ssexi 5323 . . . . . 6 ran β„€β‰₯ ∈ V
170169abrexex 7949 . . . . 5 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∈ V
171 elfi 9408 . . . . 5 ((βˆ… ∈ V ∧ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∈ V) β†’ (βˆ… ∈ (fiβ€˜{π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}) ↔ βˆƒπ‘Ÿ ∈ (𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∩ Fin)βˆ… = ∩ π‘Ÿ))
172164, 170, 171mp2an 691 . . . 4 (βˆ… ∈ (fiβ€˜{π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}) ↔ βˆƒπ‘Ÿ ∈ (𝒫 {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ∩ Fin)βˆ… = ∩ π‘Ÿ)
173163, 172sylnibr 329 . . 3 (πœ‘ β†’ Β¬ βˆ… ∈ (fiβ€˜{π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}))
174 cmptop 22899 . . . . . 6 (𝐽 ∈ Comp β†’ 𝐽 ∈ Top)
175 cmpfi 22912 . . . . . 6 (𝐽 ∈ Top β†’ (𝐽 ∈ Comp ↔ βˆ€π‘š ∈ 𝒫 (Clsdβ€˜π½)(Β¬ βˆ… ∈ (fiβ€˜π‘š) β†’ ∩ π‘š β‰  βˆ…)))
176174, 175syl 17 . . . . 5 (𝐽 ∈ Comp β†’ (𝐽 ∈ Comp ↔ βˆ€π‘š ∈ 𝒫 (Clsdβ€˜π½)(Β¬ βˆ… ∈ (fiβ€˜π‘š) β†’ ∩ π‘š β‰  βˆ…)))
177176ibi 267 . . . 4 (𝐽 ∈ Comp β†’ βˆ€π‘š ∈ 𝒫 (Clsdβ€˜π½)(Β¬ βˆ… ∈ (fiβ€˜π‘š) β†’ ∩ π‘š β‰  βˆ…))
178 fveq2 6892 . . . . . . . 8 (π‘š = {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β†’ (fiβ€˜π‘š) = (fiβ€˜{π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}))
179178eleq2d 2820 . . . . . . 7 (π‘š = {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β†’ (βˆ… ∈ (fiβ€˜π‘š) ↔ βˆ… ∈ (fiβ€˜{π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})))
180179notbid 318 . . . . . 6 (π‘š = {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β†’ (Β¬ βˆ… ∈ (fiβ€˜π‘š) ↔ Β¬ βˆ… ∈ (fiβ€˜{π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})))
181 inteq 4954 . . . . . . . 8 (π‘š = {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β†’ ∩ π‘š = ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})
182181neeq1d 3001 . . . . . . 7 (π‘š = {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β†’ (∩ π‘š β‰  βˆ… ↔ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β‰  βˆ…))
183 n0 4347 . . . . . . 7 (∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β‰  βˆ… ↔ βˆƒπ‘¦ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})
184182, 183bitrdi 287 . . . . . 6 (π‘š = {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β†’ (∩ π‘š β‰  βˆ… ↔ βˆƒπ‘¦ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}))
185180, 184imbi12d 345 . . . . 5 (π‘š = {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β†’ ((Β¬ βˆ… ∈ (fiβ€˜π‘š) β†’ ∩ π‘š β‰  βˆ…) ↔ (Β¬ βˆ… ∈ (fiβ€˜{π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}) β†’ βˆƒπ‘¦ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})))
186185rspccv 3610 . . . 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 22734 . . 3 Rel (β‡π‘‘β€˜π½)
190 r19.23v 3183 . . . . . 6 (βˆ€π‘’ ∈ ran β„€β‰₯(π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜) ↔ (βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜))
191190albii 1822 . . . . 5 (βˆ€π‘˜βˆ€π‘’ ∈ ran β„€β‰₯(π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜) ↔ βˆ€π‘˜(βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜))
192 fvex 6905 . . . . . . . 8 ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ∈ V
193 eleq2 2823 . . . . . . . 8 (π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ (𝑦 ∈ π‘˜ ↔ 𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
194192, 193ceqsalv 3512 . . . . . . 7 (βˆ€π‘˜(π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜) ↔ 𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
195194ralbii 3094 . . . . . 6 (βˆ€π‘’ ∈ ran β„€β‰₯βˆ€π‘˜(π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜) ↔ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
196 ralcom4 3284 . . . . . 6 (βˆ€π‘’ ∈ ran β„€β‰₯βˆ€π‘˜(π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜) ↔ βˆ€π‘˜βˆ€π‘’ ∈ ran β„€β‰₯(π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜))
197195, 196bitr3i 277 . . . . 5 (βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ βˆ€π‘˜βˆ€π‘’ ∈ ran β„€β‰₯(π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜))
198 vex 3479 . . . . . 6 𝑦 ∈ V
199198elintab 4963 . . . . 5 (𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ↔ βˆ€π‘˜(βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ π‘˜))
200191, 197, 1993bitr4i 303 . . . 4 (βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))})
201 eqid 2733 . . . . . . . . . . 11 ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) = ((clsβ€˜π½)β€˜(𝐹 β€œ β„•))
202 imaeq2 6056 . . . . . . . . . . . . 13 (𝑒 = β„• β†’ (𝐹 β€œ 𝑒) = (𝐹 β€œ β„•))
203202fveq2d 6896 . . . . . . . . . . . 12 (𝑒 = β„• β†’ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) = ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)))
204203rspceeqv 3634 . . . . . . . . . . 11 ((β„• ∈ ran β„€β‰₯ ∧ ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) = ((clsβ€˜π½)β€˜(𝐹 β€œ β„•))) β†’ βˆƒπ‘’ ∈ ran β„€β‰₯((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
205133, 201, 204mp2an 691 . . . . . . . . . 10 βˆƒπ‘’ ∈ ran β„€β‰₯((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))
206 fvex 6905 . . . . . . . . . . 11 ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) ∈ V
207 eqeq1 2737 . . . . . . . . . . . 12 (π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) β†’ (π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
208207rexbidv 3179 . . . . . . . . . . 11 (π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) β†’ (βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ βˆƒπ‘’ ∈ ran β„€β‰₯((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))))
209206, 208elab 3669 . . . . . . . . . 10 (((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) ∈ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} ↔ βˆƒπ‘’ ∈ ran β„€β‰₯((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
210205, 209mpbir 230 . . . . . . . . 9 ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) ∈ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}
211 intss1 4968 . . . . . . . . 9 (((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) ∈ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} β†’ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} βŠ† ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)))
212210, 211ax-mp 5 . . . . . . . 8 ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} βŠ† ((clsβ€˜π½)β€˜(𝐹 β€œ β„•))
213 imassrn 6071 . . . . . . . . . . 11 (𝐹 β€œ β„•) βŠ† ran 𝐹
214213, 13sstrid 3994 . . . . . . . . . 10 (πœ‘ β†’ (𝐹 β€œ β„•) βŠ† βˆͺ 𝐽)
21515clsss3 22563 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ (𝐹 β€œ β„•) βŠ† βˆͺ 𝐽) β†’ ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) βŠ† βˆͺ 𝐽)
2167, 214, 215syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) βŠ† βˆͺ 𝐽)
217216, 12sseqtrrd 4024 . . . . . . . 8 (πœ‘ β†’ ((clsβ€˜π½)β€˜(𝐹 β€œ β„•)) βŠ† 𝑋)
218212, 217sstrid 3994 . . . . . . 7 (πœ‘ β†’ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))} βŠ† 𝑋)
219218sselda 3983 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}) β†’ 𝑦 ∈ 𝑋)
220200, 219sylan2b 595 . . . . 5 ((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ 𝑦 ∈ 𝑋)
221 heibor1.5 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹 ∈ (Cauβ€˜π·))
222 1zzd 12593 . . . . . . . . . . . . 13 (πœ‘ β†’ 1 ∈ β„€)
223129, 4, 222iscau3 24795 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐹 ∈ (Cauβ€˜π·) ↔ (𝐹 ∈ (𝑋 ↑pm β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)(π‘˜ ∈ dom 𝐹 ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦))))
224221, 223mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ (𝐹 ∈ (𝑋 ↑pm β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)(π‘˜ ∈ dom 𝐹 ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦)))
225224simprd 497 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)(π‘˜ ∈ dom 𝐹 ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦))
226 simp3 1139 . . . . . . . . . . . . 13 ((π‘˜ ∈ dom 𝐹 ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦) β†’ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦)
227226ralimi 3084 . . . . . . . . . . . 12 (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)(π‘˜ ∈ dom 𝐹 ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦) β†’ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦)
228227reximi 3085 . . . . . . . . . . 11 (βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)(π‘˜ ∈ dom 𝐹 ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦) β†’ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦)
229228ralimi 3084 . . . . . . . . . 10 (βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)(π‘˜ ∈ dom 𝐹 ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦) β†’ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦)
230225, 229syl 17 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦)
231230adantr 482 . . . . . . . 8 ((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦)
232 rphalfcl 13001 . . . . . . . 8 (π‘Ÿ ∈ ℝ+ β†’ (π‘Ÿ / 2) ∈ ℝ+)
233 breq2 5153 . . . . . . . . . . 11 (𝑦 = (π‘Ÿ / 2) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦 ↔ ((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2)))
2342332ralbidv 3219 . . . . . . . . . 10 (𝑦 = (π‘Ÿ / 2) β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦 ↔ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2)))
235234rexbidv 3179 . . . . . . . . 9 (𝑦 = (π‘Ÿ / 2) β†’ (βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦 ↔ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2)))
236235rspccva 3612 . . . . . . . 8 ((βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < 𝑦 ∧ (π‘Ÿ / 2) ∈ ℝ+) β†’ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2))
237231, 232, 236syl2an 597 . . . . . . 7 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ π‘Ÿ ∈ ℝ+) β†’ βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2))
2389ffund 6722 . . . . . . . . . . . 12 (πœ‘ β†’ Fun 𝐹)
239238ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ Fun 𝐹)
2407ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ 𝐽 ∈ Top)
241 imassrn 6071 . . . . . . . . . . . . . 14 (𝐹 β€œ (β„€β‰₯β€˜π‘š)) βŠ† ran 𝐹
242241, 13sstrid 3994 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐹 β€œ (β„€β‰₯β€˜π‘š)) βŠ† βˆͺ 𝐽)
243242ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (𝐹 β€œ (β„€β‰₯β€˜π‘š)) βŠ† βˆͺ 𝐽)
244 nnz 12579 . . . . . . . . . . . . . . 15 (π‘š ∈ β„• β†’ π‘š ∈ β„€)
245 fnfvelrn 7083 . . . . . . . . . . . . . . 15 ((β„€β‰₯ Fn β„€ ∧ π‘š ∈ β„€) β†’ (β„€β‰₯β€˜π‘š) ∈ ran β„€β‰₯)
24657, 244, 245sylancr 588 . . . . . . . . . . . . . 14 (π‘š ∈ β„• β†’ (β„€β‰₯β€˜π‘š) ∈ ran β„€β‰₯)
247246ad2antll 728 . . . . . . . . . . . . 13 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (β„€β‰₯β€˜π‘š) ∈ ran β„€β‰₯)
248 simplr 768 . . . . . . . . . . . . 13 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)))
249 imaeq2 6056 . . . . . . . . . . . . . . . 16 (𝑒 = (β„€β‰₯β€˜π‘š) β†’ (𝐹 β€œ 𝑒) = (𝐹 β€œ (β„€β‰₯β€˜π‘š)))
250249fveq2d 6896 . . . . . . . . . . . . . . 15 (𝑒 = (β„€β‰₯β€˜π‘š) β†’ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) = ((clsβ€˜π½)β€˜(𝐹 β€œ (β„€β‰₯β€˜π‘š))))
251250eleq2d 2820 . . . . . . . . . . . . . 14 (𝑒 = (β„€β‰₯β€˜π‘š) β†’ (𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) ↔ 𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ (β„€β‰₯β€˜π‘š)))))
252251rspcv 3609 . . . . . . . . . . . . 13 ((β„€β‰₯β€˜π‘š) ∈ ran β„€β‰₯ β†’ (βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒)) β†’ 𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ (β„€β‰₯β€˜π‘š)))))
253247, 248, 252sylc 65 . . . . . . . . . . . 12 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ 𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ (β„€β‰₯β€˜π‘š))))
2544ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
255220adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ 𝑦 ∈ 𝑋)
256232ad2antrl 727 . . . . . . . . . . . . . 14 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (π‘Ÿ / 2) ∈ ℝ+)
257256rpxrd 13017 . . . . . . . . . . . . 13 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (π‘Ÿ / 2) ∈ ℝ*)
2585blopn 24009 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋 ∧ (π‘Ÿ / 2) ∈ ℝ*) β†’ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∈ 𝐽)
259254, 255, 257, 258syl3anc 1372 . . . . . . . . . . . 12 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∈ 𝐽)
260 blcntr 23919 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋 ∧ (π‘Ÿ / 2) ∈ ℝ+) β†’ 𝑦 ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))
261254, 255, 256, 260syl3anc 1372 . . . . . . . . . . . 12 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ 𝑦 ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))
26215clsndisj 22579 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ (𝐹 β€œ (β„€β‰₯β€˜π‘š)) βŠ† βˆͺ 𝐽 ∧ 𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ (β„€β‰₯β€˜π‘š)))) ∧ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∈ 𝐽 ∧ 𝑦 ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))) β†’ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) β‰  βˆ…)
263240, 243, 253, 259, 261, 262syl32anc 1379 . . . . . . . . . . 11 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) β‰  βˆ…)
264 n0 4347 . . . . . . . . . . . 12 (((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) β‰  βˆ… ↔ βˆƒπ‘› 𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))))
265 inss2 4230 . . . . . . . . . . . . . . . . 17 ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) βŠ† (𝐹 β€œ (β„€β‰₯β€˜π‘š))
266265sseli 3979 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) β†’ 𝑛 ∈ (𝐹 β€œ (β„€β‰₯β€˜π‘š)))
267 fvelima 6958 . . . . . . . . . . . . . . . 16 ((Fun 𝐹 ∧ 𝑛 ∈ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) = 𝑛)
268266, 267sylan2 594 . . . . . . . . . . . . . . 15 ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š)))) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) = 𝑛)
269 inss1 4229 . . . . . . . . . . . . . . . . . . 19 ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) βŠ† (𝑦(ballβ€˜π·)(π‘Ÿ / 2))
270269sseli 3979 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) β†’ 𝑛 ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))
271270adantl 483 . . . . . . . . . . . . . . . . 17 ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š)))) β†’ 𝑛 ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))
272 eleq1a 2829 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)) β†’ ((πΉβ€˜π‘˜) = 𝑛 β†’ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))))
273271, 272syl 17 . . . . . . . . . . . . . . . 16 ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š)))) β†’ ((πΉβ€˜π‘˜) = 𝑛 β†’ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))))
274273reximdv 3171 . . . . . . . . . . . . . . 15 ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š)))) β†’ (βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) = 𝑛 β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))))
275268, 274mpd 15 . . . . . . . . . . . . . 14 ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š)))) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))
276275ex 414 . . . . . . . . . . . . 13 (Fun 𝐹 β†’ (𝑛 ∈ ((𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ∩ (𝐹 β€œ (β„€β‰₯β€˜π‘š))) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))))
277276exlimdv 1937 . . . . . . . . . . . 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 3115 . . . . . . . . . . 11 ((βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))))
281 uznnssnn 12879 . . . . . . . . . . . . . 14 (π‘š ∈ β„• β†’ (β„€β‰₯β€˜π‘š) βŠ† β„•)
282281ad2antll 728 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (β„€β‰₯β€˜π‘š) βŠ† β„•)
283 simprlr 779 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))
2844ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ 𝐷 ∈ (∞Metβ€˜π‘‹))
285 simplrl 776 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ π‘Ÿ ∈ ℝ+)
286285, 232syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (π‘Ÿ / 2) ∈ ℝ+)
287286rpxrd 13017 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (π‘Ÿ / 2) ∈ ℝ*)
288 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ 𝑦 ∈ 𝑋)
2899ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ 𝐹:β„•βŸΆπ‘‹)
290 eluznn 12902 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘š ∈ β„• ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘š)) β†’ π‘˜ ∈ β„•)
291290ad2ant2lr 747 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•) ∧ (π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))) β†’ π‘˜ ∈ β„•)
292291ad2ant2lr 747 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ π‘˜ ∈ β„•)
293289, 292ffvelcdmd 7088 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (πΉβ€˜π‘˜) ∈ 𝑋)
294 elbl3 23898 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐷 ∈ (∞Metβ€˜π‘‹) ∧ (π‘Ÿ / 2) ∈ ℝ*) ∧ (𝑦 ∈ 𝑋 ∧ (πΉβ€˜π‘˜) ∈ 𝑋)) β†’ ((πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ↔ ((πΉβ€˜π‘˜)𝐷𝑦) < (π‘Ÿ / 2)))
295284, 287, 288, 293, 294syl22anc 838 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)) ↔ ((πΉβ€˜π‘˜)𝐷𝑦) < (π‘Ÿ / 2)))
296283, 295mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((πΉβ€˜π‘˜)𝐷𝑦) < (π‘Ÿ / 2))
2972ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ 𝐷 ∈ (Metβ€˜π‘‹))
298 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))
299 eluznn 12902 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘˜ ∈ β„• ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜)) β†’ 𝑛 ∈ β„•)
300292, 298, 299syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ 𝑛 ∈ β„•)
301289, 300ffvelcdmd 7088 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (πΉβ€˜π‘›) ∈ 𝑋)
302 metcl 23838 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ (πΉβ€˜π‘›) ∈ 𝑋) β†’ ((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) ∈ ℝ)
303297, 293, 301, 302syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) ∈ ℝ)
304 metcl 23838 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ((πΉβ€˜π‘˜)𝐷𝑦) ∈ ℝ)
305297, 293, 288, 304syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((πΉβ€˜π‘˜)𝐷𝑦) ∈ ℝ)
306286rpred 13016 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (π‘Ÿ / 2) ∈ ℝ)
307 lt2add 11699 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) ∈ ℝ ∧ ((πΉβ€˜π‘˜)𝐷𝑦) ∈ ℝ) ∧ ((π‘Ÿ / 2) ∈ ℝ ∧ (π‘Ÿ / 2) ∈ ℝ)) β†’ ((((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ ((πΉβ€˜π‘˜)𝐷𝑦) < (π‘Ÿ / 2)) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < ((π‘Ÿ / 2) + (π‘Ÿ / 2))))
308303, 305, 306, 306, 307syl22anc 838 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ ((πΉβ€˜π‘˜)𝐷𝑦) < (π‘Ÿ / 2)) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < ((π‘Ÿ / 2) + (π‘Ÿ / 2))))
309296, 308mpan2d 693 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < ((π‘Ÿ / 2) + (π‘Ÿ / 2))))
310285rpcnd 13018 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ π‘Ÿ ∈ β„‚)
3113102halvesd 12458 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((π‘Ÿ / 2) + (π‘Ÿ / 2)) = π‘Ÿ)
312311breq2d 5161 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < ((π‘Ÿ / 2) + (π‘Ÿ / 2)) ↔ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < π‘Ÿ))
313309, 312sylibd 238 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < π‘Ÿ))
314 mettri2 23847 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ ((πΉβ€˜π‘˜) ∈ 𝑋 ∧ (πΉβ€˜π‘›) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ ((πΉβ€˜π‘›)𝐷𝑦) ≀ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)))
315297, 293, 301, 288, 314syl13anc 1373 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((πΉβ€˜π‘›)𝐷𝑦) ≀ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)))
316 metcl 23838 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (Metβ€˜π‘‹) ∧ (πΉβ€˜π‘›) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ((πΉβ€˜π‘›)𝐷𝑦) ∈ ℝ)
317297, 301, 288, 316syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((πΉβ€˜π‘›)𝐷𝑦) ∈ ℝ)
318303, 305readdcld 11243 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) ∈ ℝ)
319285rpred 13016 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ π‘Ÿ ∈ ℝ)
320 lelttr 11304 . . . . . . . . . . . . . . . . . . . . . 22 ((((πΉβ€˜π‘›)𝐷𝑦) ∈ ℝ ∧ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) ∈ ℝ ∧ π‘Ÿ ∈ ℝ) β†’ ((((πΉβ€˜π‘›)𝐷𝑦) ≀ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) ∧ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < π‘Ÿ) β†’ ((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
321317, 318, 319, 320syl3anc 1372 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((((πΉβ€˜π‘›)𝐷𝑦) ≀ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) ∧ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < π‘Ÿ) β†’ ((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
322315, 321mpand 694 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ ((((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) + ((πΉβ€˜π‘˜)𝐷𝑦)) < π‘Ÿ β†’ ((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
323313, 322syld 47 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ ((π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜))) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ ((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
324323anassrs 469 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ (π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘˜)) β†’ (((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ ((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
325324ralimdva 3168 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ (π‘˜ ∈ (β„€β‰₯β€˜π‘š) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)))) β†’ (βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
326325expr 458 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘š)) β†’ ((πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)) β†’ (βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ)))
327326com23 86 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘š)) β†’ (βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ ((πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2)) β†’ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ)))
328327impd 412 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘š)) β†’ ((βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) β†’ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
329328reximdva 3169 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) β†’ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
330 ssrexv 4052 . . . . . . . . . . . . 13 ((β„€β‰₯β€˜π‘š) βŠ† β„• β†’ (βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ β†’ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
331282, 329, 330sylsyld 61 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) β†’ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
332220, 331syldanl 603 . . . . . . . . . . 11 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ (πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) β†’ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
333280, 332syl5 34 . . . . . . . . . 10 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ ((βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) ∧ βˆƒπ‘˜ ∈ (β„€β‰₯β€˜π‘š)(πΉβ€˜π‘˜) ∈ (𝑦(ballβ€˜π·)(π‘Ÿ / 2))) β†’ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
334279, 333mpan2d 693 . . . . . . . . 9 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ (π‘Ÿ ∈ ℝ+ ∧ π‘š ∈ β„•)) β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
335334anassrs 469 . . . . . . . 8 ((((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ π‘Ÿ ∈ ℝ+) ∧ π‘š ∈ β„•) β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
336335rexlimdva 3156 . . . . . . 7 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ π‘Ÿ ∈ ℝ+) β†’ (βˆƒπ‘š ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘š)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘˜)𝐷(πΉβ€˜π‘›)) < (π‘Ÿ / 2) β†’ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ))
337237, 336mpd 15 . . . . . 6 (((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) ∧ π‘Ÿ ∈ ℝ+) β†’ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ)
338337ralrimiva 3147 . . . . 5 ((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ)
339 eqidd 2734 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) = (πΉβ€˜π‘›))
3405, 4, 129, 222, 339, 9lmmbrf 24779 . . . . . 6 (πœ‘ β†’ (𝐹(β‡π‘‘β€˜π½)𝑦 ↔ (𝑦 ∈ 𝑋 ∧ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ)))
341340adantr 482 . . . . 5 ((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ (𝐹(β‡π‘‘β€˜π½)𝑦 ↔ (𝑦 ∈ 𝑋 ∧ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘˜ ∈ β„• βˆ€π‘› ∈ (β„€β‰₯β€˜π‘˜)((πΉβ€˜π‘›)𝐷𝑦) < π‘Ÿ)))
342220, 338, 341mpbir2and 712 . . . 4 ((πœ‘ ∧ βˆ€π‘’ ∈ ran β„€β‰₯𝑦 ∈ ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))) β†’ 𝐹(β‡π‘‘β€˜π½)𝑦)
343200, 342sylan2br 596 . . 3 ((πœ‘ ∧ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}) β†’ 𝐹(β‡π‘‘β€˜π½)𝑦)
344 releldm 5944 . . 3 ((Rel (β‡π‘‘β€˜π½) ∧ 𝐹(β‡π‘‘β€˜π½)𝑦) β†’ 𝐹 ∈ dom (β‡π‘‘β€˜π½))
345189, 343, 344sylancr 588 . 2 ((πœ‘ ∧ 𝑦 ∈ ∩ {π‘˜ ∣ βˆƒπ‘’ ∈ ran β„€β‰₯π‘˜ = ((clsβ€˜π½)β€˜(𝐹 β€œ 𝑒))}) β†’ 𝐹 ∈ dom (β‡π‘‘β€˜π½))
346188, 345exlimddv 1939 1 (πœ‘ β†’ 𝐹 ∈ dom (β‡π‘‘β€˜π½))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088  βˆ€wal 1540   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  {cab 2710   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   βˆͺ cun 3947   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  π’« cpw 4603  {csn 4629  βˆͺ cuni 4909  βˆ© cint 4951   class class class wbr 5149  dom cdm 5677  ran crn 5678   β€œ cima 5680  Rel wrel 5682  Fun wfun 6538   Fn wfn 6539  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409   ↑pm cpm 8821  Fincfn 8939  ficfi 9405  β„‚cc 11108  β„cr 11109  0cc0 11110  1c1 11111   + caddc 11113  β„*cxr 11247   < clt 11248   ≀ cle 11249   / cdiv 11871  β„•cn 12212  2c2 12267  β„€cz 12558  β„€β‰₯cuz 12822  β„+crp 12974  βˆžMetcxmet 20929  Metcmet 20930  ballcbl 20931  MetOpencmopn 20934  Topctop 22395  Clsdccld 22520  clsccl 22522  β‡π‘‘clm 22730  Compccmp 22890  Cauccau 24770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-map 8822  df-pm 8823  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fi 9406  df-sup 9437  df-inf 9438  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-n0 12473  df-z 12559  df-uz 12823  df-q 12933  df-rp 12975  df-xneg 13092  df-xadd 13093  df-xmul 13094  df-topgen 17389  df-psmet 20936  df-xmet 20937  df-met 20938  df-bl 20939  df-mopn 20940  df-top 22396  df-topon 22413  df-bases 22449  df-cld 22523  df-ntr 22524  df-cls 22525  df-lm 22733  df-cmp 22891  df-cau 24773
This theorem is referenced by:  heibor1  36678
  Copyright terms: Public domain W3C validator