Metamath Proof Explorer

Theorem infregelb

Description: Any lower bound of a nonempty set of real numbers is less than or equal to its infimum. (Contributed by Jeff Hankins, 1-Sep-2013) (Revised by AV, 4-Sep-2020) (Proof modification is discouraged.)

Ref Expression
Assertion infregelb ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐵 ≤ inf ( 𝐴 , ℝ , < ) ↔ ∀ 𝑧 ∈ 𝐴 𝐵 ≤ 𝑧 ) )

Proof

Step Hyp Ref Expression
1 ltso ⊢ < Or ℝ
2 1 a1i ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → < Or ℝ )
3 infm3 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑤 ∈ 𝐴 𝑤 < 𝑦 ) ) )
4 simp1 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → 𝐴 ⊆ ℝ )
5 2 3 4 infglbb ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝐵 ∈ ℝ ) → ( inf ( 𝐴 , ℝ , < ) < 𝐵 ↔ ∃ 𝑤 ∈ 𝐴 𝑤 < 𝐵 ) )
6 5 notbid ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝐵 ∈ ℝ ) → ( ¬ inf ( 𝐴 , ℝ , < ) < 𝐵 ↔ ¬ ∃ 𝑤 ∈ 𝐴 𝑤 < 𝐵 ) )
7 infrecl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ , < ) ∈ ℝ )
8 7 anim1i ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝐵 ∈ ℝ ) → ( inf ( 𝐴 , ℝ , < ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
9 8 ancomd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐵 ∈ ℝ ∧ inf ( 𝐴 , ℝ , < ) ∈ ℝ ) )
10 lenlt ⊢ ( ( 𝐵 ∈ ℝ ∧ inf ( 𝐴 , ℝ , < ) ∈ ℝ ) → ( 𝐵 ≤ inf ( 𝐴 , ℝ , < ) ↔ ¬ inf ( 𝐴 , ℝ , < ) < 𝐵 ) )
11 9 10 syl ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐵 ≤ inf ( 𝐴 , ℝ , < ) ↔ ¬ inf ( 𝐴 , ℝ , < ) < 𝐵 ) )
12 simplr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑤 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
13 ssel ⊢ ( 𝐴 ⊆ ℝ → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ ℝ ) )
14 13 adantr ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ ℝ ) )
15 14 imp ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ ℝ )
16 12 15 lenltd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝐵 ≤ 𝑤 ↔ ¬ 𝑤 < 𝐵 ) )
17 16 ralbidva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∀ 𝑤 ∈ 𝐴 𝐵 ≤ 𝑤 ↔ ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 < 𝐵 ) )
18 17 3ad2antl1 ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝐵 ∈ ℝ ) → ( ∀ 𝑤 ∈ 𝐴 𝐵 ≤ 𝑤 ↔ ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 < 𝐵 ) )
19 ralnex ⊢ ( ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 < 𝐵 ↔ ¬ ∃ 𝑤 ∈ 𝐴 𝑤 < 𝐵 )
20 18 19 bitrdi ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝐵 ∈ ℝ ) → ( ∀ 𝑤 ∈ 𝐴 𝐵 ≤ 𝑤 ↔ ¬ ∃ 𝑤 ∈ 𝐴 𝑤 < 𝐵 ) )
21 6 11 20 3bitr4d ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐵 ≤ inf ( 𝐴 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝐴 𝐵 ≤ 𝑤 ) )
22 breq2 ⊢ ( 𝑤 = 𝑧 → ( 𝐵 ≤ 𝑤 ↔ 𝐵 ≤ 𝑧 ) )
23 22 cbvralvw ⊢ ( ∀ 𝑤 ∈ 𝐴 𝐵 ≤ 𝑤 ↔ ∀ 𝑧 ∈ 𝐴 𝐵 ≤ 𝑧 )
24 21 23 bitrdi ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐵 ≤ inf ( 𝐴 , ℝ , < ) ↔ ∀ 𝑧 ∈ 𝐴 𝐵 ≤ 𝑧 ) )