Metamath Proof Explorer

Theorem fimaxg

Description: A finite set has a maximum under a total order. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 29-Jan-2014)

		Ref	Expression
	Assertion	fimaxg	$⊢ (R Or A \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A (x \neq y \to y R x)$

Proof

Step	Hyp	Ref	Expression
1		fimax2g	$⊢ (R Or A \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A \neg x R y$
2		df-ne	$⊢ x \neq y \leftrightarrow \neg x = y$
3	2	imbi1i	$⊢ (x \neq y \to y R x) \leftrightarrow (\neg x = y \to y R x)$
4		pm4.64	$⊢ (\neg x = y \to y R x) \leftrightarrow (x = y \lor y R x)$
5	3 4	bitri	$⊢ (x \neq y \to y R x) \leftrightarrow (x = y \lor y R x)$
6		sotric	$⊢ (R Or A \land (x \in A \land y \in A)) \to (x R y \leftrightarrow \neg (x = y \lor y R x))$
7	6	con2bid	$⊢ (R Or A \land (x \in A \land y \in A)) \to ((x = y \lor y R x) \leftrightarrow \neg x R y)$
8	5 7	syl5bb	$⊢ (R Or A \land (x \in A \land y \in A)) \to ((x \neq y \to y R x) \leftrightarrow \neg x R y)$
9	8	anassrs	$⊢ ((R Or A \land x \in A) \land y \in A) \to ((x \neq y \to y R x) \leftrightarrow \neg x R y)$
10	9	ralbidva	$⊢ (R Or A \land x \in A) \to (\forall y \in A (x \neq y \to y R x) \leftrightarrow \forall y \in A \neg x R y)$
11	10	rexbidva	$⊢ R Or A \to (\exists x \in A \forall y \in A (x \neq y \to y R x) \leftrightarrow \exists x \in A \forall y \in A \neg x R y)$
12	11	3ad2ant1	$⊢ (R Or A \land A \in Fin \land A \neq \emptyset) \to (\exists x \in A \forall y \in A (x \neq y \to y R x) \leftrightarrow \exists x \in A \forall y \in A \neg x R y)$
13	1 12	mpbird	$⊢ (R Or A \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A (x \neq y \to y R x)$