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 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )