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

Theorem evth 23605
 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 484 . . . . 5 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → 𝐽 ∈ Comp)
5 cmptop 22041 . . . . . . . . . 10 (𝐽 ∈ Comp → 𝐽 ∈ Top)
64, 5syl 17 . . . . . . . . 9 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → 𝐽 ∈ Top)
71toptopon 21563 . . . . . . . . 9 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
86, 7sylib 221 . . . . . . . 8 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → 𝐽 ∈ (TopOn‘𝑋))
9 eqid 2798 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
109cnfldtopon 23429 . . . . . . . . . 10 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
1110a1i 11 . . . . . . . . 9 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
12 1cnd 10643 . . . . . . . . 9 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → 1 ∈ ℂ)
138, 11, 12cnmptc 22308 . . . . . . . 8 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ 1) ∈ (𝐽 Cn (TopOpen‘ℂfld)))
14 bndth.4 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
15 uniretop 23409 . . . . . . . . . . . . . . . . . . 19 ℝ = (topGen‘ran (,))
162unieqi 4817 . . . . . . . . . . . . . . . . . . 19 𝐾 = (topGen‘ran (,))
1715, 16eqtr4i 2824 . . . . . . . . . . . . . . . . . 18 ℝ = 𝐾
181, 17cnf 21892 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶ℝ)
1914, 18syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑋⟶ℝ)
2019frnd 6502 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝐹 ⊆ ℝ)
2119fdmd 6505 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐹 = 𝑋)
22 evth.5 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ≠ ∅)
2321, 22eqnetrd 3054 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐹 ≠ ∅)
24 dm0rn0 5765 . . . . . . . . . . . . . . . . 17 (dom 𝐹 = ∅ ↔ ran 𝐹 = ∅)
2524necon3bii 3039 . . . . . . . . . . . . . . . 16 (dom 𝐹 ≠ ∅ ↔ ran 𝐹 ≠ ∅)
2623, 25sylib 221 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝐹 ≠ ∅)
271, 2, 3, 14bndth 23604 . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥)
2819ffnd 6496 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 Fn 𝑋)
29 breq1 5037 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝐹𝑦) → (𝑧𝑥 ↔ (𝐹𝑦) ≤ 𝑥))
3029ralrn 6841 . . . . . . . . . . . . . . . . . 18 (𝐹 Fn 𝑋 → (∀𝑧 ∈ ran 𝐹 𝑧𝑥 ↔ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
3128, 30syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (∀𝑧 ∈ ran 𝐹 𝑧𝑥 ↔ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
3231rexbidv 3257 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
3327, 32mpbird 260 . . . . . . . . . . . . . . 15 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧𝑥)
3420, 26, 333jca 1125 . . . . . . . . . . . . . 14 (𝜑 → (ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧𝑥))
35 suprcl 11606 . . . . . . . . . . . . . 14 ((ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧𝑥) → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
3634, 35syl 17 . . . . . . . . . . . . 13 (𝜑 → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
3736recnd 10676 . . . . . . . . . . . 12 (𝜑 → sup(ran 𝐹, ℝ, < ) ∈ ℂ)
3837adantr 484 . . . . . . . . . . 11 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → sup(ran 𝐹, ℝ, < ) ∈ ℂ)
398, 11, 38cnmptc 22308 . . . . . . . . . 10 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ sup(ran 𝐹, ℝ, < )) ∈ (𝐽 Cn (TopOpen‘ℂfld)))
4019feqmptd 6718 . . . . . . . . . . . 12 (𝜑𝐹 = (𝑧𝑋 ↦ (𝐹𝑧)))
419cnfldtop 23430 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ Top
42 cnrest2r 21933 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ∈ Top → (𝐽 Cn ((TopOpen‘ℂfld) ↾t ℝ)) ⊆ (𝐽 Cn (TopOpen‘ℂfld)))
4341, 42ax-mp 5 . . . . . . . . . . . . 13 (𝐽 Cn ((TopOpen‘ℂfld) ↾t ℝ)) ⊆ (𝐽 Cn (TopOpen‘ℂfld))
449tgioo2 23449 . . . . . . . . . . . . . . . 16 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
452, 44eqtri 2821 . . . . . . . . . . . . . . 15 𝐾 = ((TopOpen‘ℂfld) ↾t ℝ)
4645oveq2i 7156 . . . . . . . . . . . . . 14 (𝐽 Cn 𝐾) = (𝐽 Cn ((TopOpen‘ℂfld) ↾t ℝ))
4714, 46eleqtrdi 2900 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ (𝐽 Cn ((TopOpen‘ℂfld) ↾t ℝ)))
4843, 47sseldi 3915 . . . . . . . . . . . 12 (𝜑𝐹 ∈ (𝐽 Cn (TopOpen‘ℂfld)))
4940, 48eqeltrrd 2891 . . . . . . . . . . 11 (𝜑 → (𝑧𝑋 ↦ (𝐹𝑧)) ∈ (𝐽 Cn (TopOpen‘ℂfld)))
5049adantr 484 . . . . . . . . . 10 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ (𝐹𝑧)) ∈ (𝐽 Cn (TopOpen‘ℂfld)))
519subcn 23512 . . . . . . . . . . 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 22312 . . . . . . . . 9 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) ∈ (𝐽 Cn (TopOpen‘ℂfld)))
5436ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
55 ffvelrn 6836 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ∧ 𝑧𝑋) → (𝐹𝑧) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}))
5655adantll 713 . . . . . . . . . . . . . . . . 17 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (𝐹𝑧) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}))
57 eldifsn 4683 . . . . . . . . . . . . . . . . 17 ((𝐹𝑧) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔ ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝑧) ≠ sup(ran 𝐹, ℝ, < )))
5856, 57sylib 221 . . . . . . . . . . . . . . . 16 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝑧) ≠ sup(ran 𝐹, ℝ, < )))
5958simpld 498 . . . . . . . . . . . . . . 15 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (𝐹𝑧) ∈ ℝ)
6054, 59resubcld 11075 . . . . . . . . . . . . . 14 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)) ∈ ℝ)
6160recnd 10676 . . . . . . . . . . . . 13 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)) ∈ ℂ)
6254recnd 10676 . . . . . . . . . . . . . 14 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → sup(ran 𝐹, ℝ, < ) ∈ ℂ)
6359recnd 10676 . . . . . . . . . . . . . 14 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (𝐹𝑧) ∈ ℂ)
6458simprd 499 . . . . . . . . . . . . . . 15 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (𝐹𝑧) ≠ sup(ran 𝐹, ℝ, < ))
6564necomd 3042 . . . . . . . . . . . . . 14 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → sup(ran 𝐹, ℝ, < ) ≠ (𝐹𝑧))
6662, 63, 65subne0d 11013 . . . . . . . . . . . . 13 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)) ≠ 0)
67 eldifsn 4683 . . . . . . . . . . . . 13 ((sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)) ∈ (ℂ ∖ {0}) ↔ ((sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)) ∈ ℂ ∧ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)) ≠ 0))
6861, 66, 67sylanbrc 586 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)) ∈ (ℂ ∖ {0}))
6968fmpttd 6866 . . . . . . . . . . 11 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))):𝑋⟶(ℂ ∖ {0}))
7069frnd 6502 . . . . . . . . . 10 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ran (𝑧𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) ⊆ (ℂ ∖ {0}))
71 difssd 4063 . . . . . . . . . 10 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (ℂ ∖ {0}) ⊆ ℂ)
72 cnrest2 21932 . . . . . . . . . 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 1368 . . . . . . . . 9 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ((𝑧𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) ∈ (𝐽 Cn (TopOpen‘ℂfld)) ↔ (𝑧𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) ∈ (𝐽 Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})))))
7453, 73mpbid 235 . . . . . . . 8 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) ∈ (𝐽 Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))))
75 eqid 2798 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0})) = ((TopOpen‘ℂfld) ↾t (ℂ ∖ {0}))
769, 75divcn 23514 . . . . . . . . 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 22312 . . . . . . 7 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) ∈ (𝐽 Cn (TopOpen‘ℂfld)))
7960, 66rereccld 11474 . . . . . . . . . 10 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧𝑋) → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) ∈ ℝ)
8079fmpttd 6866 . . . . . . . . 9 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))):𝑋⟶ℝ)
8180frnd 6502 . . . . . . . 8 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ran (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) ⊆ ℝ)
82 ax-resscn 10601 . . . . . . . . 9 ℝ ⊆ ℂ
8382a1i 11 . . . . . . . 8 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ℝ ⊆ ℂ)
84 cnrest2 21932 . . . . . . . 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 1368 . . . . . . 7 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) ∈ (𝐽 Cn (TopOpen‘ℂfld)) ↔ (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) ∈ (𝐽 Cn ((TopOpen‘ℂfld) ↾t ℝ))))
8678, 85mpbid 235 . . . . . 6 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) ∈ (𝐽 Cn ((TopOpen‘ℂfld) ↾t ℝ)))
8786, 46eleqtrrdi 2901 . . . . 5 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) ∈ (𝐽 Cn 𝐾))
881, 2, 4, 87bndth 23604 . . . 4 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ∃𝑥 ∈ ℝ ∀𝑦𝑋 ((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥)
8936ad2antrr 725 . . . . . . . 8 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
90 simpr 488 . . . . . . . . . . 11 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
91 1re 10648 . . . . . . . . . . 11 1 ∈ ℝ
92 ifcl 4472 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → if(1 ≤ 𝑥, 𝑥, 1) ∈ ℝ)
9390, 91, 92sylancl 589 . . . . . . . . . 10 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → if(1 ≤ 𝑥, 𝑥, 1) ∈ ℝ)
94 0red 10651 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
9591a1i 11 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
96 0lt1 11169 . . . . . . . . . . . . 13 0 < 1
9796a1i 11 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 0 < 1)
98 max1 12586 . . . . . . . . . . . . 13 ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → 1 ≤ if(1 ≤ 𝑥, 𝑥, 1))
9991, 90, 98sylancr 590 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 1 ≤ if(1 ≤ 𝑥, 𝑥, 1))
10094, 95, 93, 97, 99ltletrd 10807 . . . . . . . . . . 11 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 0 < if(1 ≤ 𝑥, 𝑥, 1))
101100gt0ne0d 11211 . . . . . . . . . 10 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → if(1 ≤ 𝑥, 𝑥, 1) ≠ 0)
10293, 101rereccld 11474 . . . . . . . . 9 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (1 / if(1 ≤ 𝑥, 𝑥, 1)) ∈ ℝ)
10393, 100recgt0d 11581 . . . . . . . . 9 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 0 < (1 / if(1 ≤ 𝑥, 𝑥, 1)))
104102, 103elrpd 12436 . . . . . . . 8 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (1 / if(1 ≤ 𝑥, 𝑥, 1)) ∈ ℝ+)
10589, 104ltsubrpd 12471 . . . . . . 7 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))) < sup(ran 𝐹, ℝ, < ))
10689, 102resubcld 11075 . . . . . . . 8 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))) ∈ ℝ)
107106, 89ltnled 10794 . . . . . . 7 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → ((sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))) < sup(ran 𝐹, ℝ, < ) ↔ ¬ sup(ran 𝐹, ℝ, < ) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
108105, 107mpbid 235 . . . . . 6 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → ¬ sup(ran 𝐹, ℝ, < ) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))))
109 simprl 770 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → 𝑥 ∈ ℝ)
110 max2 12588 . . . . . . . . . . . 12 ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → 𝑥 ≤ if(1 ≤ 𝑥, 𝑥, 1))
11191, 109, 110sylancr 590 . . . . . . . . . . 11 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → 𝑥 ≤ if(1 ≤ 𝑥, 𝑥, 1))
11236ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → sup(ran 𝐹, ℝ, < ) ∈ ℝ)
113 ffvelrn 6836 . . . . . . . . . . . . . . . . 17 ((𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ∧ 𝑦𝑋) → (𝐹𝑦) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}))
114113ad2ant2l 745 . . . . . . . . . . . . . . . 16 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (𝐹𝑦) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}))
115 eldifsn 4683 . . . . . . . . . . . . . . . 16 ((𝐹𝑦) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔ ((𝐹𝑦) ∈ ℝ ∧ (𝐹𝑦) ≠ sup(ran 𝐹, ℝ, < )))
116114, 115sylib 221 . . . . . . . . . . . . . . 15 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → ((𝐹𝑦) ∈ ℝ ∧ (𝐹𝑦) ≠ sup(ran 𝐹, ℝ, < )))
117116simpld 498 . . . . . . . . . . . . . 14 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (𝐹𝑦) ∈ ℝ)
118112, 117resubcld 11075 . . . . . . . . . . . . 13 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦)) ∈ ℝ)
119 fnfvelrn 6835 . . . . . . . . . . . . . . . . . . 19 ((𝐹 Fn 𝑋𝑦𝑋) → (𝐹𝑦) ∈ ran 𝐹)
12028, 119sylan 583 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑋) → (𝐹𝑦) ∈ ran 𝐹)
121 suprub 11607 . . . . . . . . . . . . . . . . . 18 (((ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧𝑥) ∧ (𝐹𝑦) ∈ ran 𝐹) → (𝐹𝑦) ≤ sup(ran 𝐹, ℝ, < ))
12234, 120, 121syl2an2r 684 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑋) → (𝐹𝑦) ≤ sup(ran 𝐹, ℝ, < ))
123122ad2ant2rl 748 . . . . . . . . . . . . . . . 16 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (𝐹𝑦) ≤ sup(ran 𝐹, ℝ, < ))
124116simprd 499 . . . . . . . . . . . . . . . . 17 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (𝐹𝑦) ≠ sup(ran 𝐹, ℝ, < ))
125124necomd 3042 . . . . . . . . . . . . . . . 16 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → sup(ran 𝐹, ℝ, < ) ≠ (𝐹𝑦))
126117, 112, 123, 125leneltd 10801 . . . . . . . . . . . . . . 15 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (𝐹𝑦) < sup(ran 𝐹, ℝ, < ))
127117, 112posdifd 11234 . . . . . . . . . . . . . . 15 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → ((𝐹𝑦) < sup(ran 𝐹, ℝ, < ) ↔ 0 < (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))))
128126, 127mpbid 235 . . . . . . . . . . . . . 14 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → 0 < (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦)))
129128gt0ne0d 11211 . . . . . . . . . . . . 13 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦)) ≠ 0)
130118, 129rereccld 11474 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ∈ ℝ)
131109, 91, 92sylancl 589 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → if(1 ≤ 𝑥, 𝑥, 1) ∈ ℝ)
132 letr 10741 . . . . . . . . . . . 12 (((1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ if(1 ≤ 𝑥, 𝑥, 1) ∈ ℝ) → (((1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ 𝑥𝑥 ≤ if(1 ≤ 𝑥, 𝑥, 1)) → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1)))
133130, 109, 131, 132syl3anc 1368 . . . . . . . . . . 11 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (((1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ 𝑥𝑥 ≤ if(1 ≤ 𝑥, 𝑥, 1)) → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1)))
134111, 133mpan2d 693 . . . . . . . . . 10 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → ((1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ 𝑥 → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1)))
135 fveq2 6655 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → (𝐹𝑧) = (𝐹𝑦))
136135oveq2d 7161 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)) = (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦)))
137136oveq2d 7161 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))) = (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))))
138 eqid 2798 . . . . . . . . . . . . 13 (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧)))) = (𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))
139 ovex 7178 . . . . . . . . . . . . 13 (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ∈ V
140137, 138, 139fvmpt 6755 . . . . . . . . . . . 12 (𝑦𝑋 → ((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) = (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))))
141140breq1d 5044 . . . . . . . . . . 11 (𝑦𝑋 → (((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥 ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ 𝑥))
142141ad2antll 728 . . . . . . . . . 10 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥 ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ 𝑥))
143102adantrr 716 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (1 / if(1 ≤ 𝑥, 𝑥, 1)) ∈ ℝ)
144100adantrr 716 . . . . . . . . . . . . 13 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → 0 < if(1 ≤ 𝑥, 𝑥, 1))
145131, 144recgt0d 11581 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → 0 < (1 / if(1 ≤ 𝑥, 𝑥, 1)))
146 lerec 11530 . . . . . . . . . . . 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 11126 . . . . . . . . . . . 12 (((1 / if(1 ≤ 𝑥, 𝑥, 1)) ∈ ℝ ∧ sup(ran 𝐹, ℝ, < ) ∈ ℝ ∧ (𝐹𝑦) ∈ ℝ) → ((1 / if(1 ≤ 𝑥, 𝑥, 1)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦)) ↔ (𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
149143, 112, 117, 148syl3anc 1368 . . . . . . . . . . 11 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → ((1 / if(1 ≤ 𝑥, 𝑥, 1)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦)) ↔ (𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
150131recnd 10676 . . . . . . . . . . . . 13 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → if(1 ≤ 𝑥, 𝑥, 1) ∈ ℂ)
151101adantrr 716 . . . . . . . . . . . . 13 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → if(1 ≤ 𝑥, 𝑥, 1) ≠ 0)
152150, 151recrecd 11420 . . . . . . . . . . . 12 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (1 / (1 / if(1 ≤ 𝑥, 𝑥, 1))) = if(1 ≤ 𝑥, 𝑥, 1))
153152breq2d 5046 . . . . . . . . . . 11 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → ((1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ (1 / (1 / if(1 ≤ 𝑥, 𝑥, 1))) ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1)))
154147, 149, 1533bitr3d 312 . . . . . . . . . 10 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → ((𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))) ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1)))
155134, 142, 1543imtr4d 297 . . . . . . . . 9 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ (𝑥 ∈ ℝ ∧ 𝑦𝑋)) → (((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥 → (𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
156155anassrs 471 . . . . . . . 8 ((((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) ∧ 𝑦𝑋) → (((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥 → (𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
157156ralimdva 3144 . . . . . . 7 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (∀𝑦𝑋 ((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥 → ∀𝑦𝑋 (𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
15834ad2antrr 725 . . . . . . . . 9 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧𝑥))
159 suprleub 11612 . . . . . . . . 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 587 . . . . . . . 8 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (sup(ran 𝐹, ℝ, < ) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))) ↔ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
16128ad2antrr 725 . . . . . . . . 9 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn 𝑋)
162 breq1 5037 . . . . . . . . . 10 (𝑧 = (𝐹𝑦) → (𝑧 ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))) ↔ (𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
163162ralrn 6841 . . . . . . . . 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 282 . . . . . . 7 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (sup(ran 𝐹, ℝ, < ) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))) ↔ ∀𝑦𝑋 (𝐹𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
166157, 165sylibrd 262 . . . . . 6 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (∀𝑦𝑋 ((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥 → sup(ran 𝐹, ℝ, < ) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))))
167108, 166mtod 201 . . . . 5 (((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → ¬ ∀𝑦𝑋 ((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥)
168167nrexdv 3230 . . . 4 ((𝜑𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ¬ ∃𝑥 ∈ ℝ ∀𝑦𝑋 ((𝑧𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹𝑧))))‘𝑦) ≤ 𝑥)
16988, 168pm2.65da 816 . . 3 (𝜑 → ¬ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}))
170122ralrimiva 3149 . . . . . . . . 9 (𝜑 → ∀𝑦𝑋 (𝐹𝑦) ≤ sup(ran 𝐹, ℝ, < ))
171 breq2 5038 . . . . . . . . . 10 ((𝐹𝑥) = sup(ran 𝐹, ℝ, < ) → ((𝐹𝑦) ≤ (𝐹𝑥) ↔ (𝐹𝑦) ≤ sup(ran 𝐹, ℝ, < )))
172171ralbidv 3162 . . . . . . . . 9 ((𝐹𝑥) = sup(ran 𝐹, ℝ, < ) → (∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥) ↔ ∀𝑦𝑋 (𝐹𝑦) ≤ sup(ran 𝐹, ℝ, < )))
173170, 172syl5ibrcom 250 . . . . . . . 8 (𝜑 → ((𝐹𝑥) = sup(ran 𝐹, ℝ, < ) → ∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥)))
174173necon3bd 3001 . . . . . . 7 (𝜑 → (¬ ∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥) → (𝐹𝑥) ≠ sup(ran 𝐹, ℝ, < )))
175174adantr 484 . . . . . 6 ((𝜑𝑥𝑋) → (¬ ∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥) → (𝐹𝑥) ≠ sup(ran 𝐹, ℝ, < )))
17619ffvelrnda 6838 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐹𝑥) ∈ ℝ)
177 eldifsn 4683 . . . . . . . 8 ((𝐹𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) ≠ sup(ran 𝐹, ℝ, < )))
178177baib 539 . . . . . . 7 ((𝐹𝑥) ∈ ℝ → ((𝐹𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔ (𝐹𝑥) ≠ sup(ran 𝐹, ℝ, < )))
179176, 178syl 17 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐹𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔ (𝐹𝑥) ≠ sup(ran 𝐹, ℝ, < )))
180175, 179sylibrd 262 . . . . 5 ((𝜑𝑥𝑋) → (¬ ∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥) → (𝐹𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )})))
181180ralimdva 3144 . . . 4 (𝜑 → (∀𝑥𝑋 ¬ ∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥) → ∀𝑥𝑋 (𝐹𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )})))
182 ffnfv 6869 . . . . . 6 (𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔ (𝐹 Fn 𝑋 ∧ ∀𝑥𝑋 (𝐹𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )})))
183182baib 539 . . . . 5 (𝐹 Fn 𝑋 → (𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔ ∀𝑥𝑋 (𝐹𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )})))
18428, 183syl 17 . . . 4 (𝜑 → (𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔ ∀𝑥𝑋 (𝐹𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )})))
185181, 184sylibrd 262 . . 3 (𝜑 → (∀𝑥𝑋 ¬ ∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥) → 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})))
186169, 185mtod 201 . 2 (𝜑 → ¬ ∀𝑥𝑋 ¬ ∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥))
187 dfrex2 3202 . 2 (∃𝑥𝑋𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥) ↔ ¬ ∀𝑥𝑋 ¬ ∀𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥))
188186, 187sylibr 237 1 (𝜑 → ∃𝑥𝑋𝑦𝑋 (𝐹𝑦) ≤ (𝐹𝑥))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107   ∖ cdif 3880   ⊆ wss 3883  ∅c0 4246  ifcif 4428  {csn 4528  ∪ cuni 4804   class class class wbr 5034   ↦ cmpt 5114  dom cdm 5523  ran crn 5524   Fn wfn 6327  ⟶wf 6328  ‘cfv 6332  (class class class)co 7145  supcsup 8906  ℂcc 10542  ℝcr 10543  0cc0 10544  1c1 10545   < clt 10682   ≤ cle 10683   − cmin 10877   / cdiv 11304  (,)cioo 12746   ↾t crest 16706  TopOpenctopn 16707  topGenctg 16723  ℂfldccnfld 20112  Topctop 21539  TopOnctopon 21556   Cn ccn 21870  Compccmp 22032   ×t ctx 22206 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454  ax-cnex 10600  ax-resscn 10601  ax-1cn 10602  ax-icn 10603  ax-addcl 10604  ax-addrcl 10605  ax-mulcl 10606  ax-mulrcl 10607  ax-mulcom 10608  ax-addass 10609  ax-mulass 10610  ax-distr 10611  ax-i2m1 10612  ax-1ne0 10613  ax-1rid 10614  ax-rnegex 10615  ax-rrecex 10616  ax-cnre 10617  ax-pre-lttri 10618  ax-pre-lttrn 10619  ax-pre-ltadd 10620  ax-pre-mulgt0 10621  ax-pre-sup 10622  ax-mulf 10624 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-iin 4888  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-isom 6341  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7400  df-om 7574  df-1st 7684  df-2nd 7685  df-supp 7827  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-1o 8103  df-2o 8104  df-oadd 8107  df-er 8290  df-map 8409  df-ixp 8463  df-en 8511  df-dom 8512  df-sdom 8513  df-fin 8514  df-fsupp 8836  df-fi 8877  df-sup 8908  df-inf 8909  df-oi 8976  df-card 9370  df-pnf 10684  df-mnf 10685  df-xr 10686  df-ltxr 10687  df-le 10688  df-sub 10879  df-neg 10880  df-div 11305  df-nn 11644  df-2 11706  df-3 11707  df-4 11708  df-5 11709  df-6 11710  df-7 11711  df-8 11712  df-9 11713  df-n0 11904  df-z 11990  df-dec 12107  df-uz 12252  df-q 12357  df-rp 12398  df-xneg 12515  df-xadd 12516  df-xmul 12517  df-ioo 12750  df-icc 12753  df-fz 12906  df-fzo 13049  df-seq 13385  df-exp 13446  df-hash 13707  df-cj 14470  df-re 14471  df-im 14472  df-sqrt 14606  df-abs 14607  df-struct 16497  df-ndx 16498  df-slot 16499  df-base 16501  df-sets 16502  df-ress 16503  df-plusg 16590  df-mulr 16591  df-starv 16592  df-sca 16593  df-vsca 16594  df-ip 16595  df-tset 16596  df-ple 16597  df-ds 16599  df-unif 16600  df-hom 16601  df-cco 16602  df-rest 16708  df-topn 16709  df-0g 16727  df-gsum 16728  df-topgen 16729  df-pt 16730  df-prds 16733  df-xrs 16787  df-qtop 16792  df-imas 16793  df-xps 16795  df-mre 16869  df-mrc 16870  df-acs 16872  df-mgm 17864  df-sgrp 17913  df-mnd 17924  df-submnd 17969  df-mulg 18238  df-cntz 18460  df-cmn 18921  df-psmet 20104  df-xmet 20105  df-met 20106  df-bl 20107  df-mopn 20108  df-cnfld 20113  df-top 21540  df-topon 21557  df-topsp 21579  df-bases 21592  df-cn 21873  df-cnp 21874  df-cmp 22033  df-tx 22208  df-hmeo 22401  df-xms 22968  df-ms 22969  df-tms 22970 This theorem is referenced by:  evth2  23606  evthicc  24104  evthf  41827  cncmpmax  41832
 Copyright terms: Public domain W3C validator