Step | Hyp | Ref
| Expression |
1 | | fge0iccico.f |
. . . 4
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) |
2 | 1 | ffnd 6670 |
. . 3
⊢ (𝜑 → 𝐹 Fn 𝑋) |
3 | | 0xr 11207 |
. . . . . 6
⊢ 0 ∈
ℝ* |
4 | 3 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 0 ∈
ℝ*) |
5 | | pnfxr 11214 |
. . . . . 6
⊢ +∞
∈ ℝ* |
6 | 5 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → +∞ ∈
ℝ*) |
7 | | iccssxr 13353 |
. . . . . 6
⊢
(0[,]+∞) ⊆ ℝ* |
8 | 1 | ffvelcdmda 7036 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ (0[,]+∞)) |
9 | 7, 8 | sselid 3943 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈
ℝ*) |
10 | | iccgelb 13326 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝐹‘𝑥) ∈ (0[,]+∞)) → 0 ≤ (𝐹‘𝑥)) |
11 | 4, 6, 8, 10 | syl3anc 1372 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 0 ≤ (𝐹‘𝑥)) |
12 | 9 | adantr 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → (𝐹‘𝑥) ∈
ℝ*) |
13 | | simpr 486 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → ¬ (𝐹‘𝑥) < +∞) |
14 | 5 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → +∞ ∈
ℝ*) |
15 | 14, 12 | xrlenltd 11226 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → (+∞ ≤ (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑥) < +∞)) |
16 | 13, 15 | mpbird 257 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → +∞ ≤ (𝐹‘𝑥)) |
17 | 12, 16 | xrgepnfd 43652 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → (𝐹‘𝑥) = +∞) |
18 | 17 | eqcomd 2739 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → +∞ = (𝐹‘𝑥)) |
19 | 1 | ffund 6673 |
. . . . . . . . . 10
⊢ (𝜑 → Fun 𝐹) |
20 | 19 | adantr 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Fun 𝐹) |
21 | | simpr 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
22 | | fdm 6678 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝑋⟶(0[,]+∞) → dom 𝐹 = 𝑋) |
23 | 22 | eqcomd 2739 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋⟶(0[,]+∞) → 𝑋 = dom 𝐹) |
24 | 1, 23 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 = dom 𝐹) |
25 | 24 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑋 = dom 𝐹) |
26 | 21, 25 | eleqtrd 2836 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ dom 𝐹) |
27 | | fvelrn 7028 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ran 𝐹) |
28 | 20, 26, 27 | syl2anc 585 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ran 𝐹) |
29 | 28 | adantr 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → (𝐹‘𝑥) ∈ ran 𝐹) |
30 | 18, 29 | eqeltrd 2834 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → +∞ ∈ ran
𝐹) |
31 | | fge0iccico.re |
. . . . . . 7
⊢ (𝜑 → ¬ +∞ ∈ ran
𝐹) |
32 | 31 | ad2antrr 725 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → ¬ +∞ ∈
ran 𝐹) |
33 | 30, 32 | condan 817 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) < +∞) |
34 | 4, 6, 9, 11, 33 | elicod 13320 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
35 | 34 | ralrimiva 3140 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (0[,)+∞)) |
36 | 2, 35 | jca 513 |
. 2
⊢ (𝜑 → (𝐹 Fn 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (0[,)+∞))) |
37 | | ffnfv 7067 |
. 2
⊢ (𝐹:𝑋⟶(0[,)+∞) ↔ (𝐹 Fn 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (0[,)+∞))) |
38 | 36, 37 | sylibr 233 |
1
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) |