Step | Hyp | Ref
| Expression |
1 | | fge0iccico.f |
. . . 4
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) |
2 | | ffn 6045 |
. . . 4
⊢ (𝐹:𝑋⟶(0[,]+∞) → 𝐹 Fn 𝑋) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹 Fn 𝑋) |
4 | | 0xr 10086 |
. . . . . 6
⊢ 0 ∈
ℝ* |
5 | 4 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 0 ∈
ℝ*) |
6 | | pnfxr 10092 |
. . . . . 6
⊢ +∞
∈ ℝ* |
7 | 6 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → +∞ ∈
ℝ*) |
8 | | iccssxr 12256 |
. . . . . 6
⊢
(0[,]+∞) ⊆ ℝ* |
9 | 1 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ (0[,]+∞)) |
10 | 8, 9 | sseldi 3601 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈
ℝ*) |
11 | | iccgelb 12230 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝐹‘𝑥) ∈ (0[,]+∞)) → 0 ≤ (𝐹‘𝑥)) |
12 | 5, 7, 9, 11 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 0 ≤ (𝐹‘𝑥)) |
13 | 10 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → (𝐹‘𝑥) ∈
ℝ*) |
14 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → ¬ (𝐹‘𝑥) < +∞) |
15 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → +∞ ∈
ℝ*) |
16 | 15, 13 | xrlenltd 10104 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → (+∞ ≤ (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑥) < +∞)) |
17 | 14, 16 | mpbird 247 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → +∞ ≤ (𝐹‘𝑥)) |
18 | 13, 17 | xrgepnfd 39547 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → (𝐹‘𝑥) = +∞) |
19 | 18 | eqcomd 2628 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → +∞ = (𝐹‘𝑥)) |
20 | | ffun 6048 |
. . . . . . . . . . 11
⊢ (𝐹:𝑋⟶(0[,]+∞) → Fun 𝐹) |
21 | 1, 20 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → Fun 𝐹) |
22 | 21 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Fun 𝐹) |
23 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
24 | | fdm 6051 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝑋⟶(0[,]+∞) → dom 𝐹 = 𝑋) |
25 | 24 | eqcomd 2628 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋⟶(0[,]+∞) → 𝑋 = dom 𝐹) |
26 | 1, 25 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 = dom 𝐹) |
27 | 26 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑋 = dom 𝐹) |
28 | 23, 27 | eleqtrd 2703 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ dom 𝐹) |
29 | | fvelrn 6352 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ran 𝐹) |
30 | 22, 28, 29 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ran 𝐹) |
31 | 30 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → (𝐹‘𝑥) ∈ ran 𝐹) |
32 | 19, 31 | eqeltrd 2701 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → +∞ ∈ ran
𝐹) |
33 | | fge0iccico.re |
. . . . . . 7
⊢ (𝜑 → ¬ +∞ ∈ ran
𝐹) |
34 | 33 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ (𝐹‘𝑥) < +∞) → ¬ +∞ ∈
ran 𝐹) |
35 | 32, 34 | condan 835 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) < +∞) |
36 | 5, 7, 10, 12, 35 | elicod 12224 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
37 | 36 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (0[,)+∞)) |
38 | 3, 37 | jca 554 |
. 2
⊢ (𝜑 → (𝐹 Fn 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (0[,)+∞))) |
39 | | ffnfv 6388 |
. 2
⊢ (𝐹:𝑋⟶(0[,)+∞) ↔ (𝐹 Fn 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (0[,)+∞))) |
40 | 38, 39 | sylibr 224 |
1
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) |