Theorem infxrunb2

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

	Ref	Expression
Assertion	infxrunb2	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ inf ( 𝐴 , ℝ* , < ) = -∞ ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑥 𝐴 ⊆ ℝ*
2		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥
3	1 2	nfan	⊢ Ⅎ 𝑥 ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 )
4		nfv	⊢ Ⅎ 𝑦 𝐴 ⊆ ℝ*
5		nfcv	⊢ Ⅎ 𝑦 ℝ
6		nfre1	⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥
7	5 6	nfralw	⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥
8	4 7	nfan	⊢ Ⅎ 𝑦 ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 )
9		simpl	⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) → 𝐴 ⊆ ℝ* )
10		mnfxr	⊢ -∞ ∈ ℝ*
11	10	a1i	⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) → -∞ ∈ ℝ* )
12		ssel2	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ* )
13		nltmnf	⊢ ( 𝑥 ∈ ℝ* → ¬ 𝑥 < -∞ )
14	12 13	syl	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 < -∞ )
15	14	ralrimiva	⊢ ( 𝐴 ⊆ ℝ* → ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 < -∞ )
16	15	adantr	⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) → ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 < -∞ )
17		ralimralim	⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 → ∀ 𝑥 ∈ ℝ ( -∞ < 𝑥 → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
18	17	adantl	⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) → ∀ 𝑥 ∈ ℝ ( -∞ < 𝑥 → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
19	3 8 9 11 16 18	infxr	⊢ ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) → inf ( 𝐴 , ℝ* , < ) = -∞ )
20	19	ex	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 → inf ( 𝐴 , ℝ* , < ) = -∞ ) )
21		rexr	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
22	21	adantl	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) = -∞ ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ* )
23		simpl	⊢ ( ( inf ( 𝐴 , ℝ* , < ) = -∞ ∧ 𝑥 ∈ ℝ ) → inf ( 𝐴 , ℝ* , < ) = -∞ )
24		mnflt	⊢ ( 𝑥 ∈ ℝ → -∞ < 𝑥 )
25	24	adantl	⊢ ( ( inf ( 𝐴 , ℝ* , < ) = -∞ ∧ 𝑥 ∈ ℝ ) → -∞ < 𝑥 )
26	23 25	eqbrtrd	⊢ ( ( inf ( 𝐴 , ℝ* , < ) = -∞ ∧ 𝑥 ∈ ℝ ) → inf ( 𝐴 , ℝ* , < ) < 𝑥 )
27	26	adantll	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) = -∞ ) ∧ 𝑥 ∈ ℝ ) → inf ( 𝐴 , ℝ* , < ) < 𝑥 )
28		xrltso	⊢ < Or ℝ*
29	28	a1i	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) = -∞ ) ∧ 𝑥 ∈ ℝ ) → < Or ℝ* )
30		xrinfmss	⊢ ( 𝐴 ⊆ ℝ* → ∃ 𝑧 ∈ ℝ* ( ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ* ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) ) )
31	30	ad2antrr	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) = -∞ ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑧 ∈ ℝ* ( ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ* ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ) ) )
32	29 31	infglb	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) = -∞ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 ∈ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) < 𝑥 ) → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
33	22 27 32	mp2and	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) = -∞ ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 )
34	33	ralrimiva	⊢ ( ( 𝐴 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) = -∞ ) → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 )
35	34	ex	⊢ ( 𝐴 ⊆ ℝ* → ( inf ( 𝐴 , ℝ* , < ) = -∞ → ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
36	20 35	impbid	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ inf ( 𝐴 , ℝ* , < ) = -∞ ) )