Metamath Proof Explorer


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 ( 𝐴 , ℝ* , < ) = -∞ ) )