| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fge0iccico.f | . . . 4
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) | 
| 2 | 1 | ffnd 6736 | . . 3
⊢ (𝜑 → 𝐹 Fn 𝑋) | 
| 3 |  | 0xr 11309 | . . . . . 6
⊢ 0 ∈
ℝ* | 
| 4 | 3 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 0 ∈
ℝ*) | 
| 5 |  | pnfxr 11316 | . . . . . 6
⊢ +∞
∈ ℝ* | 
| 6 | 5 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → +∞ ∈
ℝ*) | 
| 7 |  | iccssxr 13471 | . . . . . 6
⊢
(0[,]+∞) ⊆ ℝ* | 
| 8 | 1 | ffvelcdmda 7103 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ (0[,]+∞)) | 
| 9 | 7, 8 | sselid 3980 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈
ℝ*) | 
| 10 |  | iccgelb 13444 | . . . . . 6
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝐹‘𝑥) ∈ (0[,]+∞)) → 0 ≤ (𝐹‘𝑥)) | 
| 11 | 4, 6, 8, 10 | syl3anc 1372 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 0 ≤ (𝐹‘𝑥)) | 
| 12 | 9 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → (𝐹‘𝑥) ∈
ℝ*) | 
| 13 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → ¬ (𝐹‘𝑥) < +∞) | 
| 14 | 5 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → +∞ ∈
ℝ*) | 
| 15 | 14, 12 | xrlenltd 11328 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → (+∞ ≤ (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑥) < +∞)) | 
| 16 | 13, 15 | mpbird 257 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → +∞ ≤ (𝐹‘𝑥)) | 
| 17 | 12, 16 | xrgepnfd 45347 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → (𝐹‘𝑥) = +∞) | 
| 18 | 17 | eqcomd 2742 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → +∞ = (𝐹‘𝑥)) | 
| 19 | 1 | ffund 6739 | . . . . . . . . . 10
⊢ (𝜑 → Fun 𝐹) | 
| 20 | 19 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Fun 𝐹) | 
| 21 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) | 
| 22 |  | fdm 6744 | . . . . . . . . . . . . 13
⊢ (𝐹:𝑋⟶(0[,]+∞) → dom 𝐹 = 𝑋) | 
| 23 | 22 | eqcomd 2742 | . . . . . . . . . . . 12
⊢ (𝐹:𝑋⟶(0[,]+∞) → 𝑋 = dom 𝐹) | 
| 24 | 1, 23 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑋 = dom 𝐹) | 
| 25 | 24 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑋 = dom 𝐹) | 
| 26 | 21, 25 | eleqtrd 2842 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ dom 𝐹) | 
| 27 |  | fvelrn 7095 | . . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ran 𝐹) | 
| 28 | 20, 26, 27 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ran 𝐹) | 
| 29 | 28 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → (𝐹‘𝑥) ∈ ran 𝐹) | 
| 30 | 18, 29 | eqeltrd 2840 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → +∞ ∈ ran
𝐹) | 
| 31 |  | fge0iccico.re | . . . . . . 7
⊢ (𝜑 → ¬ +∞ ∈ ran
𝐹) | 
| 32 | 31 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → ¬ +∞ ∈
ran 𝐹) | 
| 33 | 30, 32 | condan 817 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) < +∞) | 
| 34 | 4, 6, 9, 11, 33 | elicod 13438 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ (0[,)+∞)) | 
| 35 | 34 | ralrimiva 3145 | . . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (0[,)+∞)) | 
| 36 | 2, 35 | jca 511 | . 2
⊢ (𝜑 → (𝐹 Fn 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (0[,)+∞))) | 
| 37 |  | ffnfv 7138 | . 2
⊢ (𝐹:𝑋⟶(0[,)+∞) ↔ (𝐹 Fn 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (0[,)+∞))) | 
| 38 | 36, 37 | sylibr 234 | 1
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) |