| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lebnumlem1.u | . . . . 5
⊢ (𝜑 → 𝑈 ∈ Fin) | 
| 2 | 1 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑈 ∈ Fin) | 
| 3 |  | lebnum.d | . . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) | 
| 4 | 3 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → 𝐷 ∈ (Met‘𝑋)) | 
| 5 |  | difssd 4137 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → (𝑋 ∖ 𝑘) ⊆ 𝑋) | 
| 6 |  | lebnum.s | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ⊆ 𝐽) | 
| 7 | 6 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑈 ⊆ 𝐽) | 
| 8 | 7 | sselda 3983 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝐽) | 
| 9 |  | elssuni 4937 | . . . . . . . . . 10
⊢ (𝑘 ∈ 𝐽 → 𝑘 ⊆ ∪ 𝐽) | 
| 10 | 8, 9 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → 𝑘 ⊆ ∪ 𝐽) | 
| 11 |  | metxmet 24344 | . . . . . . . . . . . 12
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 12 | 3, 11 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) | 
| 13 |  | lebnum.j | . . . . . . . . . . . 12
⊢ 𝐽 = (MetOpen‘𝐷) | 
| 14 | 13 | mopnuni 24451 | . . . . . . . . . . 11
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) | 
| 15 | 12, 14 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 = ∪ 𝐽) | 
| 16 | 15 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → 𝑋 = ∪ 𝐽) | 
| 17 | 10, 16 | sseqtrrd 4021 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → 𝑘 ⊆ 𝑋) | 
| 18 |  | lebnumlem1.n | . . . . . . . . . . . 12
⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) | 
| 19 |  | eleq1 2829 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑋 → (𝑘 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈)) | 
| 20 | 19 | notbid 318 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑋 → (¬ 𝑘 ∈ 𝑈 ↔ ¬ 𝑋 ∈ 𝑈)) | 
| 21 | 18, 20 | syl5ibrcom 247 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑘 = 𝑋 → ¬ 𝑘 ∈ 𝑈)) | 
| 22 | 21 | necon2ad 2955 | . . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝑈 → 𝑘 ≠ 𝑋)) | 
| 23 | 22 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑘 ∈ 𝑈 → 𝑘 ≠ 𝑋)) | 
| 24 | 23 | imp 406 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → 𝑘 ≠ 𝑋) | 
| 25 |  | pssdifn0 4368 | . . . . . . . 8
⊢ ((𝑘 ⊆ 𝑋 ∧ 𝑘 ≠ 𝑋) → (𝑋 ∖ 𝑘) ≠ ∅) | 
| 26 | 17, 24, 25 | syl2anc 584 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → (𝑋 ∖ 𝑘) ≠ ∅) | 
| 27 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )) = (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, <
)) | 
| 28 | 27 | metdsre 24875 | . . . . . . 7
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝑋 ∖ 𝑘) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑘) ≠ ∅) → (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )):𝑋⟶ℝ) | 
| 29 | 4, 5, 26, 28 | syl3anc 1373 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )):𝑋⟶ℝ) | 
| 30 | 27 | fmpt 7130 | . . . . . 6
⊢
(∀𝑦 ∈
𝑋 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
ℝ ↔ (𝑦 ∈
𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )):𝑋⟶ℝ) | 
| 31 | 29, 30 | sylibr 234 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → ∀𝑦 ∈ 𝑋 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
ℝ) | 
| 32 |  | simplr 769 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → 𝑦 ∈ 𝑋) | 
| 33 |  | rsp 3247 | . . . . 5
⊢
(∀𝑦 ∈
𝑋 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
ℝ → (𝑦 ∈
𝑋 → inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
ℝ)) | 
| 34 | 31, 32, 33 | sylc 65 | . . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
ℝ) | 
| 35 | 2, 34 | fsumrecl 15770 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
ℝ) | 
| 36 |  | lebnum.u | . . . . . . 7
⊢ (𝜑 → 𝑋 = ∪ 𝑈) | 
| 37 | 36 | eleq2d 2827 | . . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝑋 ↔ 𝑦 ∈ ∪ 𝑈)) | 
| 38 | 37 | biimpa 476 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ ∪ 𝑈) | 
| 39 |  | eluni2 4911 | . . . . 5
⊢ (𝑦 ∈ ∪ 𝑈
↔ ∃𝑚 ∈
𝑈 𝑦 ∈ 𝑚) | 
| 40 | 38, 39 | sylib 218 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑚 ∈ 𝑈 𝑦 ∈ 𝑚) | 
| 41 |  | 0red 11264 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 0 ∈ ℝ) | 
| 42 |  | simplr 769 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 𝑦 ∈ 𝑋) | 
| 43 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < )) = (𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, <
)) | 
| 44 | 43 | metdsval 24869 | . . . . . . 7
⊢ (𝑦 ∈ 𝑋 → ((𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < ))‘𝑦) = inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑦𝐷𝑧)), ℝ*, <
)) | 
| 45 | 42, 44 | syl 17 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → ((𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < ))‘𝑦) = inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑦𝐷𝑧)), ℝ*, <
)) | 
| 46 | 3 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 𝐷 ∈ (Met‘𝑋)) | 
| 47 |  | difssd 4137 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → (𝑋 ∖ 𝑚) ⊆ 𝑋) | 
| 48 | 6 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 𝑈 ⊆ 𝐽) | 
| 49 |  | simprl 771 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 𝑚 ∈ 𝑈) | 
| 50 | 48, 49 | sseldd 3984 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 𝑚 ∈ 𝐽) | 
| 51 |  | elssuni 4937 | . . . . . . . . . . 11
⊢ (𝑚 ∈ 𝐽 → 𝑚 ⊆ ∪ 𝐽) | 
| 52 | 50, 51 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 𝑚 ⊆ ∪ 𝐽) | 
| 53 | 46, 11, 14 | 3syl 18 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 𝑋 = ∪ 𝐽) | 
| 54 | 52, 53 | sseqtrrd 4021 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 𝑚 ⊆ 𝑋) | 
| 55 |  | eleq1 2829 | . . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑋 → (𝑚 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈)) | 
| 56 | 55 | notbid 318 | . . . . . . . . . . . . 13
⊢ (𝑚 = 𝑋 → (¬ 𝑚 ∈ 𝑈 ↔ ¬ 𝑋 ∈ 𝑈)) | 
| 57 | 18, 56 | syl5ibrcom 247 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑚 = 𝑋 → ¬ 𝑚 ∈ 𝑈)) | 
| 58 | 57 | necon2ad 2955 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑚 ∈ 𝑈 → 𝑚 ≠ 𝑋)) | 
| 59 | 58 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → (𝑚 ∈ 𝑈 → 𝑚 ≠ 𝑋)) | 
| 60 | 49, 59 | mpd 15 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 𝑚 ≠ 𝑋) | 
| 61 |  | pssdifn0 4368 | . . . . . . . . 9
⊢ ((𝑚 ⊆ 𝑋 ∧ 𝑚 ≠ 𝑋) → (𝑋 ∖ 𝑚) ≠ ∅) | 
| 62 | 54, 60, 61 | syl2anc 584 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → (𝑋 ∖ 𝑚) ≠ ∅) | 
| 63 | 43 | metdsre 24875 | . . . . . . . 8
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝑋 ∖ 𝑚) ⊆ 𝑋 ∧ (𝑋 ∖ 𝑚) ≠ ∅) → (𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < )):𝑋⟶ℝ) | 
| 64 | 46, 47, 62, 63 | syl3anc 1373 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → (𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < )):𝑋⟶ℝ) | 
| 65 | 64, 42 | ffvelcdmd 7105 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → ((𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < ))‘𝑦) ∈
ℝ) | 
| 66 | 45, 65 | eqeltrrd 2842 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
ℝ) | 
| 67 | 35 | adantr 480 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
ℝ) | 
| 68 | 12 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 69 | 43 | metdsf 24870 | . . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑋 ∖ 𝑚) ⊆ 𝑋) → (𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < )):𝑋⟶(0[,]+∞)) | 
| 70 | 68, 47, 69 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → (𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < )):𝑋⟶(0[,]+∞)) | 
| 71 | 70, 42 | ffvelcdmd 7105 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → ((𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < ))‘𝑦) ∈
(0[,]+∞)) | 
| 72 |  | elxrge0 13497 | . . . . . . . . 9
⊢ (((𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < ))‘𝑦) ∈ (0[,]+∞) ↔
(((𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < ))‘𝑦) ∈ ℝ*
∧ 0 ≤ ((𝑤 ∈
𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < ))‘𝑦))) | 
| 73 | 71, 72 | sylib 218 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → (((𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < ))‘𝑦) ∈ ℝ*
∧ 0 ≤ ((𝑤 ∈
𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < ))‘𝑦))) | 
| 74 | 73 | simprd 495 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 0 ≤ ((𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < ))‘𝑦)) | 
| 75 |  | elndif 4133 | . . . . . . . . . 10
⊢ (𝑦 ∈ 𝑚 → ¬ 𝑦 ∈ (𝑋 ∖ 𝑚)) | 
| 76 | 75 | ad2antll 729 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → ¬ 𝑦 ∈ (𝑋 ∖ 𝑚)) | 
| 77 | 53 | difeq1d 4125 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → (𝑋 ∖ 𝑚) = (∪ 𝐽 ∖ 𝑚)) | 
| 78 | 13 | mopntop 24450 | . . . . . . . . . . . . 13
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) | 
| 79 | 68, 78 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 𝐽 ∈ Top) | 
| 80 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 81 | 80 | opncld 23041 | . . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝑚 ∈ 𝐽) → (∪ 𝐽 ∖ 𝑚) ∈ (Clsd‘𝐽)) | 
| 82 | 79, 50, 81 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → (∪ 𝐽 ∖ 𝑚) ∈ (Clsd‘𝐽)) | 
| 83 | 77, 82 | eqeltrd 2841 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → (𝑋 ∖ 𝑚) ∈ (Clsd‘𝐽)) | 
| 84 |  | cldcls 23050 | . . . . . . . . . 10
⊢ ((𝑋 ∖ 𝑚) ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘(𝑋 ∖ 𝑚)) = (𝑋 ∖ 𝑚)) | 
| 85 | 83, 84 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → ((cls‘𝐽)‘(𝑋 ∖ 𝑚)) = (𝑋 ∖ 𝑚)) | 
| 86 | 76, 85 | neleqtrrd 2864 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → ¬ 𝑦 ∈ ((cls‘𝐽)‘(𝑋 ∖ 𝑚))) | 
| 87 | 43, 13 | metdseq0 24876 | . . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑋 ∖ 𝑚) ⊆ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < ))‘𝑦) = 0 ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝑋 ∖ 𝑚)))) | 
| 88 | 68, 47, 42, 87 | syl3anc 1373 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → (((𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < ))‘𝑦) = 0 ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝑋 ∖ 𝑚)))) | 
| 89 | 88 | necon3abid 2977 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → (((𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < ))‘𝑦) ≠ 0 ↔ ¬ 𝑦 ∈ ((cls‘𝐽)‘(𝑋 ∖ 𝑚)))) | 
| 90 | 86, 89 | mpbird 257 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → ((𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < ))‘𝑦) ≠ 0) | 
| 91 | 65, 74, 90 | ne0gt0d 11398 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 0 < ((𝑤 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑤𝐷𝑧)), ℝ*, < ))‘𝑦)) | 
| 92 | 91, 45 | breqtrd 5169 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 0 < inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑦𝐷𝑧)), ℝ*, <
)) | 
| 93 | 1 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 𝑈 ∈ Fin) | 
| 94 | 34 | adantlr 715 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) ∧ 𝑘 ∈ 𝑈) → inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
ℝ) | 
| 95 | 12 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 96 | 27 | metdsf 24870 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑋 ∖ 𝑘) ⊆ 𝑋) → (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )):𝑋⟶(0[,]+∞)) | 
| 97 | 95, 5, 96 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → (𝑦 ∈ 𝑋 ↦ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )):𝑋⟶(0[,]+∞)) | 
| 98 | 27 | fmpt 7130 | . . . . . . . . . . 11
⊢
(∀𝑦 ∈
𝑋 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
(0[,]+∞) ↔ (𝑦
∈ 𝑋 ↦ inf(ran
(𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )):𝑋⟶(0[,]+∞)) | 
| 99 | 97, 98 | sylibr 234 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → ∀𝑦 ∈ 𝑋 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
(0[,]+∞)) | 
| 100 |  | rsp 3247 | . . . . . . . . . 10
⊢
(∀𝑦 ∈
𝑋 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
(0[,]+∞) → (𝑦
∈ 𝑋 → inf(ran
(𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
(0[,]+∞))) | 
| 101 | 99, 32, 100 | sylc 65 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
(0[,]+∞)) | 
| 102 |  | elxrge0 13497 | . . . . . . . . 9
⊢ (inf(ran
(𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
(0[,]+∞) ↔ (inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
ℝ* ∧ 0 ≤ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, <
))) | 
| 103 | 101, 102 | sylib 218 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → (inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
ℝ* ∧ 0 ≤ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, <
))) | 
| 104 | 103 | simprd 495 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑘 ∈ 𝑈) → 0 ≤ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, <
)) | 
| 105 | 104 | adantlr 715 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) ∧ 𝑘 ∈ 𝑈) → 0 ≤ inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, <
)) | 
| 106 |  | difeq2 4120 | . . . . . . . . 9
⊢ (𝑘 = 𝑚 → (𝑋 ∖ 𝑘) = (𝑋 ∖ 𝑚)) | 
| 107 | 106 | mpteq1d 5237 | . . . . . . . 8
⊢ (𝑘 = 𝑚 → (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)) = (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑦𝐷𝑧))) | 
| 108 | 107 | rneqd 5949 | . . . . . . 7
⊢ (𝑘 = 𝑚 → ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)) = ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑦𝐷𝑧))) | 
| 109 | 108 | infeq1d 9517 | . . . . . 6
⊢ (𝑘 = 𝑚 → inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) = inf(ran
(𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑦𝐷𝑧)), ℝ*, <
)) | 
| 110 | 93, 94, 105, 109, 49 | fsumge1 15833 | . . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → inf(ran (𝑧 ∈ (𝑋 ∖ 𝑚) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ≤
Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, <
)) | 
| 111 | 41, 66, 67, 92, 110 | ltletrd 11421 | . . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑈 ∧ 𝑦 ∈ 𝑚)) → 0 < Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, <
)) | 
| 112 | 40, 111 | rexlimddv 3161 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 0 < Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, <
)) | 
| 113 | 35, 112 | elrpd 13074 | . 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ) ∈
ℝ+) | 
| 114 |  | lebnumlem1.f | . 2
⊢ 𝐹 = (𝑦 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, <
)) | 
| 115 | 113, 114 | fmptd 7134 | 1
⊢ (𝜑 → 𝐹:𝑋⟶ℝ+) |