Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ivthALT Structured version   Visualization version   GIF version

Theorem ivthALT 32305
Description: An alternate proof of the Intermediate Value Theorem ivth 23204 using topology. (Contributed by Jeff Hankins, 17-Aug-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.)
Assertion
Ref Expression
ivthALT (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ∃𝑥 ∈ (𝐴(,)𝐵)(𝐹𝑥) = 𝑈)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐷   𝑥,𝐹   𝑥,𝑈

Proof of Theorem ivthALT
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 simp31 1095 . . . . . 6 (((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → 𝐹 ∈ (𝐷cn→ℂ))
2 cncff 22677 . . . . . 6 (𝐹 ∈ (𝐷cn→ℂ) → 𝐹:𝐷⟶ℂ)
31, 2syl 17 . . . . 5 (((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → 𝐹:𝐷⟶ℂ)
4 ffun 6035 . . . . 5 (𝐹:𝐷⟶ℂ → Fun 𝐹)
53, 4syl 17 . . . 4 (((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → Fun 𝐹)
653ad2ant3 1082 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → Fun 𝐹)
7 iccconn 22614 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Conn)
873adant3 1079 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Conn)
983ad2ant1 1080 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Conn)
10 simpr1 1065 . . . . . . . . . . . . . 14 ((𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → 𝐹 ∈ (𝐷cn→ℂ))
1110, 2syl 17 . . . . . . . . . . . . 13 ((𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → 𝐹:𝐷⟶ℂ)
1211anim2i 592 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ⊆ 𝐷 ∧ (𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝐴[,]𝐵) ⊆ 𝐷𝐹:𝐷⟶ℂ))
13123impb 1258 . . . . . . . . . . 11 (((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → ((𝐴[,]𝐵) ⊆ 𝐷𝐹:𝐷⟶ℂ))
14133ad2ant3 1082 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝐴[,]𝐵) ⊆ 𝐷𝐹:𝐷⟶ℂ))
154adantl 482 . . . . . . . . . . 11 (((𝐴[,]𝐵) ⊆ 𝐷𝐹:𝐷⟶ℂ) → Fun 𝐹)
16 fdm 6038 . . . . . . . . . . . . 13 (𝐹:𝐷⟶ℂ → dom 𝐹 = 𝐷)
1716sseq2d 3625 . . . . . . . . . . . 12 (𝐹:𝐷⟶ℂ → ((𝐴[,]𝐵) ⊆ dom 𝐹 ↔ (𝐴[,]𝐵) ⊆ 𝐷))
1817biimparc 504 . . . . . . . . . . 11 (((𝐴[,]𝐵) ⊆ 𝐷𝐹:𝐷⟶ℂ) → (𝐴[,]𝐵) ⊆ dom 𝐹)
1915, 18jca 554 . . . . . . . . . 10 (((𝐴[,]𝐵) ⊆ 𝐷𝐹:𝐷⟶ℂ) → (Fun 𝐹 ∧ (𝐴[,]𝐵) ⊆ dom 𝐹))
2014, 19syl 17 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (Fun 𝐹 ∧ (𝐴[,]𝐵) ⊆ dom 𝐹))
21 fores 6111 . . . . . . . . 9 ((Fun 𝐹 ∧ (𝐴[,]𝐵) ⊆ dom 𝐹) → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)–onto→(𝐹 “ (𝐴[,]𝐵)))
2220, 21syl 17 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)–onto→(𝐹 “ (𝐴[,]𝐵)))
23 retop 22546 . . . . . . . . . 10 (topGen‘ran (,)) ∈ Top
24 simp332 1213 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ)
25 uniretop 22547 . . . . . . . . . . 11 ℝ = (topGen‘ran (,))
2625restuni 20947 . . . . . . . . . 10 (((topGen‘ran (,)) ∈ Top ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ) → (𝐹 “ (𝐴[,]𝐵)) = ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))))
2723, 24, 26sylancr 694 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 “ (𝐴[,]𝐵)) = ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))))
28 foeq3 6100 . . . . . . . . 9 ((𝐹 “ (𝐴[,]𝐵)) = ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) → ((𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)–onto→(𝐹 “ (𝐴[,]𝐵)) ↔ (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)–onto ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵)))))
2927, 28syl 17 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)–onto→(𝐹 “ (𝐴[,]𝐵)) ↔ (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)–onto ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵)))))
3022, 29mpbid 222 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)–onto ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))))
31 simp331 1212 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐹 ∈ (𝐷cn→ℂ))
32 ssid 3616 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
33 eqid 2620 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
34 eqid 2620 . . . . . . . . . . . . . . . 16 ((TopOpen‘ℂfld) ↾t 𝐷) = ((TopOpen‘ℂfld) ↾t 𝐷)
3533cnfldtop 22568 . . . . . . . . . . . . . . . . . 18 (TopOpen‘ℂfld) ∈ Top
3633cnfldtopon 22567 . . . . . . . . . . . . . . . . . . . 20 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
3736toponunii 20702 . . . . . . . . . . . . . . . . . . 19 ℂ = (TopOpen‘ℂfld)
3837restid 16075 . . . . . . . . . . . . . . . . . 18 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
3935, 38ax-mp 5 . . . . . . . . . . . . . . . . 17 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
4039eqcomi 2629 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
4133, 34, 40cncfcn 22693 . . . . . . . . . . . . . . 15 ((𝐷 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐷cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝐷) Cn (TopOpen‘ℂfld)))
4232, 41mpan2 706 . . . . . . . . . . . . . 14 (𝐷 ⊆ ℂ → (𝐷cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝐷) Cn (TopOpen‘ℂfld)))
43423ad2ant2 1081 . . . . . . . . . . . . 13 (((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → (𝐷cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝐷) Cn (TopOpen‘ℂfld)))
44433ad2ant3 1082 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐷cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝐷) Cn (TopOpen‘ℂfld)))
4531, 44eleqtrd 2701 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐹 ∈ (((TopOpen‘ℂfld) ↾t 𝐷) Cn (TopOpen‘ℂfld)))
46 simp31 1095 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐴[,]𝐵) ⊆ 𝐷)
47 simp32 1096 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐷 ⊆ ℂ)
48 resttopon 20946 . . . . . . . . . . . . . 14 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝐷 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝐷) ∈ (TopOn‘𝐷))
4936, 47, 48sylancr 694 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((TopOpen‘ℂfld) ↾t 𝐷) ∈ (TopOn‘𝐷))
50 toponuni 20700 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ↾t 𝐷) ∈ (TopOn‘𝐷) → 𝐷 = ((TopOpen‘ℂfld) ↾t 𝐷))
5149, 50syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐷 = ((TopOpen‘ℂfld) ↾t 𝐷))
5246, 51sseqtrd 3633 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐴[,]𝐵) ⊆ ((TopOpen‘ℂfld) ↾t 𝐷))
53 eqid 2620 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t 𝐷) = ((TopOpen‘ℂfld) ↾t 𝐷)
5453cnrest 21070 . . . . . . . . . . 11 ((𝐹 ∈ (((TopOpen‘ℂfld) ↾t 𝐷) Cn (TopOpen‘ℂfld)) ∧ (𝐴[,]𝐵) ⊆ ((TopOpen‘ℂfld) ↾t 𝐷)) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((((TopOpen‘ℂfld) ↾t 𝐷) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
5545, 52, 54syl2anc 692 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((((TopOpen‘ℂfld) ↾t 𝐷) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
5635a1i 11 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (TopOpen‘ℂfld) ∈ Top)
57 cnex 10002 . . . . . . . . . . . . . 14 ℂ ∈ V
58 ssexg 4795 . . . . . . . . . . . . . 14 ((𝐷 ⊆ ℂ ∧ ℂ ∈ V) → 𝐷 ∈ V)
5947, 57, 58sylancl 693 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐷 ∈ V)
60 restabs 20950 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ⊆ 𝐷𝐷 ∈ V) → (((TopOpen‘ℂfld) ↾t 𝐷) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
6156, 46, 59, 60syl3anc 1324 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (((TopOpen‘ℂfld) ↾t 𝐷) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
62 iccssre 12240 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
63623adant3 1079 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
64633ad2ant1 1080 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐴[,]𝐵) ⊆ ℝ)
65 eqid 2620 . . . . . . . . . . . . . 14 (topGen‘ran (,)) = (topGen‘ran (,))
6633, 65rerest 22588 . . . . . . . . . . . . 13 ((𝐴[,]𝐵) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))
6764, 66syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))
6861, 67eqtrd 2654 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (((TopOpen‘ℂfld) ↾t 𝐷) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))
6968oveq1d 6650 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((((TopOpen‘ℂfld) ↾t 𝐷) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)) = (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
7055, 69eleqtrd 2701 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
7136a1i 11 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
72 df-ima 5117 . . . . . . . . . . . 12 (𝐹 “ (𝐴[,]𝐵)) = ran (𝐹 ↾ (𝐴[,]𝐵))
7372eqimss2i 3652 . . . . . . . . . . 11 ran (𝐹 ↾ (𝐴[,]𝐵)) ⊆ (𝐹 “ (𝐴[,]𝐵))
7473a1i 11 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ran (𝐹 ↾ (𝐴[,]𝐵)) ⊆ (𝐹 “ (𝐴[,]𝐵)))
75 ax-resscn 9978 . . . . . . . . . . 11 ℝ ⊆ ℂ
7624, 75syl6ss 3607 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 “ (𝐴[,]𝐵)) ⊆ ℂ)
77 cnrest2 21071 . . . . . . . . . 10 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ ran (𝐹 ↾ (𝐴[,]𝐵)) ⊆ (𝐹 “ (𝐴[,]𝐵)) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℂ) → ((𝐹 ↾ (𝐴[,]𝐵)) ∈ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐹 ↾ (𝐴[,]𝐵)) ∈ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn ((TopOpen‘ℂfld) ↾t (𝐹 “ (𝐴[,]𝐵))))))
7871, 74, 76, 77syl3anc 1324 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝐹 ↾ (𝐴[,]𝐵)) ∈ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐹 ↾ (𝐴[,]𝐵)) ∈ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn ((TopOpen‘ℂfld) ↾t (𝐹 “ (𝐴[,]𝐵))))))
7970, 78mpbid 222 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn ((TopOpen‘ℂfld) ↾t (𝐹 “ (𝐴[,]𝐵)))))
8033, 65rerest 22588 . . . . . . . . . 10 ((𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (𝐹 “ (𝐴[,]𝐵))) = ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))))
8124, 80syl 17 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((TopOpen‘ℂfld) ↾t (𝐹 “ (𝐴[,]𝐵))) = ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))))
8281oveq2d 6651 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn ((TopOpen‘ℂfld) ↾t (𝐹 “ (𝐴[,]𝐵)))) = (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵)))))
8379, 82eleqtrd 2701 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵)))))
84 eqid 2620 . . . . . . . 8 ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) = ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵)))
8584cnconn 21206 . . . . . . 7 ((((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Conn ∧ (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)–onto ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) ∧ (𝐹 ↾ (𝐴[,]𝐵)) ∈ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))))) → ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) ∈ Conn)
869, 30, 83, 85syl3anc 1324 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) ∈ Conn)
87 reconn 22612 . . . . . . . . 9 ((𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ → (((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) ∈ Conn ↔ ∀𝑥 ∈ (𝐹 “ (𝐴[,]𝐵))∀𝑦 ∈ (𝐹 “ (𝐴[,]𝐵))(𝑥[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵))))
88873ad2ant2 1081 . . . . . . . 8 ((𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))) → (((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) ∈ Conn ↔ ∀𝑥 ∈ (𝐹 “ (𝐴[,]𝐵))∀𝑦 ∈ (𝐹 “ (𝐴[,]𝐵))(𝑥[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵))))
89883ad2ant3 1082 . . . . . . 7 (((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → (((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) ∈ Conn ↔ ∀𝑥 ∈ (𝐹 “ (𝐴[,]𝐵))∀𝑦 ∈ (𝐹 “ (𝐴[,]𝐵))(𝑥[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵))))
90893ad2ant3 1082 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) ∈ Conn ↔ ∀𝑥 ∈ (𝐹 “ (𝐴[,]𝐵))∀𝑦 ∈ (𝐹 “ (𝐴[,]𝐵))(𝑥[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵))))
9186, 90mpbid 222 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ∀𝑥 ∈ (𝐹 “ (𝐴[,]𝐵))∀𝑦 ∈ (𝐹 “ (𝐴[,]𝐵))(𝑥[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵)))
92 simp11 1089 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐴 ∈ ℝ)
9392rexrd 10074 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐴 ∈ ℝ*)
94 simp12 1090 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐵 ∈ ℝ)
9594rexrd 10074 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐵 ∈ ℝ*)
96 ltle 10111 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴𝐵))
9796imp 445 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < 𝐵) → 𝐴𝐵)
98973adantl3 1217 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵) → 𝐴𝐵)
99983adant3 1079 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐴𝐵)
100 lbicc2 12273 . . . . . . . 8 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
10193, 95, 99, 100syl3anc 1324 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐴 ∈ (𝐴[,]𝐵))
102 funfvima2 6478 . . . . . . 7 ((Fun 𝐹 ∧ (𝐴[,]𝐵) ⊆ dom 𝐹) → (𝐴 ∈ (𝐴[,]𝐵) → (𝐹𝐴) ∈ (𝐹 “ (𝐴[,]𝐵))))
10320, 101, 102sylc 65 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹𝐴) ∈ (𝐹 “ (𝐴[,]𝐵)))
104 ubicc2 12274 . . . . . . . 8 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
10593, 95, 99, 104syl3anc 1324 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐵 ∈ (𝐴[,]𝐵))
106 funfvima2 6478 . . . . . . 7 ((Fun 𝐹 ∧ (𝐴[,]𝐵) ⊆ dom 𝐹) → (𝐵 ∈ (𝐴[,]𝐵) → (𝐹𝐵) ∈ (𝐹 “ (𝐴[,]𝐵))))
10720, 105, 106sylc 65 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹𝐵) ∈ (𝐹 “ (𝐴[,]𝐵)))
108 oveq1 6642 . . . . . . . 8 (𝑥 = (𝐹𝐴) → (𝑥[,]𝑦) = ((𝐹𝐴)[,]𝑦))
109108sseq1d 3624 . . . . . . 7 (𝑥 = (𝐹𝐴) → ((𝑥[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵)) ↔ ((𝐹𝐴)[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵))))
110 oveq2 6643 . . . . . . . 8 (𝑦 = (𝐹𝐵) → ((𝐹𝐴)[,]𝑦) = ((𝐹𝐴)[,](𝐹𝐵)))
111110sseq1d 3624 . . . . . . 7 (𝑦 = (𝐹𝐵) → (((𝐹𝐴)[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵)) ↔ ((𝐹𝐴)[,](𝐹𝐵)) ⊆ (𝐹 “ (𝐴[,]𝐵))))
112109, 111rspc2v 3317 . . . . . 6 (((𝐹𝐴) ∈ (𝐹 “ (𝐴[,]𝐵)) ∧ (𝐹𝐵) ∈ (𝐹 “ (𝐴[,]𝐵))) → (∀𝑥 ∈ (𝐹 “ (𝐴[,]𝐵))∀𝑦 ∈ (𝐹 “ (𝐴[,]𝐵))(𝑥[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵)) → ((𝐹𝐴)[,](𝐹𝐵)) ⊆ (𝐹 “ (𝐴[,]𝐵))))
113103, 107, 112syl2anc 692 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (∀𝑥 ∈ (𝐹 “ (𝐴[,]𝐵))∀𝑦 ∈ (𝐹 “ (𝐴[,]𝐵))(𝑥[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵)) → ((𝐹𝐴)[,](𝐹𝐵)) ⊆ (𝐹 “ (𝐴[,]𝐵))))
11491, 113mpd 15 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝐹𝐴)[,](𝐹𝐵)) ⊆ (𝐹 “ (𝐴[,]𝐵)))
115 ioossicc 12244 . . . . . . . 8 ((𝐹𝐴)(,)(𝐹𝐵)) ⊆ ((𝐹𝐴)[,](𝐹𝐵))
116115sseli 3591 . . . . . . 7 (𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)) → 𝑈 ∈ ((𝐹𝐴)[,](𝐹𝐵)))
1171163ad2ant3 1082 . . . . . 6 ((𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))) → 𝑈 ∈ ((𝐹𝐴)[,](𝐹𝐵)))
1181173ad2ant3 1082 . . . . 5 (((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → 𝑈 ∈ ((𝐹𝐴)[,](𝐹𝐵)))
1191183ad2ant3 1082 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝑈 ∈ ((𝐹𝐴)[,](𝐹𝐵)))
120114, 119sseldd 3596 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝑈 ∈ (𝐹 “ (𝐴[,]𝐵)))
121 fvelima 6235 . . 3 ((Fun 𝐹𝑈 ∈ (𝐹 “ (𝐴[,]𝐵))) → ∃𝑥 ∈ (𝐴[,]𝐵)(𝐹𝑥) = 𝑈)
1226, 120, 121syl2anc 692 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ∃𝑥 ∈ (𝐴[,]𝐵)(𝐹𝑥) = 𝑈)
123 simpl1 1062 . . . . . . . 8 (((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈) → 𝑥 ∈ ℝ*)
124123a1i 11 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈) → 𝑥 ∈ ℝ*))
125 simprr 795 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → (𝐹𝑥) = 𝑈)
12624, 103sseldd 3596 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹𝐴) ∈ ℝ)
127 simp333 1214 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))
128126rexrd 10074 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹𝐴) ∈ ℝ*)
12924, 107sseldd 3596 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹𝐵) ∈ ℝ)
130129rexrd 10074 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹𝐵) ∈ ℝ*)
131 elioo2 12201 . . . . . . . . . . . . . . . . 17 (((𝐹𝐴) ∈ ℝ* ∧ (𝐹𝐵) ∈ ℝ*) → (𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)) ↔ (𝑈 ∈ ℝ ∧ (𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵))))
132128, 130, 131syl2anc 692 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)) ↔ (𝑈 ∈ ℝ ∧ (𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵))))
133127, 132mpbid 222 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝑈 ∈ ℝ ∧ (𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))
134133simp2d 1072 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹𝐴) < 𝑈)
135126, 134gtned 10157 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝑈 ≠ (𝐹𝐴))
136135adantr 481 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → 𝑈 ≠ (𝐹𝐴))
137125, 136eqnetrd 2858 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → (𝐹𝑥) ≠ (𝐹𝐴))
138137neneqd 2796 . . . . . . . . . 10 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → ¬ (𝐹𝑥) = (𝐹𝐴))
139 fveq2 6178 . . . . . . . . . 10 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
140138, 139nsyl 135 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → ¬ 𝑥 = 𝐴)
141 simp13 1091 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝑈 ∈ ℝ)
142133simp3d 1073 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝑈 < (𝐹𝐵))
143141, 142ltned 10158 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝑈 ≠ (𝐹𝐵))
144143adantr 481 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → 𝑈 ≠ (𝐹𝐵))
145125, 144eqnetrd 2858 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → (𝐹𝑥) ≠ (𝐹𝐵))
146145neneqd 2796 . . . . . . . . . 10 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → ¬ (𝐹𝑥) = (𝐹𝐵))
147 fveq2 6178 . . . . . . . . . 10 (𝑥 = 𝐵 → (𝐹𝑥) = (𝐹𝐵))
148146, 147nsyl 135 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → ¬ 𝑥 = 𝐵)
149 simprl3 1106 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵))
150140, 148, 149ecase13d 32282 . . . . . . . 8 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → (𝐴 < 𝑥𝑥 < 𝐵))
151150ex 450 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈) → (𝐴 < 𝑥𝑥 < 𝐵)))
152124, 151jcad 555 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈) → (𝑥 ∈ ℝ* ∧ (𝐴 < 𝑥𝑥 < 𝐵))))
153 3anass 1040 . . . . . 6 ((𝑥 ∈ ℝ*𝐴 < 𝑥𝑥 < 𝐵) ↔ (𝑥 ∈ ℝ* ∧ (𝐴 < 𝑥𝑥 < 𝐵)))
154152, 153syl6ibr 242 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈) → (𝑥 ∈ ℝ*𝐴 < 𝑥𝑥 < 𝐵)))
155 rexr 10070 . . . . . . . . 9 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
156 rexr 10070 . . . . . . . . 9 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
157 elicc3 32286 . . . . . . . . 9 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵))))
158155, 156, 157syl2an 494 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵))))
1591583adant3 1079 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵))))
1601593ad2ant1 1080 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵))))
161160anbi1d 740 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝑥 ∈ (𝐴[,]𝐵) ∧ (𝐹𝑥) = 𝑈) ↔ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)))
162 elioo1 12200 . . . . . . . 8 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝑥 ∈ (𝐴(,)𝐵) ↔ (𝑥 ∈ ℝ*𝐴 < 𝑥𝑥 < 𝐵)))
163155, 156, 162syl2an 494 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴(,)𝐵) ↔ (𝑥 ∈ ℝ*𝐴 < 𝑥𝑥 < 𝐵)))
1641633adant3 1079 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) → (𝑥 ∈ (𝐴(,)𝐵) ↔ (𝑥 ∈ ℝ*𝐴 < 𝑥𝑥 < 𝐵)))
1651643ad2ant1 1080 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝑥 ∈ (𝐴(,)𝐵) ↔ (𝑥 ∈ ℝ*𝐴 < 𝑥𝑥 < 𝐵)))
166154, 161, 1653imtr4d 283 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝑥 ∈ (𝐴[,]𝐵) ∧ (𝐹𝑥) = 𝑈) → 𝑥 ∈ (𝐴(,)𝐵)))
167 simpr 477 . . . . 5 ((𝑥 ∈ (𝐴[,]𝐵) ∧ (𝐹𝑥) = 𝑈) → (𝐹𝑥) = 𝑈)
168167a1i 11 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝑥 ∈ (𝐴[,]𝐵) ∧ (𝐹𝑥) = 𝑈) → (𝐹𝑥) = 𝑈))
169166, 168jcad 555 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝑥 ∈ (𝐴[,]𝐵) ∧ (𝐹𝑥) = 𝑈) → (𝑥 ∈ (𝐴(,)𝐵) ∧ (𝐹𝑥) = 𝑈)))
170169reximdv2 3011 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (∃𝑥 ∈ (𝐴[,]𝐵)(𝐹𝑥) = 𝑈 → ∃𝑥 ∈ (𝐴(,)𝐵)(𝐹𝑥) = 𝑈))
171122, 170mpd 15 1 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ∃𝑥 ∈ (𝐴(,)𝐵)(𝐹𝑥) = 𝑈)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3o 1035  w3a 1036   = wceq 1481  wcel 1988  wne 2791  wral 2909  wrex 2910  Vcvv 3195  wss 3567   cuni 4427   class class class wbr 4644  dom cdm 5104  ran crn 5105  cres 5106  cima 5107  Fun wfun 5870  wf 5872  ontowfo 5874  cfv 5876  (class class class)co 6635  cc 9919  cr 9920  *cxr 10058   < clt 10059  cle 10060  (,)cioo 12160  [,]cicc 12163  t crest 16062  TopOpenctopn 16063  topGenctg 16079  fldccnfld 19727  Topctop 20679  TopOnctopon 20696   Cn ccn 21009  Conncconn 21195  cnccncf 22660
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-er 7727  df-map 7844  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-fi 8302  df-sup 8333  df-inf 8334  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-4 11066  df-5 11067  df-6 11068  df-7 11069  df-8 11070  df-9 11071  df-n0 11278  df-z 11363  df-dec 11479  df-uz 11673  df-q 11774  df-rp 11818  df-xneg 11931  df-xadd 11932  df-xmul 11933  df-ioo 12164  df-ico 12166  df-icc 12167  df-fz 12312  df-seq 12785  df-exp 12844  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-struct 15840  df-ndx 15841  df-slot 15842  df-base 15844  df-plusg 15935  df-mulr 15936  df-starv 15937  df-tset 15941  df-ple 15942  df-ds 15945  df-unif 15946  df-rest 16064  df-topn 16065  df-topgen 16085  df-psmet 19719  df-xmet 19720  df-met 19721  df-bl 19722  df-mopn 19723  df-cnfld 19728  df-top 20680  df-topon 20697  df-topsp 20718  df-bases 20731  df-cld 20804  df-cn 21012  df-cnp 21013  df-conn 21196  df-xms 22106  df-ms 22107  df-cncf 22662
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator