Metamath Proof Explorer

Theorem welb

Description: A nonempty subset of a well-ordered set has a lower bound. (Contributed by Jeff Madsen, 2-Sep-2009)

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

Proof

Step	Hyp	Ref	Expression
1		wess	$⊢ B \subseteq A \to (R We A \to R We B)$
2	1	impcom	$⊢ (R We A \land B \subseteq A) \to R We B$
3		weso	$⊢ R We B \to R Or B$
4	2 3	syl	$⊢ (R We A \land B \subseteq A) \to R Or B$
5		cnvso	$⊢ R Or B \leftrightarrow R^{-1} Or B$
6	4 5	sylib	$⊢ (R We A \land B \subseteq A) \to R^{-1} Or B$
7	6	3ad2antr2	$⊢ (R We A \land (B \in C \land B \subseteq A \land B \neq \emptyset)) \to R^{-1} Or B$
8		wefr	$⊢ R We B \to R Fr B$
9	2 8	syl	$⊢ (R We A \land B \subseteq A) \to R Fr B$
10	9	3ad2antr2	$⊢ (R We A \land (B \in C \land B \subseteq A \land B \neq \emptyset)) \to R Fr B$
11		ssidd	$⊢ B \subseteq A \to B \subseteq B$
12	11	3anim2i	$⊢ (B \in C \land B \subseteq A \land B \neq \emptyset) \to (B \in C \land B \subseteq B \land B \neq \emptyset)$
13	12	adantl	$⊢ (R We A \land (B \in C \land B \subseteq A \land B \neq \emptyset)) \to (B \in C \land B \subseteq B \land B \neq \emptyset)$
14		frinfm	$⊢ (R Fr B \land (B \in C \land B \subseteq B \land B \neq \emptyset)) \to \exists x \in B (\forall y \in B \neg x R^{-1} y \land \forall y \in B (y R^{-1} x \to \exists z \in B y R^{-1} z))$
15	10 13 14	syl2anc	$⊢ (R We A \land (B \in C \land B \subseteq A \land B \neq \emptyset)) \to \exists x \in B (\forall y \in B \neg x R^{-1} y \land \forall y \in B (y R^{-1} x \to \exists z \in B y R^{-1} z))$
16	7 15	jca	$⊢ (R We A \land (B \in C \land B \subseteq A \land B \neq \emptyset)) \to (R^{-1} Or B \land \exists x \in B (\forall y \in B \neg x R^{-1} y \land \forall y \in B (y R^{-1} x \to \exists z \in B y R^{-1} z)))$