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 ffvelrnd ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐹𝑏 ) ∈ ℝ )
14 13 adantr ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹𝑧 ) ≤ ( 𝐹𝑎 ) ∧ ( 𝐹𝑏 ) ≤ ( 𝐹𝑧 ) ) ) → ( 𝐹𝑏 ) ∈ ℝ )
15 simprl ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑎 ∈ ( 𝐴 [,] 𝐵 ) )
16 11 15 ffvelrnd ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐹𝑎 ) ∈ ℝ )
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 ffvelrnda ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹𝑧 ) ∈ ℝ )
27 26 biantrurd ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝐹𝑏 ) ≤ ( 𝐹𝑧 ) ∧ ( 𝐹𝑧 ) ≤ ( 𝐹𝑎 ) ) ↔ ( ( 𝐹𝑧 ) ∈ ℝ ∧ ( ( 𝐹𝑏 ) ≤ ( 𝐹𝑧 ) ∧ ( 𝐹𝑧 ) ≤ ( 𝐹𝑎 ) ) ) ) )
28 25 27 syl5bb ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝐹𝑧 ) ≤ ( 𝐹𝑎 ) ∧ ( 𝐹𝑏 ) ≤ ( 𝐹𝑧 ) ) ↔ ( ( 𝐹𝑧 ) ∈ ℝ ∧ ( ( 𝐹𝑏 ) ≤ ( 𝐹𝑧 ) ∧ ( 𝐹𝑧 ) ≤ ( 𝐹𝑎 ) ) ) ) )
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 ffvelrnda ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹𝑥 ) ∈ ℝ )
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 syl5bir ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹𝑧 ) ≤ ( 𝐹𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹𝑏 ) ≤ ( 𝐹𝑧 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ran 𝐹 = ( 𝑥 [,] 𝑦 ) ) )
51 50 rexlimdvva ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∃ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹𝑧 ) ≤ ( 𝐹𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹𝑏 ) ≤ ( 𝐹𝑧 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ran 𝐹 = ( 𝑥 [,] 𝑦 ) ) )
52 7 51 mpd ( 𝜑 → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ran 𝐹 = ( 𝑥 [,] 𝑦 ) )