This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ⊆ ℝ → inf ( 𝐴 , ℝ , < ) = ∪ { 𝑥 ∈ ℝ ∣ ( ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) } )

Proof

Step Hyp Ref Expression
1 df-inf ⊢ inf ( 𝐴 , ℝ , < ) = sup ( 𝐴 , ℝ , ◡ < )
2 df-sup ⊢ sup ( 𝐴 , ℝ , ◡ < ) = ∪ { 𝑥 ∈ ℝ ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ) }
3 ssel2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
4 vex ⊢ 𝑥 ∈ V
5 vex ⊢ 𝑦 ∈ V
6 4 5 brcnv ⊢ ( 𝑥 ◡ < 𝑦 ↔ 𝑦 < 𝑥 )
7 6 notbii ⊢ ( ¬ 𝑥 ◡ < 𝑦 ↔ ¬ 𝑦 < 𝑥 )
8 lenlt ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑥 ) )
9 7 8 bitr4id ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ¬ 𝑥 ◡ < 𝑦 ↔ 𝑥 ≤ 𝑦 ) )
10 3 9 sylan2 ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) ) → ( ¬ 𝑥 ◡ < 𝑦 ↔ 𝑥 ≤ 𝑦 ) )
11 10 ancoms ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ¬ 𝑥 ◡ < 𝑦 ↔ 𝑥 ≤ 𝑦 ) )
12 11 an32s ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝑥 ◡ < 𝑦 ↔ 𝑥 ≤ 𝑦 ) )
13 12 ralbidva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
14 5 4 brcnv ⊢ ( 𝑦 ◡ < 𝑥 ↔ 𝑥 < 𝑦 )
15 vex ⊢ 𝑧 ∈ V
16 5 15 brcnv ⊢ ( 𝑦 ◡ < 𝑧 ↔ 𝑧 < 𝑦 )
17 16 rexbii ⊢ ( ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 )
18 14 17 imbi12i ⊢ ( ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ↔ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) )
19 18 ralbii ⊢ ( ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ↔ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) )
20 19 a1i ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ↔ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
21 13 20 anbi12d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) )
22 21 rabbidva ⊢ ( 𝐴 ⊆ ℝ → { 𝑥 ∈ ℝ ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ) } = { 𝑥 ∈ ℝ ∣ ( ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) } )
23 22 unieqd ⊢ ( 𝐴 ⊆ ℝ → ∪ { 𝑥 ∈ ℝ ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ) } = ∪ { 𝑥 ∈ ℝ ∣ ( ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) } )
24 2 23 eqtrid ⊢ ( 𝐴 ⊆ ℝ → sup ( 𝐴 , ℝ , ◡ < ) = ∪ { 𝑥 ∈ ℝ ∣ ( ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) } )
25 1 24 eqtrid ⊢ ( 𝐴 ⊆ ℝ → inf ( 𝐴 , ℝ , < ) = ∪ { 𝑥 ∈ ℝ ∣ ( ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) } )