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 31334
Description: An alternate proof of the Intermediate Value Theorem ivth 22905 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 1089 . . . . . 6 (((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → 𝐹 ∈ (𝐷cn→ℂ))
2 cncff 22427 . . . . . 6 (𝐹 ∈ (𝐷cn→ℂ) → 𝐹:𝐷⟶ℂ)
31, 2syl 17 . . . . 5 (((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → 𝐹:𝐷⟶ℂ)
4 ffun 5846 . . . . 5 (𝐹:𝐷⟶ℂ → Fun 𝐹)
53, 4syl 17 . . . 4 (((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → Fun 𝐹)
653ad2ant3 1076 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → Fun 𝐹)
7 iccconn 22350 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Con)
873adant3 1073 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Con)
983ad2ant1 1074 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Con)
10 simpr1 1059 . . . . . . . . . . . . . 14 ((𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → 𝐹 ∈ (𝐷cn→ℂ))
1110, 2syl 17 . . . . . . . . . . . . 13 ((𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → 𝐹:𝐷⟶ℂ)
1211anim2i 590 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ⊆ 𝐷 ∧ (𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝐴[,]𝐵) ⊆ 𝐷𝐹:𝐷⟶ℂ))
13123impb 1251 . . . . . . . . . . 11 (((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → ((𝐴[,]𝐵) ⊆ 𝐷𝐹:𝐷⟶ℂ))
14133ad2ant3 1076 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝐴[,]𝐵) ⊆ 𝐷𝐹:𝐷⟶ℂ))
154adantl 480 . . . . . . . . . . 11 (((𝐴[,]𝐵) ⊆ 𝐷𝐹:𝐷⟶ℂ) → Fun 𝐹)
16 fdm 5849 . . . . . . . . . . . . 13 (𝐹:𝐷⟶ℂ → dom 𝐹 = 𝐷)
1716sseq2d 3500 . . . . . . . . . . . 12 (𝐹:𝐷⟶ℂ → ((𝐴[,]𝐵) ⊆ dom 𝐹 ↔ (𝐴[,]𝐵) ⊆ 𝐷))
1817biimparc 502 . . . . . . . . . . 11 (((𝐴[,]𝐵) ⊆ 𝐷𝐹:𝐷⟶ℂ) → (𝐴[,]𝐵) ⊆ dom 𝐹)
1915, 18jca 552 . . . . . . . . . 10 (((𝐴[,]𝐵) ⊆ 𝐷𝐹:𝐷⟶ℂ) → (Fun 𝐹 ∧ (𝐴[,]𝐵) ⊆ dom 𝐹))
2014, 19syl 17 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (Fun 𝐹 ∧ (𝐴[,]𝐵) ⊆ dom 𝐹))
21 fores 5921 . . . . . . . . 9 ((Fun 𝐹 ∧ (𝐴[,]𝐵) ⊆ dom 𝐹) → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)–onto→(𝐹 “ (𝐴[,]𝐵)))
2220, 21syl 17 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)–onto→(𝐹 “ (𝐴[,]𝐵)))
23 retop 22284 . . . . . . . . . 10 (topGen‘ran (,)) ∈ Top
24 simp332 1207 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ)
25 uniretop 22285 . . . . . . . . . . 11 ℝ = (topGen‘ran (,))
2625restuni 20679 . . . . . . . . . 10 (((topGen‘ran (,)) ∈ Top ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ) → (𝐹 “ (𝐴[,]𝐵)) = ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))))
2723, 24, 26sylancr 693 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 “ (𝐴[,]𝐵)) = ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))))
28 foeq3 5910 . . . . . . . . 9 ((𝐹 “ (𝐴[,]𝐵)) = ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) → ((𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)–onto→(𝐹 “ (𝐴[,]𝐵)) ↔ (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)–onto ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵)))))
2927, 28syl 17 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)–onto→(𝐹 “ (𝐴[,]𝐵)) ↔ (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)–onto ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵)))))
3022, 29mpbid 220 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)–onto ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))))
31 simp331 1206 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐹 ∈ (𝐷cn→ℂ))
32 ssid 3491 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
33 eqid 2514 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
34 eqid 2514 . . . . . . . . . . . . . . . 16 ((TopOpen‘ℂfld) ↾t 𝐷) = ((TopOpen‘ℂfld) ↾t 𝐷)
3533cnfldtop 22306 . . . . . . . . . . . . . . . . . 18 (TopOpen‘ℂfld) ∈ Top
3633cnfldtopon 22305 . . . . . . . . . . . . . . . . . . . 20 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
3736toponunii 20450 . . . . . . . . . . . . . . . . . . 19 ℂ = (TopOpen‘ℂfld)
3837restid 15801 . . . . . . . . . . . . . . . . . 18 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
3935, 38ax-mp 5 . . . . . . . . . . . . . . . . 17 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
4039eqcomi 2523 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
4133, 34, 40cncfcn 22443 . . . . . . . . . . . . . . 15 ((𝐷 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐷cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝐷) Cn (TopOpen‘ℂfld)))
4232, 41mpan2 702 . . . . . . . . . . . . . 14 (𝐷 ⊆ ℂ → (𝐷cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝐷) Cn (TopOpen‘ℂfld)))
43423ad2ant2 1075 . . . . . . . . . . . . 13 (((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → (𝐷cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝐷) Cn (TopOpen‘ℂfld)))
44433ad2ant3 1076 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐷cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝐷) Cn (TopOpen‘ℂfld)))
4531, 44eleqtrd 2594 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐹 ∈ (((TopOpen‘ℂfld) ↾t 𝐷) Cn (TopOpen‘ℂfld)))
46 simp31 1089 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐴[,]𝐵) ⊆ 𝐷)
47 simp32 1090 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐷 ⊆ ℂ)
48 resttopon 20678 . . . . . . . . . . . . . 14 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝐷 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝐷) ∈ (TopOn‘𝐷))
4936, 47, 48sylancr 693 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((TopOpen‘ℂfld) ↾t 𝐷) ∈ (TopOn‘𝐷))
50 toponuni 20445 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ↾t 𝐷) ∈ (TopOn‘𝐷) → 𝐷 = ((TopOpen‘ℂfld) ↾t 𝐷))
5149, 50syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐷 = ((TopOpen‘ℂfld) ↾t 𝐷))
5246, 51sseqtrd 3508 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐴[,]𝐵) ⊆ ((TopOpen‘ℂfld) ↾t 𝐷))
53 eqid 2514 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t 𝐷) = ((TopOpen‘ℂfld) ↾t 𝐷)
5453cnrest 20802 . . . . . . . . . . 11 ((𝐹 ∈ (((TopOpen‘ℂfld) ↾t 𝐷) Cn (TopOpen‘ℂfld)) ∧ (𝐴[,]𝐵) ⊆ ((TopOpen‘ℂfld) ↾t 𝐷)) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((((TopOpen‘ℂfld) ↾t 𝐷) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
5545, 52, 54syl2anc 690 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((((TopOpen‘ℂfld) ↾t 𝐷) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
5635a1i 11 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (TopOpen‘ℂfld) ∈ Top)
57 cnex 9772 . . . . . . . . . . . . . 14 ℂ ∈ V
58 ssexg 4631 . . . . . . . . . . . . . 14 ((𝐷 ⊆ ℂ ∧ ℂ ∈ V) → 𝐷 ∈ V)
5947, 57, 58sylancl 692 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐷 ∈ V)
60 restabs 20682 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ⊆ 𝐷𝐷 ∈ V) → (((TopOpen‘ℂfld) ↾t 𝐷) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
6156, 46, 59, 60syl3anc 1317 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (((TopOpen‘ℂfld) ↾t 𝐷) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))
62 iccssre 11995 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
63623adant3 1073 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
64633ad2ant1 1074 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐴[,]𝐵) ⊆ ℝ)
65 eqid 2514 . . . . . . . . . . . . . 14 (topGen‘ran (,)) = (topGen‘ran (,))
6633, 65rerest 22324 . . . . . . . . . . . . 13 ((𝐴[,]𝐵) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))
6764, 66syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))
6861, 67eqtrd 2548 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (((TopOpen‘ℂfld) ↾t 𝐷) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))
6968oveq1d 6441 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((((TopOpen‘ℂfld) ↾t 𝐷) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)) = (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
7055, 69eleqtrd 2594 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)))
7136a1i 11 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
72 df-ima 4945 . . . . . . . . . . . 12 (𝐹 “ (𝐴[,]𝐵)) = ran (𝐹 ↾ (𝐴[,]𝐵))
7372eqimss2i 3527 . . . . . . . . . . 11 ran (𝐹 ↾ (𝐴[,]𝐵)) ⊆ (𝐹 “ (𝐴[,]𝐵))
7473a1i 11 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ran (𝐹 ↾ (𝐴[,]𝐵)) ⊆ (𝐹 “ (𝐴[,]𝐵)))
75 ax-resscn 9748 . . . . . . . . . . 11 ℝ ⊆ ℂ
7624, 75syl6ss 3484 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 “ (𝐴[,]𝐵)) ⊆ ℂ)
77 cnrest2 20803 . . . . . . . . . 10 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ ran (𝐹 ↾ (𝐴[,]𝐵)) ⊆ (𝐹 “ (𝐴[,]𝐵)) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℂ) → ((𝐹 ↾ (𝐴[,]𝐵)) ∈ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐹 ↾ (𝐴[,]𝐵)) ∈ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn ((TopOpen‘ℂfld) ↾t (𝐹 “ (𝐴[,]𝐵))))))
7871, 74, 76, 77syl3anc 1317 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝐹 ↾ (𝐴[,]𝐵)) ∈ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld)) ↔ (𝐹 ↾ (𝐴[,]𝐵)) ∈ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn ((TopOpen‘ℂfld) ↾t (𝐹 “ (𝐴[,]𝐵))))))
7970, 78mpbid 220 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn ((TopOpen‘ℂfld) ↾t (𝐹 “ (𝐴[,]𝐵)))))
8033, 65rerest 22324 . . . . . . . . . 10 ((𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (𝐹 “ (𝐴[,]𝐵))) = ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))))
8124, 80syl 17 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((TopOpen‘ℂfld) ↾t (𝐹 “ (𝐴[,]𝐵))) = ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))))
8281oveq2d 6442 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn ((TopOpen‘ℂfld) ↾t (𝐹 “ (𝐴[,]𝐵)))) = (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵)))))
8379, 82eleqtrd 2594 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵)))))
84 eqid 2514 . . . . . . . 8 ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) = ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵)))
8584cnconn 20938 . . . . . . 7 ((((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Con ∧ (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)–onto ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) ∧ (𝐹 ↾ (𝐴[,]𝐵)) ∈ (((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) Cn ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))))) → ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) ∈ Con)
869, 30, 83, 85syl3anc 1317 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) ∈ Con)
87 reconn 22348 . . . . . . . . 9 ((𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ → (((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) ∈ Con ↔ ∀𝑥 ∈ (𝐹 “ (𝐴[,]𝐵))∀𝑦 ∈ (𝐹 “ (𝐴[,]𝐵))(𝑥[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵))))
88873ad2ant2 1075 . . . . . . . 8 ((𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))) → (((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) ∈ Con ↔ ∀𝑥 ∈ (𝐹 “ (𝐴[,]𝐵))∀𝑦 ∈ (𝐹 “ (𝐴[,]𝐵))(𝑥[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵))))
89883ad2ant3 1076 . . . . . . 7 (((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → (((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) ∈ Con ↔ ∀𝑥 ∈ (𝐹 “ (𝐴[,]𝐵))∀𝑦 ∈ (𝐹 “ (𝐴[,]𝐵))(𝑥[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵))))
90893ad2ant3 1076 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (((topGen‘ran (,)) ↾t (𝐹 “ (𝐴[,]𝐵))) ∈ Con ↔ ∀𝑥 ∈ (𝐹 “ (𝐴[,]𝐵))∀𝑦 ∈ (𝐹 “ (𝐴[,]𝐵))(𝑥[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵))))
9186, 90mpbid 220 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ∀𝑥 ∈ (𝐹 “ (𝐴[,]𝐵))∀𝑦 ∈ (𝐹 “ (𝐴[,]𝐵))(𝑥[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵)))
92 simp11 1083 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐴 ∈ ℝ)
9392rexrd 9844 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐴 ∈ ℝ*)
94 simp12 1084 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐵 ∈ ℝ)
9594rexrd 9844 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐵 ∈ ℝ*)
96 ltle 9876 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴𝐵))
9796imp 443 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < 𝐵) → 𝐴𝐵)
98973adantl3 1211 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵) → 𝐴𝐵)
99983adant3 1073 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐴𝐵)
100 lbicc2 12028 . . . . . . . 8 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
10193, 95, 99, 100syl3anc 1317 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐴 ∈ (𝐴[,]𝐵))
102 funfvima2 6274 . . . . . . 7 ((Fun 𝐹 ∧ (𝐴[,]𝐵) ⊆ dom 𝐹) → (𝐴 ∈ (𝐴[,]𝐵) → (𝐹𝐴) ∈ (𝐹 “ (𝐴[,]𝐵))))
10320, 101, 102sylc 62 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹𝐴) ∈ (𝐹 “ (𝐴[,]𝐵)))
104 ubicc2 12029 . . . . . . . 8 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
10593, 95, 99, 104syl3anc 1317 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝐵 ∈ (𝐴[,]𝐵))
106 funfvima2 6274 . . . . . . 7 ((Fun 𝐹 ∧ (𝐴[,]𝐵) ⊆ dom 𝐹) → (𝐵 ∈ (𝐴[,]𝐵) → (𝐹𝐵) ∈ (𝐹 “ (𝐴[,]𝐵))))
10720, 105, 106sylc 62 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹𝐵) ∈ (𝐹 “ (𝐴[,]𝐵)))
108 oveq1 6433 . . . . . . . 8 (𝑥 = (𝐹𝐴) → (𝑥[,]𝑦) = ((𝐹𝐴)[,]𝑦))
109108sseq1d 3499 . . . . . . 7 (𝑥 = (𝐹𝐴) → ((𝑥[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵)) ↔ ((𝐹𝐴)[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵))))
110 oveq2 6434 . . . . . . . 8 (𝑦 = (𝐹𝐵) → ((𝐹𝐴)[,]𝑦) = ((𝐹𝐴)[,](𝐹𝐵)))
111110sseq1d 3499 . . . . . . 7 (𝑦 = (𝐹𝐵) → (((𝐹𝐴)[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵)) ↔ ((𝐹𝐴)[,](𝐹𝐵)) ⊆ (𝐹 “ (𝐴[,]𝐵))))
112109, 111rspc2v 3197 . . . . . 6 (((𝐹𝐴) ∈ (𝐹 “ (𝐴[,]𝐵)) ∧ (𝐹𝐵) ∈ (𝐹 “ (𝐴[,]𝐵))) → (∀𝑥 ∈ (𝐹 “ (𝐴[,]𝐵))∀𝑦 ∈ (𝐹 “ (𝐴[,]𝐵))(𝑥[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵)) → ((𝐹𝐴)[,](𝐹𝐵)) ⊆ (𝐹 “ (𝐴[,]𝐵))))
113103, 107, 112syl2anc 690 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (∀𝑥 ∈ (𝐹 “ (𝐴[,]𝐵))∀𝑦 ∈ (𝐹 “ (𝐴[,]𝐵))(𝑥[,]𝑦) ⊆ (𝐹 “ (𝐴[,]𝐵)) → ((𝐹𝐴)[,](𝐹𝐵)) ⊆ (𝐹 “ (𝐴[,]𝐵))))
11491, 113mpd 15 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝐹𝐴)[,](𝐹𝐵)) ⊆ (𝐹 “ (𝐴[,]𝐵)))
115 ioossicc 11999 . . . . . . . 8 ((𝐹𝐴)(,)(𝐹𝐵)) ⊆ ((𝐹𝐴)[,](𝐹𝐵))
116115sseli 3468 . . . . . . 7 (𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)) → 𝑈 ∈ ((𝐹𝐴)[,](𝐹𝐵)))
1171163ad2ant3 1076 . . . . . 6 ((𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))) → 𝑈 ∈ ((𝐹𝐴)[,](𝐹𝐵)))
1181173ad2ant3 1076 . . . . 5 (((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))) → 𝑈 ∈ ((𝐹𝐴)[,](𝐹𝐵)))
1191183ad2ant3 1076 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝑈 ∈ ((𝐹𝐴)[,](𝐹𝐵)))
120114, 119sseldd 3473 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝑈 ∈ (𝐹 “ (𝐴[,]𝐵)))
121 fvelima 6042 . . 3 ((Fun 𝐹𝑈 ∈ (𝐹 “ (𝐴[,]𝐵))) → ∃𝑥 ∈ (𝐴[,]𝐵)(𝐹𝑥) = 𝑈)
1226, 120, 121syl2anc 690 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ∃𝑥 ∈ (𝐴[,]𝐵)(𝐹𝑥) = 𝑈)
123 simpl1 1056 . . . . . . . 8 (((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈) → 𝑥 ∈ ℝ*)
124123a1i 11 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈) → 𝑥 ∈ ℝ*))
125 simprr 791 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → (𝐹𝑥) = 𝑈)
12624, 103sseldd 3473 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹𝐴) ∈ ℝ)
127 simp333 1208 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)))
128126rexrd 9844 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹𝐴) ∈ ℝ*)
12924, 107sseldd 3473 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹𝐵) ∈ ℝ)
130129rexrd 9844 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹𝐵) ∈ ℝ*)
131 elioo2 11956 . . . . . . . . . . . . . . . . 17 (((𝐹𝐴) ∈ ℝ* ∧ (𝐹𝐵) ∈ ℝ*) → (𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)) ↔ (𝑈 ∈ ℝ ∧ (𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵))))
132128, 130, 131syl2anc 690 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵)) ↔ (𝑈 ∈ ℝ ∧ (𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵))))
133127, 132mpbid 220 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝑈 ∈ ℝ ∧ (𝐹𝐴) < 𝑈𝑈 < (𝐹𝐵)))
134133simp2d 1066 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝐹𝐴) < 𝑈)
135126, 134gtned 9923 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝑈 ≠ (𝐹𝐴))
136135adantr 479 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → 𝑈 ≠ (𝐹𝐴))
137125, 136eqnetrd 2753 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → (𝐹𝑥) ≠ (𝐹𝐴))
138137neneqd 2691 . . . . . . . . . 10 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → ¬ (𝐹𝑥) = (𝐹𝐴))
139 fveq2 5987 . . . . . . . . . 10 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
140138, 139nsyl 133 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → ¬ 𝑥 = 𝐴)
141 simp13 1085 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝑈 ∈ ℝ)
142133simp3d 1067 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝑈 < (𝐹𝐵))
143141, 142ltned 9924 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → 𝑈 ≠ (𝐹𝐵))
144143adantr 479 . . . . . . . . . . . 12 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → 𝑈 ≠ (𝐹𝐵))
145125, 144eqnetrd 2753 . . . . . . . . . . 11 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → (𝐹𝑥) ≠ (𝐹𝐵))
146145neneqd 2691 . . . . . . . . . 10 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → ¬ (𝐹𝑥) = (𝐹𝐵))
147 fveq2 5987 . . . . . . . . . 10 (𝑥 = 𝐵 → (𝐹𝑥) = (𝐹𝐵))
148146, 147nsyl 133 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → ¬ 𝑥 = 𝐵)
149 simprl3 1100 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵))
150140, 148, 149ecase13d 31312 . . . . . . . 8 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) ∧ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)) → (𝐴 < 𝑥𝑥 < 𝐵))
151150ex 448 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈) → (𝐴 < 𝑥𝑥 < 𝐵)))
152124, 151jcad 553 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈) → (𝑥 ∈ ℝ* ∧ (𝐴 < 𝑥𝑥 < 𝐵))))
153 3anass 1034 . . . . . 6 ((𝑥 ∈ ℝ*𝐴 < 𝑥𝑥 < 𝐵) ↔ (𝑥 ∈ ℝ* ∧ (𝐴 < 𝑥𝑥 < 𝐵)))
154152, 153syl6ibr 240 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈) → (𝑥 ∈ ℝ*𝐴 < 𝑥𝑥 < 𝐵)))
155 rexr 9840 . . . . . . . . 9 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
156 rexr 9840 . . . . . . . . 9 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
157 elicc3 31316 . . . . . . . . 9 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵))))
158155, 156, 157syl2an 492 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵))))
1591583adant3 1073 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵))))
1601593ad2ant1 1074 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵))))
161160anbi1d 736 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝑥 ∈ (𝐴[,]𝐵) ∧ (𝐹𝑥) = 𝑈) ↔ ((𝑥 ∈ ℝ*𝐴𝐵 ∧ (𝑥 = 𝐴 ∨ (𝐴 < 𝑥𝑥 < 𝐵) ∨ 𝑥 = 𝐵)) ∧ (𝐹𝑥) = 𝑈)))
162 elioo1 11955 . . . . . . . 8 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝑥 ∈ (𝐴(,)𝐵) ↔ (𝑥 ∈ ℝ*𝐴 < 𝑥𝑥 < 𝐵)))
163155, 156, 162syl2an 492 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴(,)𝐵) ↔ (𝑥 ∈ ℝ*𝐴 < 𝑥𝑥 < 𝐵)))
1641633adant3 1073 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) → (𝑥 ∈ (𝐴(,)𝐵) ↔ (𝑥 ∈ ℝ*𝐴 < 𝑥𝑥 < 𝐵)))
1651643ad2ant1 1074 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (𝑥 ∈ (𝐴(,)𝐵) ↔ (𝑥 ∈ ℝ*𝐴 < 𝑥𝑥 < 𝐵)))
166154, 161, 1653imtr4d 281 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝑥 ∈ (𝐴[,]𝐵) ∧ (𝐹𝑥) = 𝑈) → 𝑥 ∈ (𝐴(,)𝐵)))
167 simpr 475 . . . . 5 ((𝑥 ∈ (𝐴[,]𝐵) ∧ (𝐹𝑥) = 𝑈) → (𝐹𝑥) = 𝑈)
168167a1i 11 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝑥 ∈ (𝐴[,]𝐵) ∧ (𝐹𝑥) = 𝑈) → (𝐹𝑥) = 𝑈))
169166, 168jcad 553 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ((𝑥 ∈ (𝐴[,]𝐵) ∧ (𝐹𝑥) = 𝑈) → (𝑥 ∈ (𝐴(,)𝐵) ∧ (𝐹𝑥) = 𝑈)))
170169reximdv2 2901 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → (∃𝑥 ∈ (𝐴[,]𝐵)(𝐹𝑥) = 𝑈 → ∃𝑥 ∈ (𝐴(,)𝐵)(𝐹𝑥) = 𝑈))
171122, 170mpd 15 1 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹𝐴)(,)(𝐹𝐵))))) → ∃𝑥 ∈ (𝐴(,)𝐵)(𝐹𝑥) = 𝑈)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3o 1029  w3a 1030   = wceq 1474  wcel 1938  wne 2684  wral 2800  wrex 2801  Vcvv 3077  wss 3444   cuni 4270   class class class wbr 4481  dom cdm 4932  ran crn 4933  cres 4934  cima 4935  Fun wfun 5683  wf 5685  ontowfo 5687  cfv 5689  (class class class)co 6426  cc 9689  cr 9690  *cxr 9828   < clt 9829  cle 9830  (,)cioo 11915  [,]cicc 11918  t crest 15788  TopOpenctopn 15789  topGenctg 15805  fldccnfld 19471  Topctop 20420  TopOnctopon 20421   Cn ccn 20741  Conccon 20927  cnccncf 22410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6723  ax-cnex 9747  ax-resscn 9748  ax-1cn 9749  ax-icn 9750  ax-addcl 9751  ax-addrcl 9752  ax-mulcl 9753  ax-mulrcl 9754  ax-mulcom 9755  ax-addass 9756  ax-mulass 9757  ax-distr 9758  ax-i2m1 9759  ax-1ne0 9760  ax-1rid 9761  ax-rnegex 9762  ax-rrecex 9763  ax-cnre 9764  ax-pre-lttri 9765  ax-pre-lttrn 9766  ax-pre-ltadd 9767  ax-pre-mulgt0 9768  ax-pre-sup 9769
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-riota 6388  df-ov 6429  df-oprab 6430  df-mpt2 6431  df-om 6834  df-1st 6934  df-2nd 6935  df-wrecs 7169  df-recs 7231  df-rdg 7269  df-1o 7323  df-oadd 7327  df-er 7505  df-map 7622  df-en 7718  df-dom 7719  df-sdom 7720  df-fin 7721  df-fi 8076  df-sup 8107  df-inf 8108  df-pnf 9831  df-mnf 9832  df-xr 9833  df-ltxr 9834  df-le 9835  df-sub 10019  df-neg 10020  df-div 10434  df-nn 10776  df-2 10834  df-3 10835  df-4 10836  df-5 10837  df-6 10838  df-7 10839  df-8 10840  df-9 10841  df-n0 11048  df-z 11119  df-dec 11234  df-uz 11428  df-q 11531  df-rp 11575  df-xneg 11688  df-xadd 11689  df-xmul 11690  df-ioo 11919  df-ico 11921  df-icc 11922  df-fz 12066  df-seq 12532  df-exp 12591  df-cj 13546  df-re 13547  df-im 13548  df-sqrt 13682  df-abs 13683  df-struct 15581  df-ndx 15582  df-slot 15583  df-base 15584  df-plusg 15665  df-mulr 15666  df-starv 15667  df-tset 15671  df-ple 15672  df-ds 15675  df-unif 15676  df-rest 15790  df-topn 15791  df-topgen 15811  df-psmet 19463  df-xmet 19464  df-met 19465  df-bl 19466  df-mopn 19467  df-cnfld 19472  df-top 20424  df-bases 20425  df-topon 20426  df-topsp 20427  df-cld 20536  df-cn 20744  df-cnp 20745  df-con 20928  df-xms 21837  df-ms 21838  df-cncf 22412
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator