cncmpmax

Description: When the hypothesis for the extreme value theorem hold, then the sup of the range of the function belongs to the range, it is real and it an upper bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	cncmpmax.1	$⊢ T = ⋃ J$
	cncmpmax.2	$⊢ K = topGen (ran (.))$
	cncmpmax.3	$⊢ φ \to J \in Comp$
	cncmpmax.4	$⊢ φ \to F \in (J Cn K)$
	cncmpmax.5	$⊢ φ \to T \neq \emptyset$
Assertion	cncmpmax	$⊢ φ \to (sup (ran F ℝ <) \in ran F \land sup (ran F ℝ <) \in ℝ \land \forall t \in T F (t) \leq sup (ran F ℝ <))$

Proof

Step	Hyp	Ref	Expression
1		cncmpmax.1	$⊢ T = ⋃ J$
2		cncmpmax.2	$⊢ K = topGen (ran (.))$
3		cncmpmax.3	$⊢ φ \to J \in Comp$
4		cncmpmax.4	$⊢ φ \to F \in (J Cn K)$
5		cncmpmax.5	$⊢ φ \to T \neq \emptyset$
6	1 2 3 4 5	evth	$⊢ φ \to \exists x \in T \forall t \in T F (t) \leq F (x)$
7		eqid	$⊢ J Cn K = J Cn K$
8	2 1 7 4	fcnre	$⊢ φ \to F : T ⟶ ℝ$
9	8	frnd	$⊢ φ \to ran F \subseteq ℝ$
10	9	adantr	$⊢ (φ \land (x \in T \land \forall t \in T F (t) \leq F (x))) \to ran F \subseteq ℝ$
11	8	ffund	$⊢ φ \to Fun F$
12	11	adantr	$⊢ (φ \land x \in T) \to Fun F$
13		simpr	$⊢ (φ \land x \in T) \to x \in T$
14	8	adantr	$⊢ (φ \land x \in T) \to F : T ⟶ ℝ$
15	14	fdmd	$⊢ (φ \land x \in T) \to dom F = T$
16	13 15	eleqtrrd	$⊢ (φ \land x \in T) \to x \in dom F$
17		fvelrn	$⊢ (Fun F \land x \in dom F) \to F (x) \in ran F$
18	12 16 17	syl2anc	$⊢ (φ \land x \in T) \to F (x) \in ran F$
19	18	adantrr	$⊢ (φ \land (x \in T \land \forall t \in T F (t) \leq F (x))) \to F (x) \in ran F$
20		ffn	$⊢ F : T ⟶ ℝ \to F Fn T$
21		fvelrnb	$⊢ F Fn T \to (y \in ran F \leftrightarrow \exists s \in T F (s) = y)$
22	8 20 21	3syl	$⊢ φ \to (y \in ran F \leftrightarrow \exists s \in T F (s) = y)$
23	22	biimpa	$⊢ (φ \land y \in ran F) \to \exists s \in T F (s) = y$
24		df-rex	$⊢ \exists s \in T F (s) = y \leftrightarrow \exists s (s \in T \land F (s) = y)$
25	23 24	sylib	$⊢ (φ \land y \in ran F) \to \exists s (s \in T \land F (s) = y)$
26	25	adantlr	$⊢ ((φ \land \forall t \in T F (t) \leq F (x)) \land y \in ran F) \to \exists s (s \in T \land F (s) = y)$
27		simprr	$⊢ (((φ \land \forall t \in T F (t) \leq F (x)) \land y \in ran F) \land (s \in T \land F (s) = y)) \to F (s) = y$
28		simpllr	$⊢ (((φ \land \forall t \in T F (t) \leq F (x)) \land y \in ran F) \land (s \in T \land F (s) = y)) \to \forall t \in T F (t) \leq F (x)$
29		simprl	$⊢ (((φ \land \forall t \in T F (t) \leq F (x)) \land y \in ran F) \land (s \in T \land F (s) = y)) \to s \in T$
30		fveq2	$⊢ t = s \to F (t) = F (s)$
31	30	breq1d	$⊢ t = s \to (F (t) \leq F (x) \leftrightarrow F (s) \leq F (x))$
32	31	rspccva	$⊢ (\forall t \in T F (t) \leq F (x) \land s \in T) \to F (s) \leq F (x)$
33	28 29 32	syl2anc	$⊢ (((φ \land \forall t \in T F (t) \leq F (x)) \land y \in ran F) \land (s \in T \land F (s) = y)) \to F (s) \leq F (x)$
34	27 33	eqbrtrrd	$⊢ (((φ \land \forall t \in T F (t) \leq F (x)) \land y \in ran F) \land (s \in T \land F (s) = y)) \to y \leq F (x)$
35	26 34	exlimddv	$⊢ ((φ \land \forall t \in T F (t) \leq F (x)) \land y \in ran F) \to y \leq F (x)$
36	35	ralrimiva	$⊢ (φ \land \forall t \in T F (t) \leq F (x)) \to \forall y \in ran F y \leq F (x)$
37	36	adantrl	$⊢ (φ \land (x \in T \land \forall t \in T F (t) \leq F (x))) \to \forall y \in ran F y \leq F (x)$
38		ubelsupr	$⊢ (ran F \subseteq ℝ \land F (x) \in ran F \land \forall y \in ran F y \leq F (x)) \to F (x) = sup (ran F ℝ <)$
39	10 19 37 38	syl3anc	$⊢ (φ \land (x \in T \land \forall t \in T F (t) \leq F (x))) \to F (x) = sup (ran F ℝ <)$
40	39	eqcomd	$⊢ (φ \land (x \in T \land \forall t \in T F (t) \leq F (x))) \to sup (ran F ℝ <) = F (x)$
41	40 19	eqeltrd	$⊢ (φ \land (x \in T \land \forall t \in T F (t) \leq F (x))) \to sup (ran F ℝ <) \in ran F$
42	10 41	sseldd	$⊢ (φ \land (x \in T \land \forall t \in T F (t) \leq F (x))) \to sup (ran F ℝ <) \in ℝ$
43		simplrr	$⊢ ((φ \land (x \in T \land \forall t \in T F (t) \leq F (x))) \land s \in T) \to \forall t \in T F (t) \leq F (x)$
44	43 32	sylancom	$⊢ ((φ \land (x \in T \land \forall t \in T F (t) \leq F (x))) \land s \in T) \to F (s) \leq F (x)$
45	40	adantr	$⊢ ((φ \land (x \in T \land \forall t \in T F (t) \leq F (x))) \land s \in T) \to sup (ran F ℝ <) = F (x)$
46	44 45	breqtrrd	$⊢ ((φ \land (x \in T \land \forall t \in T F (t) \leq F (x))) \land s \in T) \to F (s) \leq sup (ran F ℝ <)$
47	46	ralrimiva	$⊢ (φ \land (x \in T \land \forall t \in T F (t) \leq F (x))) \to \forall s \in T F (s) \leq sup (ran F ℝ <)$
48	30	breq1d	$⊢ t = s \to (F (t) \leq sup (ran F ℝ <) \leftrightarrow F (s) \leq sup (ran F ℝ <))$
49	48	cbvralvw	$⊢ \forall t \in T F (t) \leq sup (ran F ℝ <) \leftrightarrow \forall s \in T F (s) \leq sup (ran F ℝ <)$
50	47 49	sylibr	$⊢ (φ \land (x \in T \land \forall t \in T F (t) \leq F (x))) \to \forall t \in T F (t) \leq sup (ran F ℝ <)$
51	41 42 50	3jca	$⊢ (φ \land (x \in T \land \forall t \in T F (t) \leq F (x))) \to (sup (ran F ℝ <) \in ran F \land sup (ran F ℝ <) \in ℝ \land \forall t \in T F (t) \leq sup (ran F ℝ <))$
52	6 51	rexlimddv	$⊢ φ \to (sup (ran F ℝ <) \in ran F \land sup (ran F ℝ <) \in ℝ \land \forall t \in T F (t) \leq sup (ran F ℝ <))$

Metamath Proof Explorer

Theorem cncmpmax

Proof