Theorem infxrunb3rnmpt

Description: The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	infxrunb3rnmpt.1	⊢ Ⅎ 𝑥 𝜑
	infxrunb3rnmpt.2	⊢ Ⅎ 𝑦 𝜑
	infxrunb3rnmpt.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
Assertion	infxrunb3rnmpt	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) = -∞ ) )

Proof

Step	Hyp	Ref	Expression
1		infxrunb3rnmpt.1	⊢ Ⅎ 𝑥 𝜑
2		infxrunb3rnmpt.2	⊢ Ⅎ 𝑦 𝜑
3		infxrunb3rnmpt.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
4		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5	4	nfrn	⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
6		nfv	⊢ Ⅎ 𝑥 𝑧 ≤ 𝑦
7	5 6	nfrex	⊢ Ⅎ 𝑥 ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦
8		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
9		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
10	9	elrnmpt1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ* ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
11	8 3 10	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
12	11	3adant3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≤ 𝑦 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
13		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≤ 𝑦 ) → 𝐵 ≤ 𝑦 )
14		breq1	⊢ ( 𝑧 = 𝐵 → ( 𝑧 ≤ 𝑦 ↔ 𝐵 ≤ 𝑦 ) )
15	14	rspcev	⊢ ( ( 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ 𝐵 ≤ 𝑦 ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
16	12 13 15	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≤ 𝑦 ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
17	16	3exp	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝐵 ≤ 𝑦 → ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) ) )
18	1 7 17	rexlimd	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )
19		nfv	⊢ Ⅎ 𝑧 ∃ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦
20		vex	⊢ 𝑧 ∈ V
21	9	elrnmpt	⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
22	20 21	ax-mp	⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
23	22	biimpi	⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
24	14	biimpcd	⊢ ( 𝑧 ≤ 𝑦 → ( 𝑧 = 𝐵 → 𝐵 ≤ 𝑦 ) )
25	24	a1d	⊢ ( 𝑧 ≤ 𝑦 → ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝐵 ≤ 𝑦 ) ) )
26	6 25	reximdai	⊢ ( 𝑧 ≤ 𝑦 → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → ∃ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) )
27	26	com12	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → ( 𝑧 ≤ 𝑦 → ∃ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) )
28	23 27	syl	⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ( 𝑧 ≤ 𝑦 → ∃ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) )
29	19 28	rexlimi	⊢ ( ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 → ∃ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
30	29	a1i	⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 → ∃ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) )
31	18 30	impbid	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )
32	2 31	ralbid	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )
33	1 9 3	rnmptssd	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ* )
34		infxrunb3	⊢ ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ* → ( ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ↔ inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) = -∞ ) )
35	33 34	syl	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ↔ inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) = -∞ ) )
36	32 35	bitrd	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) = -∞ ) )