Metamath Proof Explorer

Theorem ivthALT

Description: An alternate proof of the Intermediate Value Theorem ivth using topology. (Contributed by Jeff Hankins, 17-Aug-2009) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion ivthALT ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑥 ) = 𝑈 )

Proof

Step Hyp Ref Expression
1 simp31 ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
2 cncff ⊢ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) → 𝐹 : 𝐷 ⟶ ℂ )
3 1 2 syl ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) → 𝐹 : 𝐷 ⟶ ℂ )
4 ffun ⊢ ( 𝐹 : 𝐷 ⟶ ℂ → Fun 𝐹 )
5 3 4 syl ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) → Fun 𝐹 )
6 5 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → Fun 𝐹 )
7 iccconn ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Conn )
8 7 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Conn )
9 8 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Conn )
10 simpr1 ⊢ ( ( 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
11 10 2 syl ⊢ ( ( 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) → 𝐹 : 𝐷 ⟶ ℂ )
12 11 anim2i ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ ( 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐹 : 𝐷 ⟶ ℂ ) )
13 12 3impb ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) → ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐹 : 𝐷 ⟶ ℂ ) )
14 13 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐹 : 𝐷 ⟶ ℂ ) )
15 4 adantl ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐹 : 𝐷 ⟶ ℂ ) → Fun 𝐹 )
16 fdm ⊢ ( 𝐹 : 𝐷 ⟶ ℂ → dom 𝐹 = 𝐷 )
17 16 sseq2d ⊢ ( 𝐹 : 𝐷 ⟶ ℂ → ( ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 ↔ ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ) )
18 17 biimparc ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐹 : 𝐷 ⟶ ℂ ) → ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 )
19 15 18 jca ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐹 : 𝐷 ⟶ ℂ ) → ( Fun 𝐹 ∧ ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 ) )
20 14 19 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( Fun 𝐹 ∧ ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 ) )
21 fores ⊢ ( ( Fun 𝐹 ∧ ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) –onto→ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) )
22 20 21 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) –onto→ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) )
23 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
24 simp332 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ )
25 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
26 25 restuni ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ) → ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) = ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
27 23 24 26 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) = ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
28 foeq3 ⊢ ( ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) = ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) –onto→ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) –onto→ ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ) )
29 27 28 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) –onto→ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) –onto→ ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ) )
30 22 29 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) –onto→ ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
31 simp331 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
32 ssid ⊢ ℂ ⊆ ℂ
33 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
34 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 )
35 33 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
36 33 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
37 36 toponunii ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
38 37 restid ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
39 35 38 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
40 39 eqcomi ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
41 33 34 40 cncfcn ⊢ ( ( 𝐷 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐷 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( TopOpen ‘ ℂfld ) ) )
42 32 41 mpan2 ⊢ ( 𝐷 ⊆ ℂ → ( 𝐷 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( TopOpen ‘ ℂfld ) ) )
43 42 3ad2ant2 ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) → ( 𝐷 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( TopOpen ‘ ℂfld ) ) )
44 43 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐷 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( TopOpen ‘ ℂfld ) ) )
45 31 44 eleqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( TopOpen ‘ ℂfld ) ) )
46 simp31 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 )
47 simp32 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝐷 ⊆ ℂ )
48 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝐷 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
49 36 47 48 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
50 toponuni ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) → 𝐷 = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) )
51 49 50 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝐷 = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) )
52 46 51 sseqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) )
53 eqid ⊢ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 )
54 53 cnrest ⊢ ( ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( TopOpen ‘ ℂfld ) ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
55 45 52 54 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
56 35 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( TopOpen ‘ ℂfld ) ∈ Top )
57 cnex ⊢ ℂ ∈ V
58 ssexg ⊢ ( ( 𝐷 ⊆ ℂ ∧ ℂ ∈ V ) → 𝐷 ∈ V )
59 47 57 58 sylancl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝐷 ∈ V )
60 restabs ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ∈ V ) → ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) )
61 56 46 59 60 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) )
62 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
63 62 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
64 63 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
65 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
66 33 65 rerest ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) )
67 64 66 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) )
68 61 67 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) )
69 68 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) = ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
70 55 69 eleqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
71 36 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
72 df-ima ⊢ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) = ran ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) )
73 72 eqimss2i ⊢ ran ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) )
74 73 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ran ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) )
75 ax-resscn ⊢ ℝ ⊆ ℂ
76 24 75 sstrdi ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℂ )
77 cnrest2 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℂ ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ) ) )
78 71 74 76 77 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ) ) )
79 70 78 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ) )
80 33 65 rerest ⊢ ( ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
81 24 80 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
82 81 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ) = ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ) )
83 79 82 eleqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ) )
84 eqid ⊢ ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) = ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) )
85 84 cnconn ⊢ ( ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Conn ∧ ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) : ( 𝐴 [,] 𝐵 ) –onto→ ∪ ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) Cn ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ) ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ∈ Conn )
86 9 30 83 85 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ∈ Conn )
87 reconn ⊢ ( ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ∈ Conn ↔ ∀ 𝑥 ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑦 ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
88 87 3ad2ant2 ⊢ ( ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ∈ Conn ↔ ∀ 𝑥 ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑦 ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
89 88 3ad2ant3 ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ∈ Conn ↔ ∀ 𝑥 ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑦 ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
90 89 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( ( topGen ‘ ran (,) ) ↾t ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) ∈ Conn ↔ ∀ 𝑥 ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑦 ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
91 86 90 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ∀ 𝑥 ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑦 ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) )
92 simp11 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝐴 ∈ ℝ )
93 92 rexrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝐴 ∈ ℝ* )
94 simp12 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝐵 ∈ ℝ )
95 94 rexrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝐵 ∈ ℝ* )
96 ltle ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 → 𝐴 ≤ 𝐵 ) )
97 96 imp ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) → 𝐴 ≤ 𝐵 )
98 97 3adantl3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) → 𝐴 ≤ 𝐵 )
99 98 3adant3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝐴 ≤ 𝐵 )
100 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
101 93 95 99 100 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
102 funfvima2 ⊢ ( ( Fun 𝐹 ∧ ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 ) → ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
103 20 101 102 sylc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) )
104 ubicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
105 93 95 99 104 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
106 funfvima2 ⊢ ( ( Fun 𝐹 ∧ ( 𝐴 [,] 𝐵 ) ⊆ dom 𝐹 ) → ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
107 20 105 106 sylc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) )
108 oveq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝐴 ) → ( 𝑥 [,] 𝑦 ) = ( ( 𝐹 ‘ 𝐴 ) [,] 𝑦 ) )
109 108 sseq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝐴 ) → ( ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ↔ ( ( 𝐹 ‘ 𝐴 ) [,] 𝑦 ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
110 oveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) → ( ( 𝐹 ‘ 𝐴 ) [,] 𝑦 ) = ( ( 𝐹 ‘ 𝐴 ) [,] ( 𝐹 ‘ 𝐵 ) ) )
111 110 sseq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) → ( ( ( 𝐹 ‘ 𝐴 ) [,] 𝑦 ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ↔ ( ( 𝐹 ‘ 𝐴 ) [,] ( 𝐹 ‘ 𝐵 ) ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
112 109 111 rspc2v ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) → ( ∀ 𝑥 ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑦 ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ‘ 𝐴 ) [,] ( 𝐹 ‘ 𝐵 ) ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
113 103 107 112 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ∀ 𝑥 ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ∀ 𝑦 ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ( 𝑥 [,] 𝑦 ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ‘ 𝐴 ) [,] ( 𝐹 ‘ 𝐵 ) ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) )
114 91 113 mpd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( 𝐹 ‘ 𝐴 ) [,] ( 𝐹 ‘ 𝐵 ) ) ⊆ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) )
115 ioossicc ⊢ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ⊆ ( ( 𝐹 ‘ 𝐴 ) [,] ( 𝐹 ‘ 𝐵 ) )
116 115 sseli ⊢ ( 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) → 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) [,] ( 𝐹 ‘ 𝐵 ) ) )
117 116 3ad2ant3 ⊢ ( ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) → 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) [,] ( 𝐹 ‘ 𝐵 ) ) )
118 117 3ad2ant3 ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) → 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) [,] ( 𝐹 ‘ 𝐵 ) ) )
119 118 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) [,] ( 𝐹 ‘ 𝐵 ) ) )
120 114 119 sseldd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝑈 ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) )
121 fvelima ⊢ ( ( Fun 𝐹 ∧ 𝑈 ∈ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ) → ∃ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) = 𝑈 )
122 6 120 121 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ∃ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) = 𝑈 )
123 simpl1 ⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) → 𝑥 ∈ ℝ* )
124 123 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) → 𝑥 ∈ ℝ* ) )
125 simprr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) ) → ( 𝐹 ‘ 𝑥 ) = 𝑈 )
126 24 103 sseldd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
127 simp333 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) )
128 126 rexrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ* )
129 24 107 sseldd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
130 129 rexrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ* )
131 elioo2 ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝐵 ) ∈ ℝ* ) → ( 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ↔ ( 𝑈 ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) ) )
132 128 130 131 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ↔ ( 𝑈 ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) ) )
133 127 132 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝑈 ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) )
134 133 simp2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝐹 ‘ 𝐴 ) < 𝑈 )
135 126 134 gtned ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝑈 ≠ ( 𝐹 ‘ 𝐴 ) )
136 135 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) ) → 𝑈 ≠ ( 𝐹 ‘ 𝐴 ) )
137 125 136 eqnetrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) ) → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝐴 ) )
138 137 neneqd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
139 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
140 138 139 nsyl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) ) → ¬ 𝑥 = 𝐴 )
141 simp13 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝑈 ∈ ℝ )
142 133 simp3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝑈 < ( 𝐹 ‘ 𝐵 ) )
143 141 142 ltned ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → 𝑈 ≠ ( 𝐹 ‘ 𝐵 ) )
144 143 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) ) → 𝑈 ≠ ( 𝐹 ‘ 𝐵 ) )
145 125 144 eqnetrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) ) → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝐵 ) )
146 145 neneqd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
147 fveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
148 146 147 nsyl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) ) → ¬ 𝑥 = 𝐵 )
149 simprl3 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) ) → ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) )
150 140 148 149 ecase13d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) ) → ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
151 150 ex ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) → ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
152 124 151 jcad ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) → ( 𝑥 ∈ ℝ* ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) ) )
153 3anass ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
154 152 153 imbitrrdi ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) → ( 𝑥 ∈ ℝ* ∧ 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
155 rexr ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
156 rexr ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
157 elicc3 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ) )
158 155 156 157 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ) )
159 158 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ) )
160 159 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ) )
161 160 anbi1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) ↔ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ ( 𝑥 = 𝐴 ∨ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ∨ 𝑥 = 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) ) )
162 elioo1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
163 155 156 162 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
164 163 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
165 164 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
166 154 161 165 3imtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) )
167 simpr ⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) → ( 𝐹 ‘ 𝑥 ) = 𝑈 )
168 167 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) → ( 𝐹 ‘ 𝑥 ) = 𝑈 ) )
169 166 168 jcad ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑈 ) ) )
170 169 reximdv2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ( ∃ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) = 𝑈 → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑥 ) = 𝑈 ) )
171 122 170 mpd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ 𝐴 < 𝐵 ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ ( 𝐹 “ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ ∧ 𝑈 ∈ ( ( 𝐹 ‘ 𝐴 ) (,) ( 𝐹 ‘ 𝐵 ) ) ) ) ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑥 ) = 𝑈 )