frinfm

Description: A subset of a well-founded set has an infimum. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	frinfm	$⊢ (R Fr A \land (B \in C \land B \subseteq A \land B \neq \emptyset)) \to \exists x \in A (\forall y \in B \neg x R^{-1} y \land \forall y \in A (y R^{-1} x \to \exists z \in B y R^{-1} z))$

Proof

Step	Hyp	Ref	Expression
1		fri	$⊢ ((B \in C \land R Fr A) \land (B \subseteq A \land B \neq \emptyset)) \to \exists x \in B \forall y \in B \neg y R x$
2	1	ancom1s	$⊢ ((R Fr A \land B \in C) \land (B \subseteq A \land B \neq \emptyset)) \to \exists x \in B \forall y \in B \neg y R x$
3	2	exp43	$⊢ R Fr A \to (B \in C \to (B \subseteq A \to (B \neq \emptyset \to \exists x \in B \forall y \in B \neg y R x)))$
4	3	3imp2	$⊢ (R Fr A \land (B \in C \land B \subseteq A \land B \neq \emptyset)) \to \exists x \in B \forall y \in B \neg y R x$
5		ssel2	$⊢ (B \subseteq A \land x \in B) \to x \in A$
6	5	adantrr	$⊢ (B \subseteq A \land (x \in B \land \forall y \in B \neg y R x)) \to x \in A$
7		vex	$⊢ x \in V$
8		vex	$⊢ y \in V$
9	7 8	brcnv	$⊢ x R^{-1} y \leftrightarrow y R x$
10	9	biimpi	$⊢ x R^{-1} y \to y R x$
11	10	con3i	$⊢ \neg y R x \to \neg x R^{-1} y$
12	11	ralimi	$⊢ \forall y \in B \neg y R x \to \forall y \in B \neg x R^{-1} y$
13	12	ad2antll	$⊢ (B \subseteq A \land (x \in B \land \forall y \in B \neg y R x)) \to \forall y \in B \neg x R^{-1} y$
14		breq2	$⊢ z = x \to (y R^{-1} z \leftrightarrow y R^{-1} x)$
15	14	rspcev	$⊢ (x \in B \land y R^{-1} x) \to \exists z \in B y R^{-1} z$
16	15	ex	$⊢ x \in B \to (y R^{-1} x \to \exists z \in B y R^{-1} z)$
17	16	ralrimivw	$⊢ x \in B \to \forall y \in A (y R^{-1} x \to \exists z \in B y R^{-1} z)$
18	17	ad2antrl	$⊢ (B \subseteq A \land (x \in B \land \forall y \in B \neg y R x)) \to \forall y \in A (y R^{-1} x \to \exists z \in B y R^{-1} z)$
19	6 13 18	jca32	$⊢ (B \subseteq A \land (x \in B \land \forall y \in B \neg y R x)) \to (x \in A \land (\forall y \in B \neg x R^{-1} y \land \forall y \in A (y R^{-1} x \to \exists z \in B y R^{-1} z)))$
20	19	ex	$⊢ B \subseteq A \to ((x \in B \land \forall y \in B \neg y R x) \to (x \in A \land (\forall y \in B \neg x R^{-1} y \land \forall y \in A (y R^{-1} x \to \exists z \in B y R^{-1} z))))$
21	20	reximdv2	$⊢ B \subseteq A \to (\exists x \in B \forall y \in B \neg y R x \to \exists x \in A (\forall y \in B \neg x R^{-1} y \land \forall y \in A (y R^{-1} x \to \exists z \in B y R^{-1} z)))$
22	21	adantl	$⊢ (R Fr A \land B \subseteq A) \to (\exists x \in B \forall y \in B \neg y R x \to \exists x \in A (\forall y \in B \neg x R^{-1} y \land \forall y \in A (y R^{-1} x \to \exists z \in B y R^{-1} z)))$
23	22	3ad2antr2	$⊢ (R Fr A \land (B \in C \land B \subseteq A \land B \neq \emptyset)) \to (\exists x \in B \forall y \in B \neg y R x \to \exists x \in A (\forall y \in B \neg x R^{-1} y \land \forall y \in A (y R^{-1} x \to \exists z \in B y R^{-1} z)))$
24	4 23	mpd	$⊢ (R Fr A \land (B \in C \land B \subseteq A \land B \neq \emptyset)) \to \exists x \in A (\forall y \in B \neg x R^{-1} y \land \forall y \in A (y R^{-1} x \to \exists z \in B y R^{-1} z))$

Metamath Proof Explorer

Theorem frinfm

Proof