Metamath Proof Explorer

Theorem evthicc2

Description: Combine ivthicc with evthicc to exactly describe the image of a closed interval. (Contributed by Mario Carneiro, 19-Feb-2015)

Ref Expression
Hypotheses evthicc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
evthicc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
evthicc.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
evthicc.4 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
Assertion evthicc2 ( 𝜑 → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ran 𝐹 = ( 𝑥 [,] 𝑦 ) )

Proof

Step Hyp Ref Expression
1 evthicc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 evthicc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 evthicc.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4 evthicc.4 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
5 1 2 3 4 evthicc ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ∃ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) )
6 reeanv ⊢ ( ∃ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∃ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ↔ ( ∃ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ∃ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) )
7 5 6 sylibr ⊢ ( 𝜑 → ∃ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∃ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) )
8 r19.26 ⊢ ( ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ↔ ( ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) )
9 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
10 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
11 9 10 syl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
12 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑏 ∈ ( 𝐴 [,] 𝐵 ) )
13 11 12 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ℝ )
14 13 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ℝ )
15 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑎 ∈ ( 𝐴 [,] 𝐵 ) )
16 11 15 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ℝ )
17 16 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ℝ )
18 11 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
19 18 ffnd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) → 𝐹 Fn ( 𝐴 [,] 𝐵 ) )
20 16 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ℝ )
21 elicc2 ⊢ ( ( ( 𝐹 ‘ 𝑏 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑎 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑏 ) [,] ( 𝐹 ‘ 𝑎 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ) ) )
22 13 20 21 syl2an2r ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑏 ) [,] ( 𝐹 ‘ 𝑎 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ) ) )
23 3anass ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ) ) )
24 22 23 bitrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑏 ) [,] ( 𝐹 ‘ 𝑎 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ) ) ) )
25 ancom ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ↔ ( ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ) )
26 11 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
27 26 biantrurd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ) ) ) )
28 25 27 bitrid ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ) ) ) )
29 24 28 bitr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑏 ) [,] ( 𝐹 ‘ 𝑎 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) )
30 29 ralbidva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑏 ) [,] ( 𝐹 ‘ 𝑎 ) ) ↔ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) )
31 30 biimpar ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) → ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑏 ) [,] ( 𝐹 ‘ 𝑎 ) ) )
32 ffnfv ⊢ ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ( ( 𝐹 ‘ 𝑏 ) [,] ( 𝐹 ‘ 𝑎 ) ) ↔ ( 𝐹 Fn ( 𝐴 [,] 𝐵 ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝐹 ‘ 𝑏 ) [,] ( 𝐹 ‘ 𝑎 ) ) ) )
33 19 31 32 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ( ( 𝐹 ‘ 𝑏 ) [,] ( 𝐹 ‘ 𝑎 ) ) )
34 33 frnd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) → ran 𝐹 ⊆ ( ( 𝐹 ‘ 𝑏 ) [,] ( 𝐹 ‘ 𝑎 ) ) )
35 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝐴 ∈ ℝ )
36 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝐵 ∈ ℝ )
37 ssidd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
38 ax-resscn ⊢ ℝ ⊆ ℂ
39 ssid ⊢ ℂ ⊆ ℂ
40 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ⊆ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
41 38 39 40 mp2an ⊢ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ⊆ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ )
42 41 9 sselid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
43 11 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
44 35 36 12 15 37 42 43 ivthicc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝐹 ‘ 𝑏 ) [,] ( 𝐹 ‘ 𝑎 ) ) ⊆ ran 𝐹 )
45 44 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) → ( ( 𝐹 ‘ 𝑏 ) [,] ( 𝐹 ‘ 𝑎 ) ) ⊆ ran 𝐹 )
46 34 45 eqssd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) → ran 𝐹 = ( ( 𝐹 ‘ 𝑏 ) [,] ( 𝐹 ‘ 𝑎 ) ) )
47 rspceov ⊢ ( ( ( 𝐹 ‘ 𝑏 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑎 ) ∈ ℝ ∧ ran 𝐹 = ( ( 𝐹 ‘ 𝑏 ) [,] ( 𝐹 ‘ 𝑎 ) ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ran 𝐹 = ( 𝑥 [,] 𝑦 ) )
48 14 17 46 47 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ran 𝐹 = ( 𝑥 [,] 𝑦 ) )
49 48 ex ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ran 𝐹 = ( 𝑥 [,] 𝑦 ) ) )
50 8 49 biimtrrid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ran 𝐹 = ( 𝑥 [,] 𝑦 ) ) )
51 50 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∃ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐹 ‘ 𝑧 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ran 𝐹 = ( 𝑥 [,] 𝑦 ) ) )
52 7 51 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ran 𝐹 = ( 𝑥 [,] 𝑦 ) )