Theorem 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	⊢ Ⅎ 𝑡 𝐹
	stoweidlem29.2	⊢ Ⅎ 𝑡 𝜑
	stoweidlem29.3	⊢ 𝑇 = ∪ 𝐽
	stoweidlem29.4	⊢ 𝐾 = ( topGen ‘ ran (,) )
	stoweidlem29.5	⊢ ( 𝜑 → 𝐽 ∈ Comp )
	stoweidlem29.6	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
	stoweidlem29.7	⊢ ( 𝜑 → 𝑇 ≠ ∅ )
Assertion	stoweidlem29	⊢ ( 𝜑 → ( inf ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ∧ inf ( ran 𝐹 , ℝ , < ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹 ‘ 𝑡 ) ) )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem29.1	⊢ Ⅎ 𝑡 𝐹
2		stoweidlem29.2	⊢ Ⅎ 𝑡 𝜑
3		stoweidlem29.3	⊢ 𝑇 = ∪ 𝐽
4		stoweidlem29.4	⊢ 𝐾 = ( topGen ‘ ran (,) )
5		stoweidlem29.5	⊢ ( 𝜑 → 𝐽 ∈ Comp )
6		stoweidlem29.6	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
7		stoweidlem29.7	⊢ ( 𝜑 → 𝑇 ≠ ∅ )
8		eqid	⊢ ( 𝐽 Cn 𝐾 ) = ( 𝐽 Cn 𝐾 )
9	4 3 8 6	fcnre	⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )
10		df-f	⊢ ( 𝐹 : 𝑇 ⟶ ℝ ↔ ( 𝐹 Fn 𝑇 ∧ ran 𝐹 ⊆ ℝ ) )
11	9 10	sylib	⊢ ( 𝜑 → ( 𝐹 Fn 𝑇 ∧ ran 𝐹 ⊆ ℝ ) )
12	11	simprd	⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
13	11	simpld	⊢ ( 𝜑 → 𝐹 Fn 𝑇 )
14		fnfun	⊢ ( 𝐹 Fn 𝑇 → Fun 𝐹 )
15	13 14	syl	⊢ ( 𝜑 → Fun 𝐹 )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → Fun 𝐹 )
17	9	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝑇 )
18	17	eqcomd	⊢ ( 𝜑 → 𝑇 = dom 𝐹 )
19	18	eleq2d	⊢ ( 𝜑 → ( 𝑠 ∈ 𝑇 ↔ 𝑠 ∈ dom 𝐹 ) )
20	19	biimpa	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → 𝑠 ∈ dom 𝐹 )
21		fvelrn	⊢ ( ( Fun 𝐹 ∧ 𝑠 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑠 ) ∈ ran 𝐹 )
22	16 20 21	syl2anc	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑠 ) ∈ ran 𝐹 )
23		nfcv	⊢ Ⅎ 𝑡 𝑠
24	1 23	nffv	⊢ Ⅎ 𝑡 ( 𝐹 ‘ 𝑠 )
25	24	nfeq2	⊢ Ⅎ 𝑡 𝑥 = ( 𝐹 ‘ 𝑠 )
26		breq1	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑠 ) → ( 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ↔ ( 𝐹 ‘ 𝑠 ) ≤ ( 𝐹 ‘ 𝑡 ) ) )
27	25 26	ralbid	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑠 ) → ( ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑠 ) ≤ ( 𝐹 ‘ 𝑡 ) ) )
28	27	rspcev	⊢ ( ( ( 𝐹 ‘ 𝑠 ) ∈ ran 𝐹 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑠 ) ≤ ( 𝐹 ‘ 𝑡 ) ) → ∃ 𝑥 ∈ ran 𝐹 ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) )
29	22 28	sylan	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑠 ) ≤ ( 𝐹 ‘ 𝑡 ) ) → ∃ 𝑥 ∈ ran 𝐹 ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) )
30		nfcv	⊢ Ⅎ 𝑠 𝐹
31		nfcv	⊢ Ⅎ 𝑠 𝑇
32		nfcv	⊢ Ⅎ 𝑡 𝑇
33	30 1 31 32 3 4 5 6 7	evth2f	⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝑇 ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑠 ) ≤ ( 𝐹 ‘ 𝑡 ) )
34	29 33	r19.29a	⊢ ( 𝜑 → ∃ 𝑥 ∈ ran 𝐹 ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) )
35		nfv	⊢ Ⅎ 𝑦 ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) )
36		simpr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ran 𝐹 )
37	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝐹 Fn 𝑇 )
38		nfcv	⊢ Ⅎ 𝑡 𝑦
39	32 38 1	fvelrnbf	⊢ ( 𝐹 Fn 𝑇 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) = 𝑦 ) )
40	37 39	syl	⊢ ( ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) = 𝑦 ) )
41	36 40	mpbid	⊢ ( ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ∃ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) = 𝑦 )
42		nfra1	⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 )
43	2 42	nfan	⊢ Ⅎ 𝑡 ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) )
44	1	nfrn	⊢ Ⅎ 𝑡 ran 𝐹
45	44	nfcri	⊢ Ⅎ 𝑡 𝑦 ∈ ran 𝐹
46	43 45	nfan	⊢ Ⅎ 𝑡 ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑦 ∈ ran 𝐹 )
47		nfv	⊢ Ⅎ 𝑡 𝑥 ≤ 𝑦
48		rspa	⊢ ( ( ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) )
49		breq2	⊢ ( ( 𝐹 ‘ 𝑡 ) = 𝑦 → ( 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ↔ 𝑥 ≤ 𝑦 ) )
50	48 49	syl5ibcom	⊢ ( ( ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) = 𝑦 → 𝑥 ≤ 𝑦 ) )
51	50	ex	⊢ ( ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) → ( 𝑡 ∈ 𝑇 → ( ( 𝐹 ‘ 𝑡 ) = 𝑦 → 𝑥 ≤ 𝑦 ) ) )
52	51	ad2antlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑡 ∈ 𝑇 → ( ( 𝐹 ‘ 𝑡 ) = 𝑦 → 𝑥 ≤ 𝑦 ) ) )
53	46 47 52	rexlimd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ∃ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) = 𝑦 → 𝑥 ≤ 𝑦 ) )
54	41 53	mpd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑥 ≤ 𝑦 )
55	54	ex	⊢ ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ) → ( 𝑦 ∈ ran 𝐹 → 𝑥 ≤ 𝑦 ) )
56	35 55	ralrimi	⊢ ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) ) → ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 )
57	56	ex	⊢ ( 𝜑 → ( ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) → ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ) )
58	57	reximdv	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ran 𝐹 ∀ 𝑡 ∈ 𝑇 𝑥 ≤ ( 𝐹 ‘ 𝑡 ) → ∃ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ) )
59	34 58	mpd	⊢ ( 𝜑 → ∃ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 )
60		lbinfcl	⊢ ( ( ran 𝐹 ⊆ ℝ ∧ ∃ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ) → inf ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
61	12 59 60	syl2anc	⊢ ( 𝜑 → inf ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
62	12 61	sseldd	⊢ ( 𝜑 → inf ( ran 𝐹 , ℝ , < ) ∈ ℝ )
63	12	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ran 𝐹 ⊆ ℝ )
64	59	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ∃ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 )
65		dffn3	⊢ ( 𝐹 Fn 𝑇 ↔ 𝐹 : 𝑇 ⟶ ran 𝐹 )
66	13 65	sylib	⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ran 𝐹 )
67	66	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ran 𝐹 )
68		lbinfle	⊢ ( ( ran 𝐹 ⊆ ℝ ∧ ∃ 𝑥 ∈ ran 𝐹 ∀ 𝑦 ∈ ran 𝐹 𝑥 ≤ 𝑦 ∧ ( 𝐹 ‘ 𝑡 ) ∈ ran 𝐹 ) → inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹 ‘ 𝑡 ) )
69	63 64 67 68	syl3anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹 ‘ 𝑡 ) )
70	69	ex	⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 → inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹 ‘ 𝑡 ) ) )
71	2 70	ralrimi	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹 ‘ 𝑡 ) )
72	61 62 71	3jca	⊢ ( 𝜑 → ( inf ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ∧ inf ( ran 𝐹 , ℝ , < ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹 ‘ 𝑡 ) ) )