Theorem infxrgelbrnmpt

Description: The infimum of an indexed set of extended reals is greater than or equal to a lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	infxrgelbrnmpt.x	⊢ Ⅎ 𝑥 𝜑
	infxrgelbrnmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
	infxrgelbrnmpt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
Assertion	infxrgelbrnmpt	⊢ ( 𝜑 → ( 𝐶 ≤ inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ↔ ∀ 𝑥 ∈ 𝐴 𝐶 ≤ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		infxrgelbrnmpt.x	⊢ Ⅎ 𝑥 𝜑
2		infxrgelbrnmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
3		infxrgelbrnmpt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
4		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5	1 4 2	rnmptssd	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ* )
6		infxrgelb	⊢ ( ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐶 ≤ inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 ≤ 𝑧 ) )
7	5 3 6	syl2anc	⊢ ( 𝜑 → ( 𝐶 ≤ inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 ≤ 𝑧 ) )
8		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
9	8	nfrn	⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
10		nfv	⊢ Ⅎ 𝑥 𝐶 ≤ 𝑧
11	9 10	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 ≤ 𝑧
12	1 11	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 ≤ 𝑧 )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
14	4	elrnmpt1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ* ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
15	13 2 14	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
16	15	adantlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 ≤ 𝑧 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
17		simplr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 ≤ 𝑧 ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 ≤ 𝑧 )
18		breq2	⊢ ( 𝑧 = 𝐵 → ( 𝐶 ≤ 𝑧 ↔ 𝐶 ≤ 𝐵 ) )
19	18	rspcva	⊢ ( ( 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 ≤ 𝑧 ) → 𝐶 ≤ 𝐵 )
20	16 17 19	syl2anc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 ≤ 𝑧 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≤ 𝐵 )
21	20	ex	⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 ≤ 𝑧 ) → ( 𝑥 ∈ 𝐴 → 𝐶 ≤ 𝐵 ) )
22	12 21	ralrimi	⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 ≤ 𝑧 ) → ∀ 𝑥 ∈ 𝐴 𝐶 ≤ 𝐵 )
23		vex	⊢ 𝑧 ∈ V
24	4	elrnmpt	⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
25	23 24	ax-mp	⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
26	25	biimpi	⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
27	26	adantl	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ≤ 𝐵 ∧ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
28		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐶 ≤ 𝐵
29		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≤ 𝐵 )
30	18	biimprcd	⊢ ( 𝐶 ≤ 𝐵 → ( 𝑧 = 𝐵 → 𝐶 ≤ 𝑧 ) )
31	29 30	syl	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑧 = 𝐵 → 𝐶 ≤ 𝑧 ) )
32	31	ex	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ≤ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝐶 ≤ 𝑧 ) ) )
33	28 10 32	rexlimd	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ≤ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝐶 ≤ 𝑧 ) )
34	33	adantr	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ≤ 𝐵 ∧ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝐶 ≤ 𝑧 ) )
35	27 34	mpd	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐶 ≤ 𝐵 ∧ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝐶 ≤ 𝑧 )
36	35	ralrimiva	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ≤ 𝐵 → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 ≤ 𝑧 )
37	36	adantl	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≤ 𝐵 ) → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 ≤ 𝑧 )
38	22 37	impbida	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝐶 ≤ 𝑧 ↔ ∀ 𝑥 ∈ 𝐴 𝐶 ≤ 𝐵 ) )
39	7 38	bitrd	⊢ ( 𝜑 → ( 𝐶 ≤ inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ↔ ∀ 𝑥 ∈ 𝐴 𝐶 ≤ 𝐵 ) )