fisupg

Description: Lemma showing existence and closure of supremum of a finite set. (Contributed by Jeff Madsen, 2-Sep-2009)

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

Proof

Step	Hyp	Ref	Expression
1		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)$
2		sotrieq2	$⊢ (R Or A \land (x \in A \land y \in A)) \to (x = y \leftrightarrow (\neg x R y \land \neg y R x))$
3	2	simprbda	$⊢ ((R Or A \land (x \in A \land y \in A)) \land x = y) \to \neg x R y$
4	3	ex	$⊢ (R Or A \land (x \in A \land y \in A)) \to (x = y \to \neg x R y)$
5	4	anassrs	$⊢ ((R Or A \land x \in A) \land y \in A) \to (x = y \to \neg x R y)$
6	5	a1dd	$⊢ ((R Or A \land x \in A) \land y \in A) \to (x = y \to ((x \neq y \to y R x) \to \neg x R y))$
7		pm2.27	$⊢ x \neq y \to ((x \neq y \to y R x) \to y R x)$
8		so2nr	$⊢ (R Or A \land (x \in A \land y \in A)) \to \neg (x R y \land y R x)$
9		pm3.21	$⊢ y R x \to (x R y \to (x R y \land y R x))$
10	9	con3d	$⊢ y R x \to (\neg (x R y \land y R x) \to \neg x R y)$
11	8 10	syl5com	$⊢ (R Or A \land (x \in A \land y \in A)) \to (y R x \to \neg x R y)$
12	11	anassrs	$⊢ ((R Or A \land x \in A) \land y \in A) \to (y R x \to \neg x R y)$
13	7 12	syl9r	$⊢ ((R Or A \land x \in A) \land y \in A) \to (x \neq y \to ((x \neq y \to y R x) \to \neg x R y))$
14	6 13	pm2.61dne	$⊢ ((R Or A \land x \in A) \land y \in A) \to ((x \neq y \to y R x) \to \neg x R y)$
15	14	ralimdva	$⊢ (R Or A \land x \in A) \to (\forall y \in A (x \neq y \to y R x) \to \forall y \in A \neg x R y)$
16		breq2	$⊢ z = x \to (y R z \leftrightarrow y R x)$
17	16	rspcev	$⊢ (x \in A \land y R x) \to \exists z \in A y R z$
18	17	ex	$⊢ x \in A \to (y R x \to \exists z \in A y R z)$
19	18	ralrimivw	$⊢ x \in A \to \forall y \in A (y R x \to \exists z \in A y R z)$
20	19	adantl	$⊢ (R Or A \land x \in A) \to \forall y \in A (y R x \to \exists z \in A y R z)$
21	15 20	jctird	$⊢ (R Or A \land x \in A) \to (\forall y \in A (x \neq y \to y R x) \to (\forall y \in A \neg x R y \land \forall y \in A (y R x \to \exists z \in A y R z)))$
22	21	reximdva	$⊢ R Or A \to (\exists x \in A \forall y \in A (x \neq y \to y R x) \to \exists x \in A (\forall y \in A \neg x R y \land \forall y \in A (y R x \to \exists z \in A y R z)))$
23	22	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) \to \exists x \in A (\forall y \in A \neg x R y \land \forall y \in A (y R x \to \exists z \in A y R z)))$
24	1 23	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 \land \forall y \in A (y R x \to \exists z \in A y R z))$

Metamath Proof Explorer

Theorem fisupg

Proof