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

Metamath Proof Explorer

Theorem fimaxre

Description: A finite set of real numbers has a maximum. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Steven Nguyen, 3-Jun-2023)

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

Proof

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