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

Metamath Proof Explorer

Theorem fiminre

Description: A nonempty finite set of real numbers has a minimum. Analogous to fimaxre . (Contributed by AV, 9-Aug-2020) (Proof shortened by Steven Nguyen, 3-Jun-2023)

Ref Expression
Assertion fiminre ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )

Proof

Step Hyp Ref Expression
1 ltso ⊢ < Or ℝ
2 soss ⊢ ( 𝐴 ⊆ ℝ → ( < Or ℝ → < Or 𝐴 ) )
3 1 2 mpi ⊢ ( 𝐴 ⊆ ℝ → < Or 𝐴 )
4 fiming ⊢ ( ( < Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑥 < 𝑦 ) )
5 3 4 syl3an1 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑥 < 𝑦 ) )
6 ssel2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
7 6 adantr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
8 ssel2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
9 8 adantlr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
10 7 9 leloed ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ) ) )
11 orcom ⊢ ( ( 𝑥 = 𝑦 ∨ 𝑥 < 𝑦 ) ↔ ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ) )
12 11 a1i ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 = 𝑦 ∨ 𝑥 < 𝑦 ) ↔ ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ) ) )
13 neor ⊢ ( ( 𝑥 = 𝑦 ∨ 𝑥 < 𝑦 ) ↔ ( 𝑥 ≠ 𝑦 → 𝑥 < 𝑦 ) )
14 13 a1i ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 = 𝑦 ∨ 𝑥 < 𝑦 ) ↔ ( 𝑥 ≠ 𝑦 → 𝑥 < 𝑦 ) ) )
15 10 12 14 3bitr2d ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 ≠ 𝑦 → 𝑥 < 𝑦 ) ) )
16 15 biimprd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ≠ 𝑦 → 𝑥 < 𝑦 ) → 𝑥 ≤ 𝑦 ) )
17 16 ralimdva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑥 < 𝑦 ) → ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
18 17 reximdva ⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑥 < 𝑦 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
19 18 3ad2ant1 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑥 < 𝑦 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
20 5 19 mpd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )