Theorem infrpgernmpt

Description: The infimum of a nonempty, bounded below, indexed subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	infrpgernmpt.x	⊢ Ⅎ 𝑥 𝜑
	infrpgernmpt.a	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	infrpgernmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
	infrpgernmpt.y	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 )
	infrpgernmpt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
Assertion	infrpgernmpt	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		infrpgernmpt.x	⊢ Ⅎ 𝑥 𝜑
2		infrpgernmpt.a	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3		infrpgernmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
4		infrpgernmpt.y	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 )
5		infrpgernmpt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
6		nfv	⊢ Ⅎ 𝑤 𝜑
7		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
8	1 7 3	rnmptssd	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ* )
9	1 3 7 2	rnmptn0	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≠ ∅ )
10		breq1	⊢ ( 𝑦 = 𝑤 → ( 𝑦 ≤ 𝐵 ↔ 𝑤 ≤ 𝐵 ) )
11	10	ralbidv	⊢ ( 𝑦 = 𝑤 → ( ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 ) )
12	11	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 )
13	4 12	sylib	⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 )
14	13	rnmptlb	⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑧 )
15	6 8 9 14 5	infrpge	⊢ ( 𝜑 → ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )
16		simpll	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → 𝜑 )
17		simpr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )
18		vex	⊢ 𝑤 ∈ V
19	7	elrnmpt	⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 ) )
20	18 19	ax-mp	⊢ ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 )
21	20	biimpi	⊢ ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 )
22	21	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 )
23		nfcv	⊢ Ⅎ 𝑥 𝑤
24		nfcv	⊢ Ⅎ 𝑥 ≤
25		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
26	25	nfrn	⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
27		nfcv	⊢ Ⅎ 𝑥 ℝ*
28		nfcv	⊢ Ⅎ 𝑥 <
29	26 27 28	nfinf	⊢ Ⅎ 𝑥 inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < )
30		nfcv	⊢ Ⅎ 𝑥 +𝑒
31		nfcv	⊢ Ⅎ 𝑥 𝐶
32	29 30 31	nfov	⊢ Ⅎ 𝑥 ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 )
33	23 24 32	nfbr	⊢ Ⅎ 𝑥 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 )
34	1 33	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )
35		id	⊢ ( 𝑤 = 𝐵 → 𝑤 = 𝐵 )
36	35	eqcomd	⊢ ( 𝑤 = 𝐵 → 𝐵 = 𝑤 )
37	36	adantl	⊢ ( ( 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ∧ 𝑤 = 𝐵 ) → 𝐵 = 𝑤 )
38		simpl	⊢ ( ( 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ∧ 𝑤 = 𝐵 ) → 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )
39	37 38	eqbrtrd	⊢ ( ( 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ∧ 𝑤 = 𝐵 ) → 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )
40	39	ex	⊢ ( 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) → ( 𝑤 = 𝐵 → 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) )
41	40	a1d	⊢ ( 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) → ( 𝑥 ∈ 𝐴 → ( 𝑤 = 𝐵 → 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) ) )
42	41	adantl	⊢ ( ( 𝜑 ∧ 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → ( 𝑥 ∈ 𝐴 → ( 𝑤 = 𝐵 → 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) ) )
43	34 42	reximdai	⊢ ( ( 𝜑 ∧ 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → ( ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 → ∃ 𝑥 ∈ 𝐴 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) )
44	43	imp	⊢ ( ( ( 𝜑 ∧ 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) ∧ ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )
45	16 17 22 44	syl21anc	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → ∃ 𝑥 ∈ 𝐴 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )
46	45	rexlimdva2	⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) )
47	15 46	mpd	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) )