stoweidlem29

Description: When the hypothesis for the extreme value theorem hold, then the inf of the range of the function belongs to the range, it is real and it a lower bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017) (Revised by AV, 13-Sep-2020)

	Ref	Expression
Hypotheses	stoweidlem29.1	$⊢ \underline{Ⅎ} t F$
	stoweidlem29.2	$⊢ Ⅎ t φ$
	stoweidlem29.3	$⊢ T = ⋃ J$
	stoweidlem29.4	$⊢ K = topGen (ran (.))$
	stoweidlem29.5	$⊢ φ \to J \in Comp$
	stoweidlem29.6	$⊢ φ \to F \in (J Cn K)$
	stoweidlem29.7	$⊢ φ \to T \neq \emptyset$
Assertion	stoweidlem29	$⊢ φ \to (inf (ran F ℝ <) \in ran F \land inf (ran F ℝ <) \in ℝ \land \forall t \in T inf (ran F ℝ <) \leq F (t))$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem29.1	$⊢ \underline{Ⅎ} t F$
2		stoweidlem29.2	$⊢ Ⅎ t φ$
3		stoweidlem29.3	$⊢ T = ⋃ J$
4		stoweidlem29.4	$⊢ K = topGen (ran (.))$
5		stoweidlem29.5	$⊢ φ \to J \in Comp$
6		stoweidlem29.6	$⊢ φ \to F \in (J Cn K)$
7		stoweidlem29.7	$⊢ φ \to T \neq \emptyset$
8		eqid	$⊢ J Cn K = J Cn K$
9	4 3 8 6	fcnre	$⊢ φ \to F : T ⟶ ℝ$
10		df-f	$⊢ F : T ⟶ ℝ \leftrightarrow (F Fn T \land ran F \subseteq ℝ)$
11	9 10	sylib	$⊢ φ \to (F Fn T \land ran F \subseteq ℝ)$
12	11	simprd	$⊢ φ \to ran F \subseteq ℝ$
13	11	simpld	$⊢ φ \to F Fn T$
14		fnfun	$⊢ F Fn T \to Fun F$
15	13 14	syl	$⊢ φ \to Fun F$
16	15	adantr	$⊢ (φ \land s \in T) \to Fun F$
17	9	fdmd	$⊢ φ \to dom F = T$
18	17	eqcomd	$⊢ φ \to T = dom F$
19	18	eleq2d	$⊢ φ \to (s \in T \leftrightarrow s \in dom F)$
20	19	biimpa	$⊢ (φ \land s \in T) \to s \in dom F$
21		fvelrn	$⊢ (Fun F \land s \in dom F) \to F (s) \in ran F$
22	16 20 21	syl2anc	$⊢ (φ \land s \in T) \to F (s) \in ran F$
23		nfcv	$⊢ \underline{Ⅎ} t s$
24	1 23	nffv	$⊢ \underline{Ⅎ} t F (s)$
25	24	nfeq2	$⊢ Ⅎ t x = F (s)$
26		breq1	$⊢ x = F (s) \to (x \leq F (t) \leftrightarrow F (s) \leq F (t))$
27	25 26	ralbid	$⊢ x = F (s) \to (\forall t \in T x \leq F (t) \leftrightarrow \forall t \in T F (s) \leq F (t))$
28	27	rspcev	$⊢ (F (s) \in ran F \land \forall t \in T F (s) \leq F (t)) \to \exists x \in ran F \forall t \in T x \leq F (t)$
29	22 28	sylan	$⊢ ((φ \land s \in T) \land \forall t \in T F (s) \leq F (t)) \to \exists x \in ran F \forall t \in T x \leq F (t)$
30		nfcv	$⊢ \underline{Ⅎ} s F$
31		nfcv	$⊢ \underline{Ⅎ} s T$
32		nfcv	$⊢ \underline{Ⅎ} t T$
33	30 1 31 32 3 4 5 6 7	evth2f	$⊢ φ \to \exists s \in T \forall t \in T F (s) \leq F (t)$
34	29 33	r19.29a	$⊢ φ \to \exists x \in ran F \forall t \in T x \leq F (t)$
35		nfv	$⊢ Ⅎ y (φ \land \forall t \in T x \leq F (t))$
36		simpr	$⊢ ((φ \land \forall t \in T x \leq F (t)) \land y \in ran F) \to y \in ran F$
37	13	ad2antrr	$⊢ ((φ \land \forall t \in T x \leq F (t)) \land y \in ran F) \to F Fn T$
38		nfcv	$⊢ \underline{Ⅎ} t y$
39	32 38 1	fvelrnbf	$⊢ F Fn T \to (y \in ran F \leftrightarrow \exists t \in T F (t) = y)$
40	37 39	syl	$⊢ ((φ \land \forall t \in T x \leq F (t)) \land y \in ran F) \to (y \in ran F \leftrightarrow \exists t \in T F (t) = y)$
41	36 40	mpbid	$⊢ ((φ \land \forall t \in T x \leq F (t)) \land y \in ran F) \to \exists t \in T F (t) = y$
42		nfra1	$⊢ Ⅎ t \forall t \in T x \leq F (t)$
43	2 42	nfan	$⊢ Ⅎ t (φ \land \forall t \in T x \leq F (t))$
44	1	nfrn	$⊢ \underline{Ⅎ} t ran F$
45	44	nfcri	$⊢ Ⅎ t y \in ran F$
46	43 45	nfan	$⊢ Ⅎ t ((φ \land \forall t \in T x \leq F (t)) \land y \in ran F)$
47		nfv	$⊢ Ⅎ t x \leq y$
48		rspa	$⊢ (\forall t \in T x \leq F (t) \land t \in T) \to x \leq F (t)$
49		breq2	$⊢ F (t) = y \to (x \leq F (t) \leftrightarrow x \leq y)$
50	48 49	syl5ibcom	$⊢ (\forall t \in T x \leq F (t) \land t \in T) \to (F (t) = y \to x \leq y)$
51	50	ex	$⊢ \forall t \in T x \leq F (t) \to (t \in T \to (F (t) = y \to x \leq y))$
52	51	ad2antlr	$⊢ ((φ \land \forall t \in T x \leq F (t)) \land y \in ran F) \to (t \in T \to (F (t) = y \to x \leq y))$
53	46 47 52	rexlimd	$⊢ ((φ \land \forall t \in T x \leq F (t)) \land y \in ran F) \to (\exists t \in T F (t) = y \to x \leq y)$
54	41 53	mpd	$⊢ ((φ \land \forall t \in T x \leq F (t)) \land y \in ran F) \to x \leq y$
55	54	ex	$⊢ (φ \land \forall t \in T x \leq F (t)) \to (y \in ran F \to x \leq y)$
56	35 55	ralrimi	$⊢ (φ \land \forall t \in T x \leq F (t)) \to \forall y \in ran F x \leq y$
57	56	ex	$⊢ φ \to (\forall t \in T x \leq F (t) \to \forall y \in ran F x \leq y)$
58	57	reximdv	$⊢ φ \to (\exists x \in ran F \forall t \in T x \leq F (t) \to \exists x \in ran F \forall y \in ran F x \leq y)$
59	34 58	mpd	$⊢ φ \to \exists x \in ran F \forall y \in ran F x \leq y$
60		lbinfcl	$⊢ (ran F \subseteq ℝ \land \exists x \in ran F \forall y \in ran F x \leq y) \to inf (ran F ℝ <) \in ran F$
61	12 59 60	syl2anc	$⊢ φ \to inf (ran F ℝ <) \in ran F$
62	12 61	sseldd	$⊢ φ \to inf (ran F ℝ <) \in ℝ$
63	12	adantr	$⊢ (φ \land t \in T) \to ran F \subseteq ℝ$
64	59	adantr	$⊢ (φ \land t \in T) \to \exists x \in ran F \forall y \in ran F x \leq y$
65		dffn3	$⊢ F Fn T \leftrightarrow F : T ⟶ ran F$
66	13 65	sylib	$⊢ φ \to F : T ⟶ ran F$
67	66	ffvelcdmda	$⊢ (φ \land t \in T) \to F (t) \in ran F$
68		lbinfle	$⊢ (ran F \subseteq ℝ \land \exists x \in ran F \forall y \in ran F x \leq y \land F (t) \in ran F) \to inf (ran F ℝ <) \leq F (t)$
69	63 64 67 68	syl3anc	$⊢ (φ \land t \in T) \to inf (ran F ℝ <) \leq F (t)$
70	69	ex	$⊢ φ \to (t \in T \to inf (ran F ℝ <) \leq F (t))$
71	2 70	ralrimi	$⊢ φ \to \forall t \in T inf (ran F ℝ <) \leq F (t)$
72	61 62 71	3jca	$⊢ φ \to (inf (ran F ℝ <) \in ran F \land inf (ran F ℝ <) \in ℝ \land \forall t \in T inf (ran F ℝ <) \leq F (t))$

Metamath Proof Explorer

Theorem stoweidlem29

Proof