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	$⊢ (A \subseteq ℝ \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A y \leq x$

Proof

Step	Hyp	Ref	Expression
1		ltso	$⊢ < Or ℝ$
2		soss	$⊢ A \subseteq ℝ \to (< Or ℝ \to < Or A)$
3	1 2	mpi	$⊢ A \subseteq ℝ \to < Or A$
4		fimaxg	$⊢ (< Or A \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A (x \neq y \to y < x)$
5	3 4	syl3an1	$⊢ (A \subseteq ℝ \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A (x \neq y \to y < x)$
6		ssel2	$⊢ (A \subseteq ℝ \land y \in A) \to y \in ℝ$
7	6	adantrl	$⊢ (A \subseteq ℝ \land (x \in A \land y \in A)) \to y \in ℝ$
8		ssel2	$⊢ (A \subseteq ℝ \land x \in A) \to x \in ℝ$
9	8	adantrr	$⊢ (A \subseteq ℝ \land (x \in A \land y \in A)) \to x \in ℝ$
10	7 9	leloed	$⊢ (A \subseteq ℝ \land (x \in A \land y \in A)) \to (y \leq x \leftrightarrow (y < x \lor y = x))$
11		orcom	$⊢ (x = y \lor y < x) \leftrightarrow (y < x \lor x = y)$
12		equcom	$⊢ x = y \leftrightarrow y = x$
13	12	orbi2i	$⊢ (y < x \lor x = y) \leftrightarrow (y < x \lor y = x)$
14	11 13	bitri	$⊢ (x = y \lor y < x) \leftrightarrow (y < x \lor y = x)$
15	14	a1i	$⊢ (A \subseteq ℝ \land (x \in A \land y \in A)) \to ((x = y \lor y < x) \leftrightarrow (y < x \lor y = x))$
16		neor	$⊢ (x = y \lor y < x) \leftrightarrow (x \neq y \to y < x)$
17	16	a1i	$⊢ (A \subseteq ℝ \land (x \in A \land y \in A)) \to ((x = y \lor y < x) \leftrightarrow (x \neq y \to y < x))$
18	10 15 17	3bitr2d	$⊢ (A \subseteq ℝ \land (x \in A \land y \in A)) \to (y \leq x \leftrightarrow (x \neq y \to y < x))$
19	18	biimprd	$⊢ (A \subseteq ℝ \land (x \in A \land y \in A)) \to ((x \neq y \to y < x) \to y \leq x)$
20	19	anassrs	$⊢ ((A \subseteq ℝ \land x \in A) \land y \in A) \to ((x \neq y \to y < x) \to y \leq x)$
21	20	ralimdva	$⊢ (A \subseteq ℝ \land x \in A) \to (\forall y \in A (x \neq y \to y < x) \to \forall y \in A y \leq x)$
22	21	reximdva	$⊢ A \subseteq ℝ \to (\exists x \in A \forall y \in A (x \neq y \to y < x) \to \exists x \in A \forall y \in A y \leq x)$
23	22	3ad2ant1	$⊢ (A \subseteq ℝ \land A \in Fin \land A \neq \emptyset) \to (\exists x \in A \forall y \in A (x \neq y \to y < x) \to \exists x \in A \forall y \in A y \leq x)$
24	5 23	mpd	$⊢ (A \subseteq ℝ \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A y \leq x$

Metamath Proof Explorer

Theorem fimaxre

Proof