Metamath Proof Explorer

Theorem evth

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)

Ref Expression
Hypotheses bndth.1 ⊢ 𝑋 = ∪ 𝐽
bndth.2 ⊢ 𝐾 = ( topGen ‘ ran (,) )
bndth.3 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
bndth.4 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
evth.5 ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
Assertion evth ( 𝜑 → ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 bndth.1 ⊢ 𝑋 = ∪ 𝐽
2 bndth.2 ⊢ 𝐾 = ( topGen ‘ ran (,) )
3 bndth.3 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
4 bndth.4 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
5 evth.5 ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
6 3 adantr ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → 𝐽 ∈ Comp )
7 cmptop ⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
8 6 7 syl ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → 𝐽 ∈ Top )
9 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
10 8 9 sylib ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
11 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
12 11 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
13 12 a1i ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
14 1cnd ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → 1 ∈ ℂ )
15 10 13 14 cnmptc ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ( 𝑧 ∈ 𝑋 ↦ 1 ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) )
16 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
17 2 unieqi ⊢ ∪ 𝐾 = ∪ ( topGen ‘ ran (,) )
18 16 17 eqtr4i ⊢ ℝ = ∪ 𝐾
19 1 18 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝑋 ⟶ ℝ )
20 4 19 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
21 20 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
22 20 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝑋 )
23 22 5 eqnetrd ⊢ ( 𝜑 → dom 𝐹 ≠ ∅ )
24 dm0rn0 ⊢ ( dom 𝐹 = ∅ ↔ ran 𝐹 = ∅ )
25 24 necon3bii ⊢ ( dom 𝐹 ≠ ∅ ↔ ran 𝐹 ≠ ∅ )
26 23 25 sylib ⊢ ( 𝜑 → ran 𝐹 ≠ ∅ )
27 1 2 3 4 bndth ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 )
28 20 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
29 breq1 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑦 ) → ( 𝑧 ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 ) )
30 29 ralrn ⊢ ( 𝐹 Fn 𝑋 → ( ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 ) )
31 28 30 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 ) )
32 31 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 ) )
33 27 32 mpbird ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 )
34 21 26 33 3jca ⊢ ( 𝜑 → ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ) )
35 suprcl ⊢ ( ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )
36 34 35 syl ⊢ ( 𝜑 → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )
37 36 recnd ⊢ ( 𝜑 → sup ( ran 𝐹 , ℝ , < ) ∈ ℂ )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℂ )
39 10 13 38 cnmptc ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ( 𝑧 ∈ 𝑋 ↦ sup ( ran 𝐹 , ℝ , < ) ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) )
40 20 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑧 ) ) )
41 11 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
42 cnrest2r ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ⊆ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) )
43 41 42 ax-mp ⊢ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ⊆ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) )
44 11 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
45 2 44 eqtri ⊢ 𝐾 = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
46 45 oveq2i ⊢ ( 𝐽 Cn 𝐾 ) = ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
47 4 46 eleqtrdi ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) )
48 43 47 sseldi ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) )
49 40 48 eqeltrrd ⊢ ( 𝜑 → ( 𝑧 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) )
50 49 adantr ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) )
51 11 subcn ⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
52 51 a1i ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
53 10 39 50 52 cnmpt12f ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ( 𝑧 ∈ 𝑋 ↦ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) )
54 36 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑧 ∈ 𝑋 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )
55 ffvelrn ⊢ ( ( 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) )
56 55 adantll ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) )
57 eldifsn ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ≠ sup ( ran 𝐹 , ℝ , < ) ) )
58 56 57 sylib ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ≠ sup ( ran 𝐹 , ℝ , < ) ) )
59 58 simpld ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
60 54 59 resubcld ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑧 ∈ 𝑋 ) → ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
61 60 recnd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑧 ∈ 𝑋 ) → ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ∈ ℂ )
62 54 recnd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑧 ∈ 𝑋 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℂ )
63 59 recnd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
64 58 simprd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ≠ sup ( ran 𝐹 , ℝ , < ) )
65 64 necomd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑧 ∈ 𝑋 ) → sup ( ran 𝐹 , ℝ , < ) ≠ ( 𝐹 ‘ 𝑧 ) )
66 62 63 65 subne0d ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑧 ∈ 𝑋 ) → ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ≠ 0 )
67 eldifsn ⊢ ( ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ∈ ℂ ∧ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ≠ 0 ) )
68 61 66 67 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑧 ∈ 𝑋 ) → ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ∈ ( ℂ ∖ { 0 } ) )
69 68 fmpttd ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ( 𝑧 ∈ 𝑋 ↦ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) : 𝑋 ⟶ ( ℂ ∖ { 0 } ) )
70 69 frnd ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ran ( 𝑧 ∈ 𝑋 ↦ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ⊆ ( ℂ ∖ { 0 } ) )
71 difssd ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ( ℂ ∖ { 0 } ) ⊆ ℂ )
72 cnrest2 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑧 ∈ 𝑋 ↦ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ⊆ ( ℂ ∖ { 0 } ) ∧ ( ℂ ∖ { 0 } ) ⊆ ℂ ) → ( ( 𝑧 ∈ 𝑋 ↦ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑧 ∈ 𝑋 ↦ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) ) )
73 13 70 71 72 syl3anc ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ( ( 𝑧 ∈ 𝑋 ↦ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑧 ∈ 𝑋 ↦ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) ) )
74 53 73 mpbid ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ( 𝑧 ∈ 𝑋 ↦ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) )
75 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) )
76 11 75 divcn ⊢ / ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) Cn ( TopOpen ‘ ℂfld ) )
77 76 a1i ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → / ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) Cn ( TopOpen ‘ ℂfld ) ) )
78 10 15 74 77 cnmpt12f ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) )
79 60 66 rereccld ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ∈ ℝ )
80 79 fmpttd ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) : 𝑋 ⟶ ℝ )
81 80 frnd ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ran ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ⊆ ℝ )
82 ax-resscn ⊢ ℝ ⊆ ℂ
83 82 a1i ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ℝ ⊆ ℂ )
84 cnrest2 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ∈ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
85 13 81 83 84 syl3anc ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ( ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ∈ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
86 78 85 mpbid ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ∈ ( 𝐽 Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) )
87 86 46 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ∈ ( 𝐽 Cn 𝐾 ) )
88 1 2 6 87 bndth ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ≤ 𝑥 )
89 36 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )
90 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
91 1re ⊢ 1 ∈ ℝ
92 ifcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ∈ ℝ ) → if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ∈ ℝ )
93 90 91 92 sylancl ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ∈ ℝ )
94 0red ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → 0 ∈ ℝ )
95 91 a1i ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → 1 ∈ ℝ )
96 0lt1 ⊢ 0 < 1
97 96 a1i ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → 0 < 1 )
98 max1 ⊢ ( ( 1 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → 1 ≤ if ( 1 ≤ 𝑥 , 𝑥 , 1 ) )
99 91 90 98 sylancr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → 1 ≤ if ( 1 ≤ 𝑥 , 𝑥 , 1 ) )
100 94 95 93 97 99 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → 0 < if ( 1 ≤ 𝑥 , 𝑥 , 1 ) )
101 100 gt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ≠ 0 )
102 93 101 rereccld ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ∈ ℝ )
103 93 100 recgt0d ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → 0 < ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) )
104 102 103 elrpd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ∈ ℝ+ )
105 89 104 ltsubrpd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) < sup ( ran 𝐹 , ℝ , < ) )
106 89 102 resubcld ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ∈ ℝ )
107 106 89 ltnled ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) < sup ( ran 𝐹 , ℝ , < ) ↔ ¬ sup ( ran 𝐹 , ℝ , < ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ) )
108 105 107 mpbid ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → ¬ sup ( ran 𝐹 , ℝ , < ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) )
109 simprl ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ ℝ )
110 max2 ⊢ ( ( 1 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → 𝑥 ≤ if ( 1 ≤ 𝑥 , 𝑥 , 1 ) )
111 91 109 110 sylancr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ≤ if ( 1 ≤ 𝑥 , 𝑥 , 1 ) )
112 36 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )
113 ffvelrn ⊢ ( ( 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) )
114 113 ad2ant2l ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) )
115 eldifsn ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ↔ ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑦 ) ≠ sup ( ran 𝐹 , ℝ , < ) ) )
116 114 115 sylib ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑦 ) ≠ sup ( ran 𝐹 , ℝ , < ) ) )
117 116 simpld ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
118 112 117 resubcld ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ )
119 fnfvelrn ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) ∈ ran 𝐹 )
120 28 119 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) ∈ ran 𝐹 )
121 suprub ⊢ ( ( ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ ran 𝐹 ) → ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran 𝐹 , ℝ , < ) )
122 34 120 121 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran 𝐹 , ℝ , < ) )
123 122 ad2ant2rl ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran 𝐹 , ℝ , < ) )
124 116 simprd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑦 ) ≠ sup ( ran 𝐹 , ℝ , < ) )
125 124 necomd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → sup ( ran 𝐹 , ℝ , < ) ≠ ( 𝐹 ‘ 𝑦 ) )
126 117 112 123 125 leneltd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑦 ) < sup ( ran 𝐹 , ℝ , < ) )
127 117 112 posdifd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑦 ) < sup ( ran 𝐹 , ℝ , < ) ↔ 0 < ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) )
128 126 127 mpbid ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → 0 < ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) )
129 128 gt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ≠ 0 )
130 118 129 rereccld ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) ∈ ℝ )
131 109 91 92 sylancl ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ∈ ℝ )
132 letr ⊢ ( ( ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ∈ ℝ ) → ( ( ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ 𝑥 ∧ 𝑥 ≤ if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) → ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) )
133 130 109 131 132 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ 𝑥 ∧ 𝑥 ≤ if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) → ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) )
134 111 133 mpan2d ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ 𝑥 → ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) )
135 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )
136 135 oveq2d ⊢ ( 𝑧 = 𝑦 → ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) = ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) )
137 136 oveq2d ⊢ ( 𝑧 = 𝑦 → ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) = ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) )
138 eqid ⊢ ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) )
139 ovex ⊢ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) ∈ V
140 137 138 139 fvmpt ⊢ ( 𝑦 ∈ 𝑋 → ( ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) = ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) )
141 140 breq1d ⊢ ( 𝑦 ∈ 𝑋 → ( ( ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ≤ 𝑥 ↔ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ 𝑥 ) )
142 141 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ≤ 𝑥 ↔ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ 𝑥 ) )
143 102 adantrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ∈ ℝ )
144 100 adantrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → 0 < if ( 1 ≤ 𝑥 , 𝑥 , 1 ) )
145 131 144 recgt0d ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → 0 < ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) )
146 lerec ⊢ ( ( ( ( 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 ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ↔ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ ( 1 / ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ) )
148 lesub ⊢ ( ( ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ∈ ℝ ∧ sup ( ran 𝐹 , ℝ , < ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑦 ) ∈ ℝ ) → ( ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ 𝑦 ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ) )
149 143 112 117 148 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ 𝑦 ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ) )
150 131 recnd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ∈ ℂ )
151 101 adantrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ≠ 0 )
152 150 151 recrecd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( 1 / ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) = if ( 1 ≤ 𝑥 , 𝑥 , 1 ) )
153 152 breq2d ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ ( 1 / ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ↔ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) )
154 147 149 153 3bitr3d ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑦 ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ↔ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑦 ) ) ) ≤ if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) )
155 134 142 154 3imtr4d ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ≤ 𝑥 → ( 𝐹 ‘ 𝑦 ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ) )
156 155 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ≤ 𝑥 → ( 𝐹 ‘ 𝑦 ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ) )
157 156 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ≤ 𝑥 → ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ) )
158 34 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → ( ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ) )
159 suprleub ⊢ ( ( ( 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 ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → ( sup ( ran 𝐹 , ℝ , < ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ↔ ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ) )
161 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → 𝐹 Fn 𝑋 )
162 breq1 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑦 ) → ( 𝑧 ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ↔ ( 𝐹 ‘ 𝑦 ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ) )
163 162 ralrn ⊢ ( 𝐹 Fn 𝑋 → ( ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ) )
164 161 163 syl ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ) )
165 160 164 bitrd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → ( sup ( ran 𝐹 , ℝ , < ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ) )
166 157 165 sylibrd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ≤ 𝑥 → sup ( ran 𝐹 , ℝ , < ) ≤ ( sup ( ran 𝐹 , ℝ , < ) − ( 1 / if ( 1 ≤ 𝑥 , 𝑥 , 1 ) ) ) ) )
167 108 166 mtod ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) ∧ 𝑥 ∈ ℝ ) → ¬ ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ≤ 𝑥 )
168 167 nrexdv ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) → ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( ( 𝑧 ∈ 𝑋 ↦ ( 1 / ( sup ( ran 𝐹 , ℝ , < ) − ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝑦 ) ≤ 𝑥 )
169 88 168 pm2.65da ⊢ ( 𝜑 → ¬ 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) )
170 122 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran 𝐹 , ℝ , < ) )
171 breq2 ⊢ ( ( 𝐹 ‘ 𝑥 ) = sup ( ran 𝐹 , ℝ , < ) → ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran 𝐹 , ℝ , < ) ) )
172 171 ralbidv ⊢ ( ( 𝐹 ‘ 𝑥 ) = sup ( ran 𝐹 , ℝ , < ) → ( ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ sup ( ran 𝐹 , ℝ , < ) ) )
173 170 172 syl5ibrcom ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑥 ) = sup ( ran 𝐹 , ℝ , < ) → ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
174 173 necon3bd ⊢ ( 𝜑 → ( ¬ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) ≠ sup ( ran 𝐹 , ℝ , < ) ) )
175 174 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ¬ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) ≠ sup ( ran 𝐹 , ℝ , < ) ) )
176 20 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
177 eldifsn ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ≠ sup ( ran 𝐹 , ℝ , < ) ) )
178 177 baib ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ → ( ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ↔ ( 𝐹 ‘ 𝑥 ) ≠ sup ( ran 𝐹 , ℝ , < ) ) )
179 176 178 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ↔ ( 𝐹 ‘ 𝑥 ) ≠ sup ( ran 𝐹 , ℝ , < ) ) )
180 175 179 sylibrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ¬ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) )
181 180 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ¬ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) )
182 ffnfv ⊢ ( 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ↔ ( 𝐹 Fn 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) )
183 182 baib ⊢ ( 𝐹 Fn 𝑋 → ( 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ↔ ∀ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) )
184 28 183 syl ⊢ ( 𝜑 → ( 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ↔ ∀ 𝑥 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ∈ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) )
185 181 184 sylibrd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ¬ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) → 𝐹 : 𝑋 ⟶ ( ℝ ∖ { sup ( ran 𝐹 , ℝ , < ) } ) ) )
186 169 185 mtod ⊢ ( 𝜑 → ¬ ∀ 𝑥 ∈ 𝑋 ¬ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) )
187 dfrex2 ⊢ ( ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ 𝑋 ¬ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) )
188 186 187 sylibr ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) )