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	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )

Proof

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