weinflb

Description: In a well-order, an infimum is a lower bound. (Contributed by Thierry Arnoux, 29-Oct-2026)

	Ref	Expression
Hypotheses	weinflb.1	$⊢ φ \to Rel R$
	weinflb.2	$⊢ φ \to R We A$
	weinflb.3	$⊢ φ \to B \in V$
	weinflb.4	$⊢ φ \to B \subseteq A$
	weinflb.5	$⊢ φ \to B \neq \emptyset$
	weinflb.6	$⊢ φ \to C \in B$
Assertion	weinflb	$⊢ φ \to \neg C R inf (B, A, R)$

Proof

Step	Hyp	Ref	Expression
1		weinflb.1	$⊢ φ \to Rel R$
2		weinflb.2	$⊢ φ \to R We A$
3		weinflb.3	$⊢ φ \to B \in V$
4		weinflb.4	$⊢ φ \to B \subseteq A$
5		weinflb.5	$⊢ φ \to B \neq \emptyset$
6		weinflb.6	$⊢ φ \to C \in B$
7		weso	$⊢ R We A \to R Or A$
8	2 7	syl	$⊢ φ \to R Or A$
9		welb	$⊢ (R We A \land (B \in V \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)))$
10	2 3 4 5 9	syl13anc	$⊢ φ \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)))$
11	10	simprd	$⊢ φ \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))$
12	4	sselda	$⊢ (φ \land x \in B) \to x \in A$
13	12	adantrr	$⊢ (φ \land (x \in B \land (\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)))) \to x \in A$
14		brcnvg	$⊢ (x \in B \land y \in B) \to (x R^{-1} y \leftrightarrow y R x)$
15	14	notbid	$⊢ (x \in B \land y \in B) \to (\neg x R^{-1} y \leftrightarrow \neg y R x)$
16	15	ralbidva	$⊢ x \in B \to (\forall y \in B \neg x R^{-1} y \leftrightarrow \forall y \in B \neg y R x)$
17	16	biimpa	$⊢ (x \in B \land \forall y \in B \neg x R^{-1} y) \to \forall y \in B \neg y R x$
18	17	adantll	$⊢ ((φ \land x \in B) \land \forall y \in B \neg x R^{-1} y) \to \forall y \in B \neg y R x$
19		breq1	$⊢ z = x \to (z R y \leftrightarrow x R y)$
20		simpllr	$⊢ (((φ \land x \in B) \land y \in A) \land x R y) \to x \in B$
21		simpr	$⊢ (((φ \land x \in B) \land y \in A) \land x R y) \to x R y$
22	19 20 21	rspcedvdw	$⊢ (((φ \land x \in B) \land y \in A) \land x R y) \to \exists z \in B z R y$
23	22	ex	$⊢ ((φ \land x \in B) \land y \in A) \to (x R y \to \exists z \in B z R y)$
24	23	ralrimiva	$⊢ (φ \land x \in B) \to \forall y \in A (x R y \to \exists z \in B z R y)$
25	24	adantr	$⊢ ((φ \land x \in B) \land \forall y \in B (y R^{-1} x \to \exists z \in B y R^{-1} z)) \to \forall y \in A (x R y \to \exists z \in B z R y)$
26	18 25	anim12dan	$⊢ ((φ \land x \in B) \land (\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))) \to (\forall y \in B \neg y R x \land \forall y \in A (x R y \to \exists z \in B z R y))$
27	26	anasss	$⊢ (φ \land (x \in B \land (\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)))) \to (\forall y \in B \neg y R x \land \forall y \in A (x R y \to \exists z \in B z R y))$
28	11 13 27	reximssdv	$⊢ φ \to \exists x \in A (\forall y \in B \neg y R x \land \forall y \in A (x R y \to \exists z \in B z R y))$
29	8 28	inflb	$⊢ φ \to (C \in B \to \neg C R inf (B, A, R))$
30	6 29	mpd	$⊢ φ \to \neg C R inf (B, A, R)$

Metamath Proof Explorer

Theorem weinflb

Proof