MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  evth Structured version   Visualization version   GIF version

Theorem evth 24274
Description: The Extreme Value Theorem. A continuous function from a nonempty compact topological space to the reals attains its maximum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014.)
Hypotheses
Ref Expression
bndth.1 𝑋 = 𝐽
bndth.2 𝐾 = (topGen‘ran (,))
bndth.3 (𝜑𝐽 ∈ Comp)
bndth.4 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
evth.5 (𝜑𝑋 ≠ ∅)
Assertion
Ref Expression
evth (𝜑 → ∃𝑥𝑋𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥))
Distinct variable groups:   𝑥,𝑦,𝐹   𝑦,𝐾   𝜑,𝑥,𝑦   𝑥,𝑋,𝑦   𝑥,𝐽,𝑦
Allowed substitution hint:   𝐾(𝑥)

Proof of Theorem evth
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 bndth.1 . . . . 5 𝑋 = 𝐽
2 bndth.2 . . . . 5 𝐾 = (topGen‘ran (,))
3 bndth.3 . . . . . 6 (𝜑𝐽 ∈ Comp)
43adantr 481 . . . . 5 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → 𝐽 ∈ Comp)
5 cmptop 22698 . . . . . . . . . 10 (𝐽 ∈ Comp → 𝐽 ∈ Top)
64, 5syl 17 . . . . . . . . 9 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → 𝐽 ∈ Top)
71toptopon 22218 . . . . . . . . 9 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
86, 7sylib 217 . . . . . . . 8 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → 𝐽 ∈ (TopOn‘𝑋))
9 eqid 2737 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
109cnfldtopon 24098 . . . . . . . . . 10 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
1110a1i 11 . . . . . . . . 9 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
12 1cnd 11108 . . . . . . . . 9 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → 1 ∈ ℂ)
138, 11, 12cnmptc 22965 . . . . . . . 8 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ 1) ∈ (𝐽 Cn (TopOpen‘ℂfld)))
14 bndth.4 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
15 uniretop 24078 . . . . . . . . . . . . . . . . . . 19 ℝ = (topGen‘ran (,))
162unieqi 4876 . . . . . . . . . . . . . . . . . . 19 𝐾 = (topGen‘ran (,))
1715, 16eqtr4i 2768 . . . . . . . . . . . . . . . . . 18 ℝ = 𝐾
181, 17cnf 22549 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶ℝ)
1914, 18syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑋⟶ℝ)
2019frnd 6673 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝐹 ⊆ ℝ)
2119fdmd 6676 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐹 = 𝑋)
22 evth.5 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ≠ ∅)
2321, 22eqnetrd 3009 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐹 ≠ ∅)
24 dm0rn0 5878 . . . . . . . . . . . . . . . . 17 (dom 𝐹 = ∅ ↔ ran 𝐹 = ∅)
2524necon3bii 2994 . . . . . . . . . . . . . . . 16 (dom 𝐹 ≠ ∅ ↔ ran 𝐹 ≠ ∅)
2623, 25sylib 217 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝐹 ≠ ∅)
271, 2, 3, 14bndth 24273 . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥)
2819ffnd 6666 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 Fn 𝑋)
29 breq1 5106 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝐹𝑦) → (𝑧𝑥 ↔ (𝐹𝑦) ≤ 𝑥))
3029ralrn 7034 . . . . . . . . . . . . . . . . . 18 (𝐹 Fn 𝑋 → (∀𝑧 ∈ ran 𝐹 𝑧𝑥 ↔ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
3128, 30syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (∀𝑧 ∈ ran 𝐹 𝑧𝑥 ↔ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
3231rexbidv 3173 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
3327, 32mpbird 256 . . . . . . . . . . . . . . 15 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧𝑥)
3420, 26, 333jca 1128 . . . . . . . . . . . . . 14 (𝜑 → (ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧𝑥))
35 suprcl 12073 . . . . . . . . . . . . . 14 ((ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧𝑥) → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
3634, 35syl 17 . . . . . . . . . . . . 13 (𝜑 → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
3736recnd 11141 . . . . . . . . . . . 12 (𝜑 → sup(ran 𝐹, ℝ, < ) ∈ ℂ)
3837adantr 481 . . . . . . . . . . 11 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → sup(ran 𝐹, ℝ, < ) ∈ ℂ)
398, 11, 38cnmptc 22965 . . . . . . . . . 10 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ sup(ran 𝐹, ℝ, < )) ∈ (𝐽 Cn (TopOpen‘ℂfld)))
4019feqmptd 6907 . . . . . . . . . . . 12 (𝜑𝐹 = (𝑧𝑋 ↦ (𝐹𝑧)))
419cnfldtop 24099 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ Top
42 cnrest2r 22590 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ∈ Top → (𝐽 Cn ((TopOpen‘ℂfld) ↾t ℝ)) ⊆ (𝐽 Cn (TopOpen‘ℂfld)))
4341, 42ax-mp 5 . . . . . . . . . . . . 13 (𝐽 Cn ((TopOpen‘ℂfld) ↾t ℝ)) ⊆ (𝐽 Cn (TopOpen‘ℂfld))
449tgioo2 24118 . . . . . . . . . . . . . . . 16 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
452, 44eqtri 2765 . . . . . . . . . . . . . . 15 𝐾 = ((TopOpen‘ℂfld) ↾t ℝ)
4645oveq2i 7362 . . . . . . . . . . . . . 14 (𝐽 Cn 𝐾) = (𝐽 Cn ((TopOpen‘ℂfld) ↾t ℝ))
4714, 46eleqtrdi 2848 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ (𝐽 Cn ((TopOpen‘ℂfld) ↾t ℝ)))
4843, 47sselid 3940 . . . . . . . . . . . 12 (𝜑𝐹 ∈ (𝐽 Cn (TopOpen‘ℂfld)))
4940, 48eqeltrrd 2839 . . . . . . . . . . 11 (𝜑 → (𝑧𝑋 ↦ (𝐹𝑧)) ∈ (𝐽 Cn (TopOpen‘ℂfld)))
5049adantr 481 . . . . . . . . . 10 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ (𝐹𝑧)) ∈ (𝐽 Cn (TopOpen‘ℂfld)))
519subcn 24181 . . . . . . . . . . 11 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
5251a1i 11 . . . . . . . . . 10 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
538, 39, 50, 52cnmpt12f 22969 . . . . . . . . 9 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) ∈ (𝐽 Cn (TopOpen‘ℂfld)))
5436ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
55 ffvelcdm 7029 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ∧ 𝑧𝑋) → (𝐹𝑧) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}))
5655adantll 712 . . . . . . . . . . . . . . . . 17 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (𝐹𝑧) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}))
57 eldifsn 4745 . . . . . . . . . . . . . . . . 17 ((𝐹𝑧) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔ ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝑧) ≠ sup(ran 𝐹, ℝ, < )))
5856, 57sylib 217 . . . . . . . . . . . . . . . 16 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝑧) ≠ sup(ran 𝐹, ℝ, < )))
5958simpld 495 . . . . . . . . . . . . . . 15 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (𝐹𝑧) ∈ ℝ)
6054, 59resubcld 11541 . . . . . . . . . . . . . 14 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)) ∈ ℝ)
6160recnd 11141 . . . . . . . . . . . . 13 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)) ∈ ℂ)
6254recnd 11141 . . . . . . . . . . . . . 14 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → sup(ran 𝐹, ℝ, < ) ∈ ℂ)
6359recnd 11141 . . . . . . . . . . . . . 14 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (𝐹𝑧) ∈ ℂ)
6458simprd 496 . . . . . . . . . . . . . . 15 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (𝐹𝑧) ≠ sup(ran 𝐹, ℝ, < ))
6564necomd 2997 . . . . . . . . . . . . . 14 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → sup(ran 𝐹, ℝ, < ) ≠ (𝐹𝑧))
6662, 63, 65subne0d 11479 . . . . . . . . . . . . 13 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)) ≠ 0)
67 eldifsn 4745 . . . . . . . . . . . . 13 ((sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)) ∈ (ℂ ∖ {0}) ↔ ((sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)) ∈ ℂ ∧ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)) ≠ 0))
6861, 66, 67sylanbrc 583 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)) ∈ (ℂ ∖ {0}))
6968fmpttd 7059 . . . . . . . . . . 11 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))):𝑋⟶(ℂ ∖ {0}))
7069frnd 6673 . . . . . . . . . 10 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ran (𝑧𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) ⊆ (ℂ ∖ {0}))
71 difssd 4090 . . . . . . . . . 10 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (ℂ ∖ {0}) ⊆ ℂ)
72 cnrest2 22589 . . . . . . . . . 10 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ ran (𝑧𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) ⊆ (ℂ ∖ {0}) ∧ (ℂ ∖ {0}) ⊆ ℂ) → ((𝑧𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) ∈ (𝐽 Cn (TopOpen‘ℂfld)) ↔ (𝑧𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) ∈ (𝐽 Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))))
7311, 70, 71, 72syl3anc 1371 . . . . . . . . 9 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ((𝑧𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) ∈ (𝐽 Cn (TopOpen‘ℂfld)) ↔ (𝑧𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) ∈ (𝐽 Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))))
7453, 73mpbid 231 . . . . . . . 8 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) ∈ (𝐽 Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))))
75 eqid 2737 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) = ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))
769, 75divcn 24183 . . . . . . . . 9 / ∈ (((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) Cn (TopOpen‘ℂfld))
7776a1i 11 . . . . . . . 8 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → / ∈ (((TopOpen‘ℂfld) ×t ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))) Cn (TopOpen‘ℂfld)))
788, 13, 74, 77cnmpt12f 22969 . . . . . . 7 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) ∈ (𝐽 Cn (TopOpen‘ℂfld)))
7960, 66rereccld 11940 . . . . . . . . . 10 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) ∈ ℝ)
8079fmpttd 7059 . . . . . . . . 9 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))):𝑋⟶ℝ)
8180frnd 6673 . . . . . . . 8 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ran (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) ⊆ ℝ)
82 ax-resscn 11066 . . . . . . . . 9 ℝ ⊆ ℂ
8382a1i 11 . . . . . . . 8 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ℝ ⊆ ℂ)
84 cnrest2 22589 . . . . . . . 8 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ ran (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) ⊆ ℝ ∧ ℝ ⊆ ℂ) → ((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) ∈ (𝐽 Cn (TopOpen‘ℂfld)) ↔ (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) ∈ (𝐽 Cn ((TopOpen‘ℂfld) ↾t ℝ))))
8511, 81, 83, 84syl3anc 1371 . . . . . . 7 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) ∈ (𝐽 Cn (TopOpen‘ℂfld)) ↔ (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) ∈ (𝐽 Cn ((TopOpen‘ℂfld) ↾t ℝ))))
8678, 85mpbid 231 . . . . . 6 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) ∈ (𝐽 Cn ((TopOpen‘ℂfld) ↾t ℝ)))
8786, 46eleqtrrdi 2849 . . . . 5 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) ∈ (𝐽 Cn 𝐾))
881, 2, 4, 87bndth 24273 . . . 4 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ∃𝑥 ∈ ℝ ∀𝑦𝑋 ((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥)
8936ad2antrr 724 . . . . . . . 8 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
90 simpr 485 . . . . . . . . . . 11 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
91 1re 11113 . . . . . . . . . . 11 1 ∈ ℝ
92 ifcl 4529 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → if(1 ≤ 𝑥, 𝑥, 1) ∈ ℝ)
9390, 91, 92sylancl 586 . . . . . . . . . 10 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → if(1 ≤ 𝑥, 𝑥, 1) ∈ ℝ)
94 0red 11116 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
9591a1i 11 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
96 0lt1 11635 . . . . . . . . . . . . 13 0 < 1
9796a1i 11 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 0 < 1)
98 max1 13058 . . . . . . . . . . . . 13 ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → 1 ≤ if(1 ≤ 𝑥, 𝑥, 1))
9991, 90, 98sylancr 587 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 1 ≤ if(1 ≤ 𝑥, 𝑥, 1))
10094, 95, 93, 97, 99ltletrd 11273 . . . . . . . . . . 11 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 0 < if(1 ≤ 𝑥, 𝑥, 1))
101100gt0ne0d 11677 . . . . . . . . . 10 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → if(1 ≤ 𝑥, 𝑥, 1) ≠ 0)
10293, 101rereccld 11940 . . . . . . . . 9 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (1 / if(1 ≤ 𝑥, 𝑥, 1)) ∈ ℝ)
10393, 100recgt0d 12047 . . . . . . . . 9 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 0 < (1 / if(1 ≤ 𝑥, 𝑥, 1)))
104102, 103elrpd 12908 . . . . . . . 8 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (1 / if(1 ≤ 𝑥, 𝑥, 1)) ∈ ℝ+)
10589, 104ltsubrpd 12943 . . . . . . 7 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))) < sup(ran 𝐹, ℝ, < ))
10689, 102resubcld 11541 . . . . . . . 8 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))) ∈ ℝ)
107106, 89ltnled 11260 . . . . . . 7 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → ((sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))) < sup(ran 𝐹, ℝ, < ) ↔ ¬ sup(ran 𝐹, ℝ, < ) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
108105, 107mpbid 231 . . . . . 6 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → ¬ sup(ran 𝐹, ℝ, < ) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))))
109 simprl 769 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → 𝑥 ∈ ℝ)
110 max2 13060 . . . . . . . . . . . 12 ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → 𝑥 ≤ if(1 ≤ 𝑥, 𝑥, 1))
11191, 109, 110sylancr 587 . . . . . . . . . . 11 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → 𝑥 ≤ if(1 ≤ 𝑥, 𝑥, 1))
11236ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
113 ffvelcdm 7029 . . . . . . . . . . . . . . . . 17 ((𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ∧ 𝑦𝑋) → (𝐹𝑦) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}))
114113ad2ant2l 744 . . . . . . . . . . . . . . . 16 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (𝐹𝑦) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}))
115 eldifsn 4745 . . . . . . . . . . . . . . . 16 ((𝐹𝑦) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔ ((𝐹𝑦) ∈ ℝ ∧ (𝐹𝑦) ≠ sup(ran 𝐹, ℝ, < )))
116114, 115sylib 217 . . . . . . . . . . . . . . 15 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → ((𝐹𝑦) ∈ ℝ ∧ (𝐹𝑦) ≠ sup(ran 𝐹, ℝ, < )))
117116simpld 495 . . . . . . . . . . . . . 14 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (𝐹𝑦) ∈ ℝ)
118112, 117resubcld 11541 . . . . . . . . . . . . 13 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦)) ∈ ℝ)
119 fnfvelrn 7028 . . . . . . . . . . . . . . . . . . 19 ((𝐹 Fn 𝑋𝑦𝑋) → (𝐹𝑦) ∈ ran 𝐹)
12028, 119sylan 580 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑋) → (𝐹𝑦) ∈ ran 𝐹)
121 suprub 12074 . . . . . . . . . . . . . . . . . 18 (((ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧𝑥) ∧ (𝐹𝑦) ∈ ran 𝐹) → (𝐹𝑦) ≤ sup(ran 𝐹, ℝ, < ))
12234, 120, 121syl2an2r 683 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑋) → (𝐹𝑦) ≤ sup(ran 𝐹, ℝ, < ))
123122ad2ant2rl 747 . . . . . . . . . . . . . . . 16 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (𝐹𝑦) ≤ sup(ran 𝐹, ℝ, < ))
124116simprd 496 . . . . . . . . . . . . . . . . 17 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (𝐹𝑦) ≠ sup(ran 𝐹, ℝ, < ))
125124necomd 2997 . . . . . . . . . . . . . . . 16 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → sup(ran 𝐹, ℝ, < ) ≠ (𝐹𝑦))
126117, 112, 123, 125leneltd 11267 . . . . . . . . . . . . . . 15 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (𝐹𝑦) < sup(ran 𝐹, ℝ, < ))
127117, 112posdifd 11700 . . . . . . . . . . . . . . 15 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → ((𝐹𝑦) < sup(ran 𝐹, ℝ, < ) ↔ 0 < (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))))
128126, 127mpbid 231 . . . . . . . . . . . . . 14 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → 0 < (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦)))
129128gt0ne0d 11677 . . . . . . . . . . . . 13 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦)) ≠ 0)
130118, 129rereccld 11940 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ∈ ℝ)
131109, 91, 92sylancl 586 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → if(1 ≤ 𝑥, 𝑥, 1) ∈ ℝ)
132 letr 11207 . . . . . . . . . . . 12 (((1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ if(1 ≤ 𝑥, 𝑥, 1) ∈ ℝ) → (((1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ 𝑥𝑥 ≤ if(1 ≤ 𝑥, 𝑥, 1)) → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1)))
133130, 109, 131, 132syl3anc 1371 . . . . . . . . . . 11 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (((1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ 𝑥𝑥 ≤ if(1 ≤ 𝑥, 𝑥, 1)) → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1)))
134111, 133mpan2d 692 . . . . . . . . . 10 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → ((1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ 𝑥 → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1)))
135 fveq2 6839 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → (𝐹𝑧) = (𝐹𝑦))
136135oveq2d 7367 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)) = (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦)))
137136oveq2d 7367 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) = (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))))
138 eqid 2737 . . . . . . . . . . . . 13 (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) = (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))
139 ovex 7384 . . . . . . . . . . . . 13 (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ∈ V
140137, 138, 139fvmpt 6945 . . . . . . . . . . . 12 (𝑦𝑋 → ((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) = (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))))
141140breq1d 5113 . . . . . . . . . . 11 (𝑦𝑋 → (((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥 ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ 𝑥))
142141ad2antll 727 . . . . . . . . . 10 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥 ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ 𝑥))
143102adantrr 715 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (1 / if(1 ≤ 𝑥, 𝑥, 1)) ∈ ℝ)
144100adantrr 715 . . . . . . . . . . . . 13 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → 0 < if(1 ≤ 𝑥, 𝑥, 1))
145131, 144recgt0d 12047 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → 0 < (1 / if(1 ≤ 𝑥, 𝑥, 1)))
146 lerec 11996 . . . . . . . . . . . 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)))))
147143, 145, 118, 128, 146syl22anc 837 . . . . . . . . . . 11 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → ((1 / if(1 ≤ 𝑥, 𝑥, 1)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦)) ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ (1 / (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
148 lesub 11592 . . . . . . . . . . . 12 (((1 / if(1 ≤ 𝑥, 𝑥, 1)) ∈ ℝ ∧ sup(ran 𝐹, ℝ, < ) ∈ ℝ ∧ (𝐹𝑦) ∈ ℝ) → ((1 / if(1 ≤ 𝑥, 𝑥, 1)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦)) ↔ (𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
149143, 112, 117, 148syl3anc 1371 . . . . . . . . . . 11 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → ((1 / if(1 ≤ 𝑥, 𝑥, 1)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦)) ↔ (𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
150131recnd 11141 . . . . . . . . . . . . 13 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → if(1 ≤ 𝑥, 𝑥, 1) ∈ ℂ)
151101adantrr 715 . . . . . . . . . . . . 13 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → if(1 ≤ 𝑥, 𝑥, 1) ≠ 0)
152150, 151recrecd 11886 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (1 / (1 / if(1 ≤ 𝑥, 𝑥, 1))) = if(1 ≤ 𝑥, 𝑥, 1))
153152breq2d 5115 . . . . . . . . . . 11 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → ((1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ (1 / (1 / if(1 ≤ 𝑥, 𝑥, 1))) ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1)))
154147, 149, 1533bitr3d 308 . . . . . . . . . 10 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → ((𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))) ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1)))
155134, 142, 1543imtr4d 293 . . . . . . . . 9 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥 → (𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
156155anassrs 468 . . . . . . . 8 ((((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) ∧ 𝑦𝑋) → (((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥 → (𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
157156ralimdva 3162 . . . . . . 7 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (∀𝑦𝑋 ((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥 → ∀𝑦𝑋 (𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
15834ad2antrr 724 . . . . . . . . 9 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧𝑥))
159 suprleub 12079 . . . . . . . . 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)))))
160158, 106, 159syl2anc 584 . . . . . . . 8 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (sup(ran 𝐹, ℝ, < ) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))) ↔ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
16128ad2antrr 724 . . . . . . . . 9 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn 𝑋)
162 breq1 5106 . . . . . . . . . 10 (𝑧 = (𝐹𝑦) → (𝑧 ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))) ↔ (𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
163162ralrn 7034 . . . . . . . . 9 (𝐹 Fn 𝑋 → (∀𝑧 ∈ ran 𝐹 𝑧 ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))) ↔ ∀𝑦𝑋 (𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
164161, 163syl 17 . . . . . . . 8 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran 𝐹 𝑧 ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))) ↔ ∀𝑦𝑋 (𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
165160, 164bitrd 278 . . . . . . 7 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (sup(ran 𝐹, ℝ, < ) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))) ↔ ∀𝑦𝑋 (𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
166157, 165sylibrd 258 . . . . . 6 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (∀𝑦𝑋 ((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥 → sup(ran 𝐹, ℝ, < ) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
167108, 166mtod 197 . . . . 5 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → ¬ ∀𝑦𝑋 ((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥)
168167nrexdv 3144 . . . 4 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ¬ ∃𝑥 ∈ ℝ ∀𝑦𝑋 ((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥)
16988, 168pm2.65da 815 . . 3 (𝜑 → ¬ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}))
170122ralrimiva 3141 . . . . . . . . 9 (𝜑 → ∀𝑦𝑋 (𝐹𝑦) ≤ sup(ran 𝐹, ℝ, < ))
171 breq2 5107 . . . . . . . . . 10 ((𝐹𝑥) = sup(ran 𝐹, ℝ, < ) → ((𝐹𝑦) ≤ (𝐹𝑥) ↔ (𝐹𝑦) ≤ sup(ran 𝐹, ℝ, < )))
172171ralbidv 3172 . . . . . . . . 9 ((𝐹𝑥) = sup(ran 𝐹, ℝ, < ) → (∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥) ↔ ∀𝑦𝑋 (𝐹𝑦) ≤ sup(ran 𝐹, ℝ, < )))
173170, 172syl5ibrcom 246 . . . . . . . 8 (𝜑 → ((𝐹𝑥) = sup(ran 𝐹, ℝ, < ) → ∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥)))
174173necon3bd 2955 . . . . . . 7 (𝜑 → (¬ ∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥) → (𝐹𝑥) ≠ sup(ran 𝐹, ℝ, < )))
175174adantr 481 . . . . . 6 ((𝜑𝑥𝑋) → (¬ ∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥) → (𝐹𝑥) ≠ sup(ran 𝐹, ℝ, < )))
17619ffvelcdmda 7031 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐹𝑥) ∈ ℝ)
177 eldifsn 4745 . . . . . . . 8 ((𝐹𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) ≠ sup(ran 𝐹, ℝ, < )))
178177baib 536 . . . . . . 7 ((𝐹𝑥) ∈ ℝ → ((𝐹𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔ (𝐹𝑥) ≠ sup(ran 𝐹, ℝ, < )))
179176, 178syl 17 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐹𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔ (𝐹𝑥) ≠ sup(ran 𝐹, ℝ, < )))
180175, 179sylibrd 258 . . . . 5 ((𝜑𝑥𝑋) → (¬ ∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥) → (𝐹𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )})))
181180ralimdva 3162 . . . 4 (𝜑 → (∀𝑥𝑋 ¬ ∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥) → ∀𝑥𝑋 (𝐹𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )})))
182 ffnfv 7062 . . . . . 6 (𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔ (𝐹 Fn 𝑋 ∧ ∀𝑥𝑋 (𝐹𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )})))
183182baib 536 . . . . 5 (𝐹 Fn 𝑋 → (𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔ ∀𝑥𝑋 (𝐹𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )})))
18428, 183syl 17 . . . 4 (𝜑 → (𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔ ∀𝑥𝑋 (𝐹𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )})))
185181, 184sylibrd 258 . . 3 (𝜑 → (∀𝑥𝑋 ¬ ∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥) → 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})))
186169, 185mtod 197 . 2 (𝜑 → ¬ ∀𝑥𝑋 ¬ ∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥))
187 dfrex2 3074 . 2 (∃𝑥𝑋𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥) ↔ ¬ ∀𝑥𝑋 ¬ ∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥))
188186, 187sylibr 233 1 (𝜑 → ∃𝑥𝑋𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2941  wral 3062  wrex 3071  cdif 3905  wss 3908  c0 4280  ifcif 4484  {csn 4584   cuni 4863   class class class wbr 5103  cmpt 5186  dom cdm 5631  ran crn 5632   Fn wfn 6488  wf 6489  cfv 6493  (class class class)co 7351  supcsup 9334  cc 11007  cr 11008  0cc0 11009  1c1 11010   < clt 11147  cle 11148  cmin 11343   / cdiv 11770  (,)cioo 13218  t crest 17262  TopOpenctopn 17263  topGenctg 17279  fldccnfld 20749  Topctop 22194  TopOnctopon 22211   Cn ccn 22527  Compccmp 22689   ×t ctx 22863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-pre-sup 11087  ax-mulf 11089
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-iin 4955  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7307  df-ov 7354  df-oprab 7355  df-mpo 7356  df-of 7609  df-om 7795  df-1st 7913  df-2nd 7914  df-supp 8085  df-frecs 8204  df-wrecs 8235  df-recs 8309  df-rdg 8348  df-1o 8404  df-2o 8405  df-er 8606  df-map 8725  df-ixp 8794  df-en 8842  df-dom 8843  df-sdom 8844  df-fin 8845  df-fsupp 9264  df-fi 9305  df-sup 9336  df-inf 9337  df-oi 9404  df-card 9833  df-pnf 11149  df-mnf 11150  df-xr 11151  df-ltxr 11152  df-le 11153  df-sub 11345  df-neg 11346  df-div 11771  df-nn 12112  df-2 12174  df-3 12175  df-4 12176  df-5 12177  df-6 12178  df-7 12179  df-8 12180  df-9 12181  df-n0 12372  df-z 12458  df-dec 12577  df-uz 12722  df-q 12828  df-rp 12870  df-xneg 12987  df-xadd 12988  df-xmul 12989  df-ioo 13222  df-icc 13225  df-fz 13379  df-fzo 13522  df-seq 13861  df-exp 13922  df-hash 14185  df-cj 14944  df-re 14945  df-im 14946  df-sqrt 15080  df-abs 15081  df-struct 16979  df-sets 16996  df-slot 17014  df-ndx 17026  df-base 17044  df-ress 17073  df-plusg 17106  df-mulr 17107  df-starv 17108  df-sca 17109  df-vsca 17110  df-ip 17111  df-tset 17112  df-ple 17113  df-ds 17115  df-unif 17116  df-hom 17117  df-cco 17118  df-rest 17264  df-topn 17265  df-0g 17283  df-gsum 17284  df-topgen 17285  df-pt 17286  df-prds 17289  df-xrs 17344  df-qtop 17349  df-imas 17350  df-xps 17352  df-mre 17426  df-mrc 17427  df-acs 17429  df-mgm 18457  df-sgrp 18506  df-mnd 18517  df-submnd 18562  df-mulg 18832  df-cntz 19056  df-cmn 19523  df-psmet 20741  df-xmet 20742  df-met 20743  df-bl 20744  df-mopn 20745  df-cnfld 20750  df-top 22195  df-topon 22212  df-topsp 22234  df-bases 22248  df-cn 22530  df-cnp 22531  df-cmp 22690  df-tx 22865  df-hmeo 23058  df-xms 23625  df-ms 23626  df-tms 23627
This theorem is referenced by:  evth2  24275  evthicc  24775  evthf  43143  cncmpmax  43148
  Copyright terms: Public domain W3C validator