This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ivthicc

Description: The interval between any two points of a continuous real function is contained in the range of the function. Equivalently, the range of a continuous real function is convex. (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Hypotheses ivthicc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ivthicc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ivthicc.3 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐴 [,] 𝐵 ) )
ivthicc.4 ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐴 [,] 𝐵 ) )
ivthicc.5 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 )
ivthicc.7 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
ivthicc.8 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
Assertion ivthicc ( 𝜑 → ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ⊆ ran 𝐹 )

Proof

Step Hyp Ref Expression
1 ivthicc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 ivthicc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 ivthicc.3 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐴 [,] 𝐵 ) )
4 ivthicc.4 ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐴 [,] 𝐵 ) )
5 ivthicc.5 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 )
6 ivthicc.7 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
7 ivthicc.8 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
8 simpll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → 𝜑 )
9 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑀 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑀 ∈ ℝ ∧ 𝐴 ≤ 𝑀 ∧ 𝑀 ≤ 𝐵 ) ) )
10 1 2 9 syl2anc ⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑀 ∈ ℝ ∧ 𝐴 ≤ 𝑀 ∧ 𝑀 ≤ 𝐵 ) ) )
11 3 10 mpbid ⊢ ( 𝜑 → ( 𝑀 ∈ ℝ ∧ 𝐴 ≤ 𝑀 ∧ 𝑀 ≤ 𝐵 ) )
12 11 simp1d ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
13 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → 𝑀 ∈ ℝ )
14 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑁 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑁 ∈ ℝ ∧ 𝐴 ≤ 𝑁 ∧ 𝑁 ≤ 𝐵 ) ) )
15 1 2 14 syl2anc ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑁 ∈ ℝ ∧ 𝐴 ≤ 𝑁 ∧ 𝑁 ≤ 𝐵 ) ) )
16 4 15 mpbid ⊢ ( 𝜑 → ( 𝑁 ∈ ℝ ∧ 𝐴 ≤ 𝑁 ∧ 𝑁 ≤ 𝐵 ) )
17 16 simp1d ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
18 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → 𝑁 ∈ ℝ )
19 fveq2 ⊢ ( 𝑥 = 𝑀 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑀 ) )
20 19 eleq1d ⊢ ( 𝑥 = 𝑀 → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑀 ) ∈ ℝ ) )
21 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
22 20 21 3 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ℝ )
23 fveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑁 ) )
24 23 eleq1d ⊢ ( 𝑥 = 𝑁 → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑁 ) ∈ ℝ ) )
25 24 21 4 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
26 iccssre ⊢ ( ( ( 𝐹 ‘ 𝑀 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ⊆ ℝ )
27 22 25 26 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ⊆ ℝ )
28 27 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) → 𝑦 ∈ ℝ )
29 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → 𝑦 ∈ ℝ )
30 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → 𝑀 < 𝑁 )
31 11 simp2d ⊢ ( 𝜑 → 𝐴 ≤ 𝑀 )
32 16 simp3d ⊢ ( 𝜑 → 𝑁 ≤ 𝐵 )
33 iccss ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≤ 𝑀 ∧ 𝑁 ≤ 𝐵 ) ) → ( 𝑀 [,] 𝑁 ) ⊆ ( 𝐴 [,] 𝐵 ) )
34 1 2 31 32 33 syl22anc ⊢ ( 𝜑 → ( 𝑀 [,] 𝑁 ) ⊆ ( 𝐴 [,] 𝐵 ) )
35 34 5 sstrd ⊢ ( 𝜑 → ( 𝑀 [,] 𝑁 ) ⊆ 𝐷 )
36 35 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → ( 𝑀 [,] 𝑁 ) ⊆ 𝐷 )
37 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
38 34 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
39 38 7 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
40 8 39 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
41 elicc2 ⊢ ( ( ( 𝐹 ‘ 𝑀 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑁 ) ∈ ℝ ) → ( 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑀 ) ≤ 𝑦 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑁 ) ) ) )
42 22 25 41 syl2anc ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑀 ) ≤ 𝑦 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑁 ) ) ) )
43 42 biimpa ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) → ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑀 ) ≤ 𝑦 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑁 ) ) )
44 3simpc ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑀 ) ≤ 𝑦 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑁 ) ) → ( ( 𝐹 ‘ 𝑀 ) ≤ 𝑦 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑁 ) ) )
45 43 44 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) → ( ( 𝐹 ‘ 𝑀 ) ≤ 𝑦 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑁 ) ) )
46 45 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) ≤ 𝑦 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑁 ) ) )
47 13 18 29 30 36 37 40 46 ivthle ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → ∃ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( 𝐹 ‘ 𝑧 ) = 𝑦 )
48 35 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝑧 ∈ 𝐷 )
49 cncff ⊢ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) → 𝐹 : 𝐷 ⟶ ℂ )
50 ffn ⊢ ( 𝐹 : 𝐷 ⟶ ℂ → 𝐹 Fn 𝐷 )
51 6 49 50 3syl ⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
52 fnfvelrn ⊢ ( ( 𝐹 Fn 𝐷 ∧ 𝑧 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑧 ) ∈ ran 𝐹 )
53 51 52 sylan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑧 ) ∈ ran 𝐹 )
54 eleq1 ⊢ ( ( 𝐹 ‘ 𝑧 ) = 𝑦 → ( ( 𝐹 ‘ 𝑧 ) ∈ ran 𝐹 ↔ 𝑦 ∈ ran 𝐹 ) )
55 53 54 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑧 ) = 𝑦 → 𝑦 ∈ ran 𝐹 ) )
56 48 55 syldan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ( 𝐹 ‘ 𝑧 ) = 𝑦 → 𝑦 ∈ ran 𝐹 ) )
57 56 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( 𝐹 ‘ 𝑧 ) = 𝑦 → 𝑦 ∈ ran 𝐹 ) )
58 8 47 57 sylc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 < 𝑁 ) → 𝑦 ∈ ran 𝐹 )
59 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) )
60 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → 𝑀 = 𝑁 )
61 60 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → ( 𝐹 ‘ 𝑀 ) = ( 𝐹 ‘ 𝑁 ) )
62 61 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑀 ) ) = ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) )
63 22 rexrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ℝ* )
64 63 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ∈ ℝ* )
65 iccid ⊢ ( ( 𝐹 ‘ 𝑀 ) ∈ ℝ* → ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑀 ) ) = { ( 𝐹 ‘ 𝑀 ) } )
66 64 65 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑀 ) ) = { ( 𝐹 ‘ 𝑀 ) } )
67 62 66 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) = { ( 𝐹 ‘ 𝑀 ) } )
68 59 67 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → 𝑦 ∈ { ( 𝐹 ‘ 𝑀 ) } )
69 elsni ⊢ ( 𝑦 ∈ { ( 𝐹 ‘ 𝑀 ) } → 𝑦 = ( 𝐹 ‘ 𝑀 ) )
70 68 69 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → 𝑦 = ( 𝐹 ‘ 𝑀 ) )
71 5 3 sseldd ⊢ ( 𝜑 → 𝑀 ∈ 𝐷 )
72 fnfvelrn ⊢ ( ( 𝐹 Fn 𝐷 ∧ 𝑀 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑀 ) ∈ ran 𝐹 )
73 51 71 72 syl2anc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ran 𝐹 )
74 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → ( 𝐹 ‘ 𝑀 ) ∈ ran 𝐹 )
75 70 74 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑀 = 𝑁 ) → 𝑦 ∈ ran 𝐹 )
76 simpll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → 𝜑 )
77 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → 𝑁 ∈ ℝ )
78 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → 𝑀 ∈ ℝ )
79 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → 𝑦 ∈ ℝ )
80 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → 𝑁 < 𝑀 )
81 16 simp2d ⊢ ( 𝜑 → 𝐴 ≤ 𝑁 )
82 11 simp3d ⊢ ( 𝜑 → 𝑀 ≤ 𝐵 )
83 iccss ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≤ 𝑁 ∧ 𝑀 ≤ 𝐵 ) ) → ( 𝑁 [,] 𝑀 ) ⊆ ( 𝐴 [,] 𝐵 ) )
84 1 2 81 82 83 syl22anc ⊢ ( 𝜑 → ( 𝑁 [,] 𝑀 ) ⊆ ( 𝐴 [,] 𝐵 ) )
85 84 5 sstrd ⊢ ( 𝜑 → ( 𝑁 [,] 𝑀 ) ⊆ 𝐷 )
86 85 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → ( 𝑁 [,] 𝑀 ) ⊆ 𝐷 )
87 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
88 84 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 [,] 𝑀 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
89 88 7 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑁 [,] 𝑀 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
90 76 89 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) ∧ 𝑥 ∈ ( 𝑁 [,] 𝑀 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
91 45 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → ( ( 𝐹 ‘ 𝑀 ) ≤ 𝑦 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑁 ) ) )
92 77 78 79 80 86 87 90 91 ivthle2 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → ∃ 𝑧 ∈ ( 𝑁 [,] 𝑀 ) ( 𝐹 ‘ 𝑧 ) = 𝑦 )
93 85 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑁 [,] 𝑀 ) ) → 𝑧 ∈ 𝐷 )
94 93 55 syldan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑁 [,] 𝑀 ) ) → ( ( 𝐹 ‘ 𝑧 ) = 𝑦 → 𝑦 ∈ ran 𝐹 ) )
95 94 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝑁 [,] 𝑀 ) ( 𝐹 ‘ 𝑧 ) = 𝑦 → 𝑦 ∈ ran 𝐹 ) )
96 76 92 95 sylc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) ∧ 𝑁 < 𝑀 ) → 𝑦 ∈ ran 𝐹 )
97 12 17 lttri4d ⊢ ( 𝜑 → ( 𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀 ) )
98 97 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) → ( 𝑀 < 𝑁 ∨ 𝑀 = 𝑁 ∨ 𝑁 < 𝑀 ) )
99 58 75 96 98 mpjao3dan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ) → 𝑦 ∈ ran 𝐹 )
100 99 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) → 𝑦 ∈ ran 𝐹 ) )
101 100 ssrdv ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑀 ) [,] ( 𝐹 ‘ 𝑁 ) ) ⊆ ran 𝐹 )