fiinfg

Description: Lemma showing existence and closure of infimum of a finite set. (Contributed by AV, 6-Oct-2020)

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

Proof

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

Metamath Proof Explorer

Theorem fiinfg

Proof