| Step | Hyp | Ref
| Expression |
| 1 | | bndth.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
| 2 | | bndth.2 |
. . . . 5
⊢ 𝐾 = (topGen‘ran
(,)) |
| 3 | | bndth.3 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ Comp) |
| 4 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
𝐽 ∈
Comp) |
| 5 | | cmptop 23403 |
. . . . . . . . . 10
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
| 6 | 4, 5 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
𝐽 ∈
Top) |
| 7 | 1 | toptopon 22923 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
| 8 | 6, 7 | sylib 218 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
𝐽 ∈ (TopOn‘𝑋)) |
| 9 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 10 | 9 | cnfldtopon 24803 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
| 12 | | 1cnd 11256 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → 1
∈ ℂ) |
| 13 | 8, 11, 12 | cnmptc 23670 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ 1) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
| 14 | | bndth.4 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
| 15 | | uniretop 24783 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℝ =
∪ (topGen‘ran (,)) |
| 16 | 2 | unieqi 4919 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∪ 𝐾 =
∪ (topGen‘ran (,)) |
| 17 | 15, 16 | eqtr4i 2768 |
. . . . . . . . . . . . . . . . . 18
⊢ ℝ =
∪ 𝐾 |
| 18 | 1, 17 | cnf 23254 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶ℝ) |
| 19 | 14, 18 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
| 20 | 19 | frnd 6744 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
| 21 | 19 | fdmd 6746 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐹 = 𝑋) |
| 22 | | evth.5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 ≠ ∅) |
| 23 | 21, 22 | eqnetrd 3008 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐹 ≠ ∅) |
| 24 | | dm0rn0 5935 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
𝐹 = ∅ ↔ ran
𝐹 =
∅) |
| 25 | 24 | necon3bii 2993 |
. . . . . . . . . . . . . . . 16
⊢ (dom
𝐹 ≠ ∅ ↔ ran
𝐹 ≠
∅) |
| 26 | 23, 25 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐹 ≠ ∅) |
| 27 | 1, 2, 3, 14 | bndth 24990 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥) |
| 28 | 19 | ffnd 6737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 Fn 𝑋) |
| 29 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝐹‘𝑦) → (𝑧 ≤ 𝑥 ↔ (𝐹‘𝑦) ≤ 𝑥)) |
| 30 | 29 | ralrn 7108 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 Fn 𝑋 → (∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥)) |
| 31 | 28, 30 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥)) |
| 32 | 31 | rexbidv 3179 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥)) |
| 33 | 27, 32 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥) |
| 34 | 20, 26, 33 | 3jca 1129 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥)) |
| 35 | | suprcl 12228 |
. . . . . . . . . . . . . 14
⊢ ((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥) → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
| 36 | 34, 35 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
| 37 | 36 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → sup(ran 𝐹, ℝ, < ) ∈
ℂ) |
| 38 | 37 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
sup(ran 𝐹, ℝ, < )
∈ ℂ) |
| 39 | 8, 11, 38 | cnmptc 23670 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ sup(ran 𝐹, ℝ, < )) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
| 40 | 19 | feqmptd 6977 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 = (𝑧 ∈ 𝑋 ↦ (𝐹‘𝑧))) |
| 41 | 9 | cnfldtop 24804 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈ Top |
| 42 | | cnrest2r 23295 |
. . . . . . . . . . . . . 14
⊢
((TopOpen‘ℂfld) ∈ Top → (𝐽 Cn
((TopOpen‘ℂfld) ↾t ℝ)) ⊆
(𝐽 Cn
(TopOpen‘ℂfld))) |
| 43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐽 Cn
((TopOpen‘ℂfld) ↾t ℝ)) ⊆
(𝐽 Cn
(TopOpen‘ℂfld)) |
| 44 | | tgioo4 24826 |
. . . . . . . . . . . . . . . 16
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 45 | 2, 44 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢ 𝐾 =
((TopOpen‘ℂfld) ↾t
ℝ) |
| 46 | 45 | oveq2i 7442 |
. . . . . . . . . . . . . 14
⊢ (𝐽 Cn 𝐾) = (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ)) |
| 47 | 14, 46 | eleqtrdi 2851 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ))) |
| 48 | 43, 47 | sselid 3981 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
| 49 | 40, 48 | eqeltrrd 2842 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ 𝑋 ↦ (𝐹‘𝑧)) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
| 50 | 49 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ (𝐹‘𝑧)) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
| 51 | 9 | subcn 24888 |
. . . . . . . . . . 11
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
| 52 | 51 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
− ∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
| 53 | 8, 39, 50, 52 | cnmpt12f 23674 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
| 54 | 36 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
| 55 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)})) |
| 56 | 55 | adantll 714 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)})) |
| 57 | | eldifsn 4786 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑧) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔
((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) ≠ sup(ran 𝐹, ℝ, < ))) |
| 58 | 56, 57 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) ≠ sup(ran 𝐹, ℝ, < ))) |
| 59 | 58 | simpld 494 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ℝ) |
| 60 | 54, 59 | resubcld 11691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)) ∈ ℝ) |
| 61 | 60 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)) ∈ ℂ) |
| 62 | 54 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → sup(ran 𝐹, ℝ, < ) ∈
ℂ) |
| 63 | 59 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ℂ) |
| 64 | 58 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ≠ sup(ran 𝐹, ℝ, < )) |
| 65 | 64 | necomd 2996 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → sup(ran 𝐹, ℝ, < ) ≠ (𝐹‘𝑧)) |
| 66 | 62, 63, 65 | subne0d 11629 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)) ≠ 0) |
| 67 | | eldifsn 4786 |
. . . . . . . . . . . . 13
⊢ ((sup(ran
𝐹, ℝ, < ) −
(𝐹‘𝑧)) ∈ (ℂ ∖ {0}) ↔
((sup(ran 𝐹, ℝ, <
) − (𝐹‘𝑧)) ∈ ℂ ∧ (sup(ran
𝐹, ℝ, < ) −
(𝐹‘𝑧)) ≠ 0)) |
| 68 | 61, 66, 67 | sylanbrc 583 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)) ∈ (ℂ ∖
{0})) |
| 69 | 68 | fmpttd 7135 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))):𝑋⟶(ℂ ∖
{0})) |
| 70 | 69 | frnd 6744 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ran
(𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ⊆ (ℂ ∖
{0})) |
| 71 | | difssd 4137 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(ℂ ∖ {0}) ⊆ ℂ) |
| 72 | | cnrest2 23294 |
. . . . . . . . . 10
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ran (𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ⊆ (ℂ ∖ {0}) ∧
(ℂ ∖ {0}) ⊆ ℂ) → ((𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ∈ (𝐽 Cn (TopOpen‘ℂfld))
↔ (𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t (ℂ ∖ {0}))))) |
| 73 | 11, 70, 71, 72 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
((𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ∈ (𝐽 Cn (TopOpen‘ℂfld))
↔ (𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t (ℂ ∖ {0}))))) |
| 74 | 53, 73 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t (ℂ ∖ {0})))) |
| 75 | | eqid 2737 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t (ℂ
∖ {0})) = ((TopOpen‘ℂfld) ↾t
(ℂ ∖ {0})) |
| 76 | 9, 75 | divcn 24892 |
. . . . . . . . 9
⊢ / ∈
(((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) Cn (TopOpen‘ℂfld)) |
| 77 | 76 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → /
∈ (((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) Cn (TopOpen‘ℂfld))) |
| 78 | 8, 13, 74, 77 | cnmpt12f 23674 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
| 79 | 60, 66 | rereccld 12094 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ∈ ℝ) |
| 80 | 79 | fmpttd 7135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))):𝑋⟶ℝ) |
| 81 | 80 | frnd 6744 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ran
(𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ⊆ ℝ) |
| 82 | | ax-resscn 11212 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
| 83 | 82 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
ℝ ⊆ ℂ) |
| 84 | | cnrest2 23294 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ran (𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ⊆ ℝ ∧ ℝ ⊆
ℂ) → ((𝑧 ∈
𝑋 ↦ (1 / (sup(ran
𝐹, ℝ, < ) −
(𝐹‘𝑧)))) ∈ (𝐽 Cn (TopOpen‘ℂfld))
↔ (𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ)))) |
| 85 | 11, 81, 83, 84 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ∈ (𝐽 Cn (TopOpen‘ℂfld))
↔ (𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ)))) |
| 86 | 78, 85 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ))) |
| 87 | 86, 46 | eleqtrrdi 2852 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ∈ (𝐽 Cn 𝐾)) |
| 88 | 1, 2, 4, 87 | bndth 24990 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑋 ((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥) |
| 89 | 36 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → sup(ran
𝐹, ℝ, < ) ∈
ℝ) |
| 90 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈
ℝ) |
| 91 | | 1re 11261 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
| 92 | | ifcl 4571 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 1 ∈
ℝ) → if(1 ≤ 𝑥, 𝑥, 1) ∈ ℝ) |
| 93 | 90, 91, 92 | sylancl 586 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → if(1
≤ 𝑥, 𝑥, 1) ∈ ℝ) |
| 94 | | 0red 11264 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 0 ∈
ℝ) |
| 95 | 91 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 1 ∈
ℝ) |
| 96 | | 0lt1 11785 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
| 97 | 96 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 0 <
1) |
| 98 | | max1 13227 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℝ ∧ 𝑥
∈ ℝ) → 1 ≤ if(1 ≤ 𝑥, 𝑥, 1)) |
| 99 | 91, 90, 98 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 1 ≤
if(1 ≤ 𝑥, 𝑥, 1)) |
| 100 | 94, 95, 93, 97, 99 | ltletrd 11421 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 0 <
if(1 ≤ 𝑥, 𝑥, 1)) |
| 101 | 100 | gt0ne0d 11827 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → if(1
≤ 𝑥, 𝑥, 1) ≠ 0) |
| 102 | 93, 101 | rereccld 12094 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (1 /
if(1 ≤ 𝑥, 𝑥, 1)) ∈
ℝ) |
| 103 | 93, 100 | recgt0d 12202 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 0 <
(1 / if(1 ≤ 𝑥, 𝑥, 1))) |
| 104 | 102, 103 | elrpd 13074 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (1 /
if(1 ≤ 𝑥, 𝑥, 1)) ∈
ℝ+) |
| 105 | 89, 104 | ltsubrpd 13109 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (sup(ran
𝐹, ℝ, < ) −
(1 / if(1 ≤ 𝑥, 𝑥, 1))) < sup(ran 𝐹, ℝ, <
)) |
| 106 | 89, 102 | resubcld 11691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (sup(ran
𝐹, ℝ, < ) −
(1 / if(1 ≤ 𝑥, 𝑥, 1))) ∈
ℝ) |
| 107 | 106, 89 | ltnled 11408 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) →
((sup(ran 𝐹, ℝ, <
) − (1 / if(1 ≤ 𝑥,
𝑥, 1))) < sup(ran 𝐹, ℝ, < ) ↔ ¬
sup(ran 𝐹, ℝ, < )
≤ (sup(ran 𝐹, ℝ,
< ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))))) |
| 108 | 105, 107 | mpbid 232 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → ¬
sup(ran 𝐹, ℝ, < )
≤ (sup(ran 𝐹, ℝ,
< ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))) |
| 109 | | simprl 771 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → 𝑥 ∈ ℝ) |
| 110 | | max2 13229 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝑥
∈ ℝ) → 𝑥
≤ if(1 ≤ 𝑥, 𝑥, 1)) |
| 111 | 91, 109, 110 | sylancr 587 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → 𝑥 ≤ if(1 ≤ 𝑥, 𝑥, 1)) |
| 112 | 36 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
| 113 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ∧ 𝑦 ∈ 𝑋) → (𝐹‘𝑦) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)})) |
| 114 | 113 | ad2ant2l 746 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (𝐹‘𝑦) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)})) |
| 115 | | eldifsn 4786 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑦) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔
((𝐹‘𝑦) ∈ ℝ ∧ (𝐹‘𝑦) ≠ sup(ran 𝐹, ℝ, < ))) |
| 116 | 114, 115 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → ((𝐹‘𝑦) ∈ ℝ ∧ (𝐹‘𝑦) ≠ sup(ran 𝐹, ℝ, < ))) |
| 117 | 116 | simpld 494 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (𝐹‘𝑦) ∈ ℝ) |
| 118 | 112, 117 | resubcld 11691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)) ∈ ℝ) |
| 119 | | fnfvelrn 7100 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 Fn 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘𝑦) ∈ ran 𝐹) |
| 120 | 28, 119 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹‘𝑦) ∈ ran 𝐹) |
| 121 | | suprub 12229 |
. . . . . . . . . . . . . . . . . 18
⊢ (((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥) ∧ (𝐹‘𝑦) ∈ ran 𝐹) → (𝐹‘𝑦) ≤ sup(ran 𝐹, ℝ, < )) |
| 122 | 34, 120, 121 | syl2an2r 685 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹‘𝑦) ≤ sup(ran 𝐹, ℝ, < )) |
| 123 | 122 | ad2ant2rl 749 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (𝐹‘𝑦) ≤ sup(ran 𝐹, ℝ, < )) |
| 124 | 116 | simprd 495 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (𝐹‘𝑦) ≠ sup(ran 𝐹, ℝ, < )) |
| 125 | 124 | necomd 2996 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → sup(ran 𝐹, ℝ, < ) ≠ (𝐹‘𝑦)) |
| 126 | 117, 112,
123, 125 | leneltd 11415 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (𝐹‘𝑦) < sup(ran 𝐹, ℝ, < )) |
| 127 | 117, 112 | posdifd 11850 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → ((𝐹‘𝑦) < sup(ran 𝐹, ℝ, < ) ↔ 0 < (sup(ran
𝐹, ℝ, < ) −
(𝐹‘𝑦)))) |
| 128 | 126, 127 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → 0 < (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) |
| 129 | 128 | gt0ne0d 11827 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)) ≠ 0) |
| 130 | 118, 129 | rereccld 12094 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ∈ ℝ) |
| 131 | 109, 91, 92 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → if(1 ≤ 𝑥, 𝑥, 1) ∈ ℝ) |
| 132 | | letr 11355 |
. . . . . . . . . . . 12
⊢ (((1 /
(sup(ran 𝐹, ℝ, < )
− (𝐹‘𝑦))) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ if(1 ≤
𝑥, 𝑥, 1) ∈ ℝ) → (((1 / (sup(ran
𝐹, ℝ, < ) −
(𝐹‘𝑦))) ≤ 𝑥 ∧ 𝑥 ≤ if(1 ≤ 𝑥, 𝑥, 1)) → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1))) |
| 133 | 130, 109,
131, 132 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (((1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ 𝑥 ∧ 𝑥 ≤ if(1 ≤ 𝑥, 𝑥, 1)) → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1))) |
| 134 | 111, 133 | mpan2d 694 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → ((1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ 𝑥 → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1))) |
| 135 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑦 → (𝐹‘𝑧) = (𝐹‘𝑦)) |
| 136 | 135 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)) = (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) |
| 137 | 136 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) = (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)))) |
| 138 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) = (𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) |
| 139 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ (1 /
(sup(ran 𝐹, ℝ, < )
− (𝐹‘𝑦))) ∈ V |
| 140 | 137, 138,
139 | fvmpt 7016 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑋 → ((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) = (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)))) |
| 141 | 140 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑋 → (((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥 ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ 𝑥)) |
| 142 | 141 | ad2antll 729 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥 ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ 𝑥)) |
| 143 | 102 | adantrr 717 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (1 / if(1 ≤ 𝑥, 𝑥, 1)) ∈ ℝ) |
| 144 | 100 | adantrr 717 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → 0 < if(1 ≤ 𝑥, 𝑥, 1)) |
| 145 | 131, 144 | recgt0d 12202 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → 0 < (1 / if(1 ≤ 𝑥, 𝑥, 1))) |
| 146 | | lerec 12151 |
. . . . . . . . . . . 12
⊢ ((((1 /
if(1 ≤ 𝑥, 𝑥, 1)) ∈ ℝ ∧ 0
< (1 / if(1 ≤ 𝑥,
𝑥, 1))) ∧ ((sup(ran
𝐹, ℝ, < ) −
(𝐹‘𝑦)) ∈ ℝ ∧ 0 < (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)))) → ((1 / if(1 ≤ 𝑥, 𝑥, 1)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)) ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ (1 / (1 / if(1 ≤ 𝑥, 𝑥, 1))))) |
| 147 | 143, 145,
118, 128, 146 | syl22anc 839 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → ((1 / if(1 ≤ 𝑥, 𝑥, 1)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)) ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ (1 / (1 / if(1 ≤ 𝑥, 𝑥, 1))))) |
| 148 | | lesub 11742 |
. . . . . . . . . . . 12
⊢ (((1 /
if(1 ≤ 𝑥, 𝑥, 1)) ∈ ℝ ∧
sup(ran 𝐹, ℝ, < )
∈ ℝ ∧ (𝐹‘𝑦) ∈ ℝ) → ((1 / if(1 ≤
𝑥, 𝑥, 1)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)) ↔ (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
| 149 | 143, 112,
117, 148 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → ((1 / if(1 ≤ 𝑥, 𝑥, 1)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)) ↔ (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
| 150 | 131 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → if(1 ≤ 𝑥, 𝑥, 1) ∈ ℂ) |
| 151 | 101 | adantrr 717 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → if(1 ≤ 𝑥, 𝑥, 1) ≠ 0) |
| 152 | 150, 151 | recrecd 12040 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (1 / (1 / if(1 ≤ 𝑥, 𝑥, 1))) = if(1 ≤ 𝑥, 𝑥, 1)) |
| 153 | 152 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → ((1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ (1 / (1 / if(1 ≤ 𝑥, 𝑥, 1))) ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1))) |
| 154 | 147, 149,
153 | 3bitr3d 309 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → ((𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))) ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1))) |
| 155 | 134, 142,
154 | 3imtr4d 294 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥 → (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
| 156 | 155 | anassrs 467 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ 𝑋) → (((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥 → (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
| 157 | 156 | ralimdva 3167 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝑋 ((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥 → ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
| 158 | 34 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥)) |
| 159 | | suprleub 12234 |
. . . . . . . . 9
⊢ (((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))) ∈ ℝ) → (sup(ran 𝐹, ℝ, < ) ≤ (sup(ran
𝐹, ℝ, < ) −
(1 / if(1 ≤ 𝑥, 𝑥, 1))) ↔ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
| 160 | 158, 106,
159 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (sup(ran
𝐹, ℝ, < ) ≤
(sup(ran 𝐹, ℝ, < )
− (1 / if(1 ≤ 𝑥,
𝑥, 1))) ↔
∀𝑧 ∈ ran 𝐹 𝑧 ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
| 161 | 28 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn 𝑋) |
| 162 | | breq1 5146 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐹‘𝑦) → (𝑧 ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))) ↔ (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
| 163 | 162 | ralrn 7108 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑋 → (∀𝑧 ∈ ran 𝐹 𝑧 ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))) ↔ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
| 164 | 161, 163 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) →
(∀𝑧 ∈ ran 𝐹 𝑧 ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))) ↔ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
| 165 | 160, 164 | bitrd 279 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (sup(ran
𝐹, ℝ, < ) ≤
(sup(ran 𝐹, ℝ, < )
− (1 / if(1 ≤ 𝑥,
𝑥, 1))) ↔
∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
| 166 | 157, 165 | sylibrd 259 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝑋 ((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥 → sup(ran 𝐹, ℝ, < ) ≤ (sup(ran 𝐹, ℝ, < ) − (1 /
if(1 ≤ 𝑥, 𝑥, 1))))) |
| 167 | 108, 166 | mtod 198 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → ¬
∀𝑦 ∈ 𝑋 ((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥) |
| 168 | 167 | nrexdv 3149 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
¬ ∃𝑥 ∈
ℝ ∀𝑦 ∈
𝑋 ((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥) |
| 169 | 88, 168 | pm2.65da 817 |
. . 3
⊢ (𝜑 → ¬ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, <
)})) |
| 170 | 122 | ralrimiva 3146 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ sup(ran 𝐹, ℝ, < )) |
| 171 | | breq2 5147 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) = sup(ran 𝐹, ℝ, < ) → ((𝐹‘𝑦) ≤ (𝐹‘𝑥) ↔ (𝐹‘𝑦) ≤ sup(ran 𝐹, ℝ, < ))) |
| 172 | 171 | ralbidv 3178 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) = sup(ran 𝐹, ℝ, < ) → (∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥) ↔ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ sup(ran 𝐹, ℝ, < ))) |
| 173 | 170, 172 | syl5ibrcom 247 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝑥) = sup(ran 𝐹, ℝ, < ) → ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥))) |
| 174 | 173 | necon3bd 2954 |
. . . . . . 7
⊢ (𝜑 → (¬ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥) → (𝐹‘𝑥) ≠ sup(ran 𝐹, ℝ, < ))) |
| 175 | 174 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (¬ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥) → (𝐹‘𝑥) ≠ sup(ran 𝐹, ℝ, < ))) |
| 176 | 19 | ffvelcdmda 7104 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ℝ) |
| 177 | | eldifsn 4786 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔
((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) ≠ sup(ran 𝐹, ℝ, < ))) |
| 178 | 177 | baib 535 |
. . . . . . 7
⊢ ((𝐹‘𝑥) ∈ ℝ → ((𝐹‘𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔
(𝐹‘𝑥) ≠ sup(ran 𝐹, ℝ, < ))) |
| 179 | 176, 178 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔
(𝐹‘𝑥) ≠ sup(ran 𝐹, ℝ, < ))) |
| 180 | 175, 179 | sylibrd 259 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (¬ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥) → (𝐹‘𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)}))) |
| 181 | 180 | ralimdva 3167 |
. . . 4
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ¬ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥) → ∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)}))) |
| 182 | | ffnfv 7139 |
. . . . . 6
⊢ (𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔
(𝐹 Fn 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)}))) |
| 183 | 182 | baib 535 |
. . . . 5
⊢ (𝐹 Fn 𝑋 → (𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔
∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)}))) |
| 184 | 28, 183 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔
∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)}))) |
| 185 | 181, 184 | sylibrd 259 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ¬ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥) → 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, <
)}))) |
| 186 | 169, 185 | mtod 198 |
. 2
⊢ (𝜑 → ¬ ∀𝑥 ∈ 𝑋 ¬ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥)) |
| 187 | | dfrex2 3073 |
. 2
⊢
(∃𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥) ↔ ¬ ∀𝑥 ∈ 𝑋 ¬ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥)) |
| 188 | 186, 187 | sylibr 234 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥)) |