somo

Description: A totally ordered set has at most one minimal element. (Contributed by Mario Carneiro, 24-Jun-2015) (Revised by NM, 16-Jun-2017)

		Ref	Expression
	Assertion	somo	$⊢ R Or A \to \exists^{*} x \in A \forall y \in A \neg y R x$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ y = x \to (y R z \leftrightarrow x R z)$
2	1	notbid	$⊢ y = x \to (\neg y R z \leftrightarrow \neg x R z)$
3	2	rspcv	$⊢ x \in A \to (\forall y \in A \neg y R z \to \neg x R z)$
4		breq1	$⊢ y = z \to (y R x \leftrightarrow z R x)$
5	4	notbid	$⊢ y = z \to (\neg y R x \leftrightarrow \neg z R x)$
6	5	rspcv	$⊢ z \in A \to (\forall y \in A \neg y R x \to \neg z R x)$
7	3 6	im2anan9	$⊢ (x \in A \land z \in A) \to ((\forall y \in A \neg y R z \land \forall y \in A \neg y R x) \to (\neg x R z \land \neg z R x))$
8	7	ancomsd	$⊢ (x \in A \land z \in A) \to ((\forall y \in A \neg y R x \land \forall y \in A \neg y R z) \to (\neg x R z \land \neg z R x))$
9	8	imp	$⊢ ((x \in A \land z \in A) \land (\forall y \in A \neg y R x \land \forall y \in A \neg y R z)) \to (\neg x R z \land \neg z R x)$
10		ioran	$⊢ \neg (x R z \lor z R x) \leftrightarrow (\neg x R z \land \neg z R x)$
11		solin	$⊢ (R Or A \land (x \in A \land z \in A)) \to (x R z \lor x = z \lor z R x)$
12		df-3or	$⊢ (x R z \lor x = z \lor z R x) \leftrightarrow ((x R z \lor x = z) \lor z R x)$
13	11 12	sylib	$⊢ (R Or A \land (x \in A \land z \in A)) \to ((x R z \lor x = z) \lor z R x)$
14		or32	$⊢ ((x R z \lor x = z) \lor z R x) \leftrightarrow ((x R z \lor z R x) \lor x = z)$
15	13 14	sylib	$⊢ (R Or A \land (x \in A \land z \in A)) \to ((x R z \lor z R x) \lor x = z)$
16	15	ord	$⊢ (R Or A \land (x \in A \land z \in A)) \to (\neg (x R z \lor z R x) \to x = z)$
17	10 16	syl5bir	$⊢ (R Or A \land (x \in A \land z \in A)) \to ((\neg x R z \land \neg z R x) \to x = z)$
18	9 17	syl5	$⊢ (R Or A \land (x \in A \land z \in A)) \to (((x \in A \land z \in A) \land (\forall y \in A \neg y R x \land \forall y \in A \neg y R z)) \to x = z)$
19	18	exp4b	$⊢ R Or A \to ((x \in A \land z \in A) \to ((x \in A \land z \in A) \to ((\forall y \in A \neg y R x \land \forall y \in A \neg y R z) \to x = z)))$
20	19	pm2.43d	$⊢ R Or A \to ((x \in A \land z \in A) \to ((\forall y \in A \neg y R x \land \forall y \in A \neg y R z) \to x = z))$
21	20	ralrimivv	$⊢ R Or A \to \forall x \in A \forall z \in A ((\forall y \in A \neg y R x \land \forall y \in A \neg y R z) \to x = z)$
22		breq2	$⊢ x = z \to (y R x \leftrightarrow y R z)$
23	22	notbid	$⊢ x = z \to (\neg y R x \leftrightarrow \neg y R z)$
24	23	ralbidv	$⊢ x = z \to (\forall y \in A \neg y R x \leftrightarrow \forall y \in A \neg y R z)$
25	24	rmo4	$⊢ \exists^{*} x \in A \forall y \in A \neg y R x \leftrightarrow \forall x \in A \forall z \in A ((\forall y \in A \neg y R x \land \forall y \in A \neg y R z) \to x = z)$
26	21 25	sylibr	$⊢ R Or A \to \exists^{*} x \in A \forall y \in A \neg y R x$

Metamath Proof Explorer

Theorem somo

Proof