evthicc2

Description: Combine ivthicc with evthicc to exactly describe the image of a closed interval. (Contributed by Mario Carneiro, 19-Feb-2015)

	Ref	Expression
Hypotheses	evthicc.1	$⊢ φ \to A \in ℝ$
	evthicc.2	$⊢ φ \to B \in ℝ$
	evthicc.3	$⊢ φ \to A \leq B$
	evthicc.4	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
Assertion	evthicc2	$⊢ φ \to \exists x \in ℝ \exists y \in ℝ ran F = [x, y]$

Proof

Step	Hyp	Ref	Expression
1		evthicc.1	$⊢ φ \to A \in ℝ$
2		evthicc.2	$⊢ φ \to B \in ℝ$
3		evthicc.3	$⊢ φ \to A \leq B$
4		evthicc.4	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
5	1 2 3 4	evthicc	$⊢ φ \to (\exists a \in [A, B] \forall z \in [A, B] F (z) \leq F (a) \land \exists b \in [A, B] \forall z \in [A, B] F (b) \leq F (z))$
6		reeanv	$⊢ \exists a \in [A, B] \exists b \in [A, B] (\forall z \in [A, B] F (z) \leq F (a) \land \forall z \in [A, B] F (b) \leq F (z)) \leftrightarrow (\exists a \in [A, B] \forall z \in [A, B] F (z) \leq F (a) \land \exists b \in [A, B] \forall z \in [A, B] F (b) \leq F (z))$
7	5 6	sylibr	$⊢ φ \to \exists a \in [A, B] \exists b \in [A, B] (\forall z \in [A, B] F (z) \leq F (a) \land \forall z \in [A, B] F (b) \leq F (z))$
8		r19.26	$⊢ \forall z \in [A, B] (F (z) \leq F (a) \land F (b) \leq F (z)) \leftrightarrow (\forall z \in [A, B] F (z) \leq F (a) \land \forall z \in [A, B] F (b) \leq F (z))$
9	4	adantr	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to F : [A, B] \underset{cn}{⟶} ℝ$
10		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℝ \to F : [A, B] ⟶ ℝ$
11	9 10	syl	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to F : [A, B] ⟶ ℝ$
12		simprr	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to b \in [A, B]$
13	11 12	ffvelrnd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to F (b) \in ℝ$
14	13	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land \forall z \in [A, B] (F (z) \leq F (a) \land F (b) \leq F (z))) \to F (b) \in ℝ$
15		simprl	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to a \in [A, B]$
16	11 15	ffvelrnd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to F (a) \in ℝ$
17	16	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land \forall z \in [A, B] (F (z) \leq F (a) \land F (b) \leq F (z))) \to F (a) \in ℝ$
18	11	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land \forall z \in [A, B] (F (z) \leq F (a) \land F (b) \leq F (z))) \to F : [A, B] ⟶ ℝ$
19	18	ffnd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land \forall z \in [A, B] (F (z) \leq F (a) \land F (b) \leq F (z))) \to F Fn [A, B]$
20	16	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land z \in [A, B]) \to F (a) \in ℝ$
21		elicc2	$⊢ (F (b) \in ℝ \land F (a) \in ℝ) \to (F (z) \in [F (b), F (a)] \leftrightarrow (F (z) \in ℝ \land F (b) \leq F (z) \land F (z) \leq F (a)))$
22	13 20 21	syl2an2r	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land z \in [A, B]) \to (F (z) \in [F (b), F (a)] \leftrightarrow (F (z) \in ℝ \land F (b) \leq F (z) \land F (z) \leq F (a)))$
23		3anass	$⊢ (F (z) \in ℝ \land F (b) \leq F (z) \land F (z) \leq F (a)) \leftrightarrow (F (z) \in ℝ \land (F (b) \leq F (z) \land F (z) \leq F (a)))$
24	22 23	bitrdi	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land z \in [A, B]) \to (F (z) \in [F (b), F (a)] \leftrightarrow (F (z) \in ℝ \land (F (b) \leq F (z) \land F (z) \leq F (a))))$
25		ancom	$⊢ (F (z) \leq F (a) \land F (b) \leq F (z)) \leftrightarrow (F (b) \leq F (z) \land F (z) \leq F (a))$
26	11	ffvelrnda	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land z \in [A, B]) \to F (z) \in ℝ$
27	26	biantrurd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land z \in [A, B]) \to ((F (b) \leq F (z) \land F (z) \leq F (a)) \leftrightarrow (F (z) \in ℝ \land (F (b) \leq F (z) \land F (z) \leq F (a))))$
28	25 27	syl5bb	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land z \in [A, B]) \to ((F (z) \leq F (a) \land F (b) \leq F (z)) \leftrightarrow (F (z) \in ℝ \land (F (b) \leq F (z) \land F (z) \leq F (a))))$
29	24 28	bitr4d	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land z \in [A, B]) \to (F (z) \in [F (b), F (a)] \leftrightarrow (F (z) \leq F (a) \land F (b) \leq F (z)))$
30	29	ralbidva	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to (\forall z \in [A, B] F (z) \in [F (b), F (a)] \leftrightarrow \forall z \in [A, B] (F (z) \leq F (a) \land F (b) \leq F (z)))$
31	30	biimpar	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land \forall z \in [A, B] (F (z) \leq F (a) \land F (b) \leq F (z))) \to \forall z \in [A, B] F (z) \in [F (b), F (a)]$
32		ffnfv	$⊢ F : [A, B] ⟶ [F (b), F (a)] \leftrightarrow (F Fn [A, B] \land \forall z \in [A, B] F (z) \in [F (b), F (a)])$
33	19 31 32	sylanbrc	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land \forall z \in [A, B] (F (z) \leq F (a) \land F (b) \leq F (z))) \to F : [A, B] ⟶ [F (b), F (a)]$
34	33	frnd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land \forall z \in [A, B] (F (z) \leq F (a) \land F (b) \leq F (z))) \to ran F \subseteq [F (b), F (a)]$
35	1	adantr	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to A \in ℝ$
36	2	adantr	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to B \in ℝ$
37		ssidd	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to [A, B] \subseteq [A, B]$
38		ax-resscn	$⊢ ℝ \subseteq ℂ$
39		ssid	$⊢ ℂ \subseteq ℂ$
40		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to [A, B] \underset{cn}{⟶} ℝ \subseteq [A, B] \underset{cn}{⟶} ℂ$
41	38 39 40	mp2an	$⊢ [A, B] \underset{cn}{⟶} ℝ \subseteq [A, B] \underset{cn}{⟶} ℂ$
42	41 9	sseldi	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to F : [A, B] \underset{cn}{⟶} ℂ$
43	11	ffvelrnda	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land x \in [A, B]) \to F (x) \in ℝ$
44	35 36 12 15 37 42 43	ivthicc	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to [F (b), F (a)] \subseteq ran F$
45	44	adantr	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land \forall z \in [A, B] (F (z) \leq F (a) \land F (b) \leq F (z))) \to [F (b), F (a)] \subseteq ran F$
46	34 45	eqssd	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land \forall z \in [A, B] (F (z) \leq F (a) \land F (b) \leq F (z))) \to ran F = [F (b), F (a)]$
47		rspceov	$⊢ (F (b) \in ℝ \land F (a) \in ℝ \land ran F = [F (b), F (a)]) \to \exists x \in ℝ \exists y \in ℝ ran F = [x, y]$
48	14 17 46 47	syl3anc	$⊢ ((φ \land (a \in [A, B] \land b \in [A, B])) \land \forall z \in [A, B] (F (z) \leq F (a) \land F (b) \leq F (z))) \to \exists x \in ℝ \exists y \in ℝ ran F = [x, y]$
49	48	ex	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to (\forall z \in [A, B] (F (z) \leq F (a) \land F (b) \leq F (z)) \to \exists x \in ℝ \exists y \in ℝ ran F = [x, y])$
50	8 49	syl5bir	$⊢ (φ \land (a \in [A, B] \land b \in [A, B])) \to ((\forall z \in [A, B] F (z) \leq F (a) \land \forall z \in [A, B] F (b) \leq F (z)) \to \exists x \in ℝ \exists y \in ℝ ran F = [x, y])$
51	50	rexlimdvva	$⊢ φ \to (\exists a \in [A, B] \exists b \in [A, B] (\forall z \in [A, B] F (z) \leq F (a) \land \forall z \in [A, B] F (b) \leq F (z)) \to \exists x \in ℝ \exists y \in ℝ ran F = [x, y])$
52	7 51	mpd	$⊢ φ \to \exists x \in ℝ \exists y \in ℝ ran F = [x, y]$

Metamath Proof Explorer

Theorem evthicc2

Proof