Metamath Proof Explorer

Theorem dfinfre

Description: The infimum of a set of reals A . (Contributed by NM, 9-Oct-2005) (Revised by AV, 4-Sep-2020)

Ref Expression
Assertion dfinfre ⊢ A ⊆ ℝ → inf A ℝ < = ⋃ x ∈ ℝ | ∀ y ∈ A x ≤ y ∧ ∀ y ∈ ℝ x < y → ∃ z ∈ A z < y

Proof

Step Hyp Ref Expression
1 df-inf ⊢ inf A ℝ < = sup A ℝ < -1
2 df-sup ⊢ sup A ℝ < -1 = ⋃ x ∈ ℝ | ∀ y ∈ A ¬ x < -1 y ∧ ∀ y ∈ ℝ y < -1 x → ∃ z ∈ A y < -1 z
3 ssel2 ⊢ A ⊆ ℝ ∧ y ∈ A → y ∈ ℝ
4 vex ⊢ x ∈ V
5 vex ⊢ y ∈ V
6 4 5 brcnv ⊢ x < -1 y ↔ y < x
7 6 notbii ⊢ ¬ x < -1 y ↔ ¬ y < x
8 lenlt ⊢ x ∈ ℝ ∧ y ∈ ℝ → x ≤ y ↔ ¬ y < x
9 7 8 bitr4id ⊢ x ∈ ℝ ∧ y ∈ ℝ → ¬ x < -1 y ↔ x ≤ y
10 3 9 sylan2 ⊢ x ∈ ℝ ∧ A ⊆ ℝ ∧ y ∈ A → ¬ x < -1 y ↔ x ≤ y
11 10 ancoms ⊢ A ⊆ ℝ ∧ y ∈ A ∧ x ∈ ℝ → ¬ x < -1 y ↔ x ≤ y
12 11 an32s ⊢ A ⊆ ℝ ∧ x ∈ ℝ ∧ y ∈ A → ¬ x < -1 y ↔ x ≤ y
13 12 ralbidva ⊢ A ⊆ ℝ ∧ x ∈ ℝ → ∀ y ∈ A ¬ x < -1 y ↔ ∀ y ∈ A x ≤ y
14 5 4 brcnv ⊢ y < -1 x ↔ x < y
15 vex ⊢ z ∈ V
16 5 15 brcnv ⊢ y < -1 z ↔ z < y
17 16 rexbii ⊢ ∃ z ∈ A y < -1 z ↔ ∃ z ∈ A z < y
18 14 17 imbi12i ⊢ y < -1 x → ∃ z ∈ A y < -1 z ↔ x < y → ∃ z ∈ A z < y
19 18 ralbii ⊢ ∀ y ∈ ℝ y < -1 x → ∃ z ∈ A y < -1 z ↔ ∀ y ∈ ℝ x < y → ∃ z ∈ A z < y
20 19 a1i ⊢ A ⊆ ℝ ∧ x ∈ ℝ → ∀ y ∈ ℝ y < -1 x → ∃ z ∈ A y < -1 z ↔ ∀ y ∈ ℝ x < y → ∃ z ∈ A z < y
21 13 20 anbi12d ⊢ A ⊆ ℝ ∧ x ∈ ℝ → ∀ y ∈ A ¬ x < -1 y ∧ ∀ y ∈ ℝ y < -1 x → ∃ z ∈ A y < -1 z ↔ ∀ y ∈ A x ≤ y ∧ ∀ y ∈ ℝ x < y → ∃ z ∈ A z < y
22 21 rabbidva ⊢ A ⊆ ℝ → x ∈ ℝ | ∀ y ∈ A ¬ x < -1 y ∧ ∀ y ∈ ℝ y < -1 x → ∃ z ∈ A y < -1 z = x ∈ ℝ | ∀ y ∈ A x ≤ y ∧ ∀ y ∈ ℝ x < y → ∃ z ∈ A z < y
23 22 unieqd ⊢ A ⊆ ℝ → ⋃ x ∈ ℝ | ∀ y ∈ A ¬ x < -1 y ∧ ∀ y ∈ ℝ y < -1 x → ∃ z ∈ A y < -1 z = ⋃ x ∈ ℝ | ∀ y ∈ A x ≤ y ∧ ∀ y ∈ ℝ x < y → ∃ z ∈ A z < y
24 2 23 eqtrid ⊢ A ⊆ ℝ → sup A ℝ < -1 = ⋃ x ∈ ℝ | ∀ y ∈ A x ≤ y ∧ ∀ y ∈ ℝ x < y → ∃ z ∈ A z < y
25 1 24 eqtrid ⊢ A ⊆ ℝ → inf A ℝ < = ⋃ x ∈ ℝ | ∀ y ∈ A x ≤ y ∧ ∀ y ∈ ℝ x < y → ∃ z ∈ A z < y