fimax2g

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

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

Proof

Step	Hyp	Ref	Expression
1		sopo	$⊢ R Or A \to R Po A$
2		cnvpo	$⊢ R Po A \leftrightarrow R^{-1} Po A$
3	1 2	sylib	$⊢ R Or A \to R^{-1} Po A$
4		frfi	$⊢ (R^{-1} Po A \land A \in Fin) \to R^{-1} Fr A$
5	3 4	sylan	$⊢ (R Or A \land A \in Fin) \to R^{-1} Fr A$
6	5	3adant3	$⊢ (R Or A \land A \in Fin \land A \neq \emptyset) \to R^{-1} Fr A$
7		ssid	$⊢ A \subseteq A$
8		fri	$⊢ ((A \in Fin \land R^{-1} Fr A) \land (A \subseteq A \land A \neq \emptyset)) \to \exists x \in A \forall y \in A \neg y R^{-1} x$
9	7 8	mpanr1	$⊢ ((A \in Fin \land R^{-1} Fr A) \land A \neq \emptyset) \to \exists x \in A \forall y \in A \neg y R^{-1} x$
10	9	an32s	$⊢ ((A \in Fin \land A \neq \emptyset) \land R^{-1} Fr A) \to \exists x \in A \forall y \in A \neg y R^{-1} x$
11		vex	$⊢ y \in V$
12		vex	$⊢ x \in V$
13	11 12	brcnv	$⊢ y R^{-1} x \leftrightarrow x R y$
14	13	notbii	$⊢ \neg y R^{-1} x \leftrightarrow \neg x R y$
15	14	ralbii	$⊢ \forall y \in A \neg y R^{-1} x \leftrightarrow \forall y \in A \neg x R y$
16	15	rexbii	$⊢ \exists x \in A \forall y \in A \neg y R^{-1} x \leftrightarrow \exists x \in A \forall y \in A \neg x R y$
17	10 16	sylib	$⊢ ((A \in Fin \land A \neq \emptyset) \land R^{-1} Fr A) \to \exists x \in A \forall y \in A \neg x R y$
18	17	ex	$⊢ (A \in Fin \land A \neq \emptyset) \to (R^{-1} Fr A \to \exists x \in A \forall y \in A \neg x R y)$
19	18	3adant1	$⊢ (R Or A \land A \in Fin \land A \neq \emptyset) \to (R^{-1} Fr A \to \exists x \in A \forall y \in A \neg x R y)$
20	6 19	mpd	$⊢ (R Or A \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A \neg x R y$

Metamath Proof Explorer

Theorem fimax2g

Proof