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	$⊢ ((A \in ℝ \land B \in ℝ \land U \in ℝ) \land A < B \land ([A, B] \subseteq D \land D \subseteq ℂ \land (F : D \underset{cn}{⟶} ℂ \land F [[A, B]] \subseteq ℝ \land U \in (F (A), F (B))))) \to \exists x \in (A, B) F (x) = U$

Proof

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

Metamath Proof Explorer

Theorem ivthALT

Proof