Theorem infxrbnd2

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

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

Proof

Step	Hyp	Ref	Expression
1		ralnex	⊢ ( ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
2		ssel2	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ* )
3		rexr	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
4		simpl	⊢ ( ( 𝑦 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → 𝑦 ∈ ℝ* )
5		simpr	⊢ ( ( 𝑦 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → 𝑥 ∈ ℝ* )
6	4 5	xrltnled	⊢ ( ( 𝑦 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 𝑦 < 𝑥 ↔ ¬ 𝑥 ≤ 𝑦 ) )
7	2 3 6	syl2an	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑦 < 𝑥 ↔ ¬ 𝑥 ≤ 𝑦 ) )
8	7	an32s	⊢ ( ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 < 𝑥 ↔ ¬ 𝑥 ≤ 𝑦 ) )
9	8	rexbidva	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 ≤ 𝑦 ) )
10		rexnal	⊢ ( ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 ≤ 𝑦 ↔ ¬ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
11	9 10	bitr2di	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝑥 ∈ ℝ ) → ( ¬ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
12	11	ralbidva	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
13	1 12	bitr3id	⊢ ( 𝐴 ⊆ ℝ* → ( ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) )
14		infxrunb2	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ inf ( 𝐴 , ℝ* , < ) = -∞ ) )
15		infxrcl	⊢ ( 𝐴 ⊆ ℝ* → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
16		ngtmnft	⊢ ( inf ( 𝐴 , ℝ* , < ) ∈ ℝ* → ( inf ( 𝐴 , ℝ* , < ) = -∞ ↔ ¬ -∞ < inf ( 𝐴 , ℝ* , < ) ) )
17	15 16	syl	⊢ ( 𝐴 ⊆ ℝ* → ( inf ( 𝐴 , ℝ* , < ) = -∞ ↔ ¬ -∞ < inf ( 𝐴 , ℝ* , < ) ) )
18	13 14 17	3bitrd	⊢ ( 𝐴 ⊆ ℝ* → ( ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ¬ -∞ < inf ( 𝐴 , ℝ* , < ) ) )
19	18	con4bid	⊢ ( 𝐴 ⊆ ℝ* → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ -∞ < inf ( 𝐴 , ℝ* , < ) ) )