fiming

Description: A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020)

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

Step	Hyp	Ref	Expression
1		fimin2g	$⊢ (R Or A \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A \neg y R x$
2		nesym	$⊢ x \neq y \leftrightarrow \neg y = x$
3	2	imbi1i	$⊢ (x \neq y \to x R y) \leftrightarrow (\neg y = x \to x R y)$
4		pm4.64	$⊢ (\neg y = x \to x R y) \leftrightarrow (y = x \lor x R y)$
5	3 4	bitri	$⊢ (x \neq y \to x R y) \leftrightarrow (y = x \lor x R y)$
6		sotric	$⊢ (R Or A \land (y \in A \land x \in A)) \to (y R x \leftrightarrow \neg (y = x \lor x R y))$
7	6	ancom2s	$⊢ (R Or A \land (x \in A \land y \in A)) \to (y R x \leftrightarrow \neg (y = x \lor x R y))$
8	7	con2bid	$⊢ (R Or A \land (x \in A \land y \in A)) \to ((y = x \lor x R y) \leftrightarrow \neg y R x)$
9	5 8	syl5bb	$⊢ (R Or A \land (x \in A \land y \in A)) \to ((x \neq y \to x R y) \leftrightarrow \neg y R x)$
10	9	anassrs	$⊢ ((R Or A \land x \in A) \land y \in A) \to ((x \neq y \to x R y) \leftrightarrow \neg y R x)$
11	10	ralbidva	$⊢ (R Or A \land x \in A) \to (\forall y \in A (x \neq y \to x R y) \leftrightarrow \forall y \in A \neg y R x)$
12	11	rexbidva	$⊢ R Or A \to (\exists x \in A \forall y \in A (x \neq y \to x R y) \leftrightarrow \exists x \in A \forall y \in A \neg y R x)$
13	12	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 x R y) \leftrightarrow \exists x \in A \forall y \in A \neg y R x)$
14	1 13	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 x R y)$

Metamath Proof Explorer