Metamath Proof Explorer

Theorem fimaxre2

Description: A nonempty finite set of real numbers has an upper bound. (Contributed by Jeff Madsen, 27-May-2011) (Revised by Mario Carneiro, 13-Feb-2014)

Ref Expression
Assertion fimaxre2 ⊢A⊆ℝ∧A∈Fin→∃x∈ℝ∀y∈Ay≤x

Proof

Step Hyp Ref Expression
1 0re ⊢0∈ℝ
2 rzal ⊢A=∅→∀y∈Ay≤0
3 brralrspcev ⊢0∈ℝ∧∀y∈Ay≤0→∃x∈ℝ∀y∈Ay≤x
4 1 2 3 sylancr ⊢A=∅→∃x∈ℝ∀y∈Ay≤x
5 4 a1i ⊢A⊆ℝ∧A∈Fin→A=∅→∃x∈ℝ∀y∈Ay≤x
6 fimaxre ⊢A⊆ℝ∧A∈Fin∧A≠∅→∃x∈A∀y∈Ay≤x
7 6 3expia ⊢A⊆ℝ∧A∈Fin→A≠∅→∃x∈A∀y∈Ay≤x
8 ssrexv ⊢A⊆ℝ→∃x∈A∀y∈Ay≤x→∃x∈ℝ∀y∈Ay≤x
9 8 adantr ⊢A⊆ℝ∧A∈Fin→∃x∈A∀y∈Ay≤x→∃x∈ℝ∀y∈Ay≤x
10 7 9 syld ⊢A⊆ℝ∧A∈Fin→A≠∅→∃x∈ℝ∀y∈Ay≤x
11 5 10 pm2.61dne ⊢A⊆ℝ∧A∈Fin→∃x∈ℝ∀y∈Ay≤x