fimin2g

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

		Ref	Expression
	Assertion	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$

Step	Hyp	Ref	Expression
1		3simpc	$⊢ (R Or A \land A \in Fin \land A \neq \emptyset) \to (A \in Fin \land A \neq \emptyset)$
2		sopo	$⊢ R Or A \to R Po A$
3	2	3ad2ant1	$⊢ (R Or A \land A \in Fin \land A \neq \emptyset) \to R Po A$
4		simp2	$⊢ (R Or A \land A \in Fin \land A \neq \emptyset) \to A \in Fin$
5		frfi	$⊢ (R Po A \land A \in Fin) \to R Fr A$
6	3 4 5	syl2anc	$⊢ (R Or A \land A \in Fin \land A \neq \emptyset) \to R Fr A$
7		ssid	$⊢ A \subseteq A$
8		fri	$⊢ ((A \in Fin \land R Fr A) \land (A \subseteq A \land A \neq \emptyset)) \to \exists x \in A \forall y \in A \neg y R x$
9	7 8	mpanr1	$⊢ ((A \in Fin \land R Fr A) \land A \neq \emptyset) \to \exists x \in A \forall y \in A \neg y R x$
10	9	an32s	$⊢ ((A \in Fin \land A \neq \emptyset) \land R Fr A) \to \exists x \in A \forall y \in A \neg y R x$
11	1 6 10	syl2anc	$⊢ (R Or A \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A \neg y R x$

Metamath Proof Explorer