inflb

Description: An infimum is a lower bound. See also infcl and infglb . (Contributed by AV, 3-Sep-2020)

	Ref	Expression
Hypotheses	infcl.1	$⊢ φ \to R Or A$
	infcl.2	$⊢ φ \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))$
Assertion	inflb	$⊢ φ \to (C \in B \to \neg C R sup (B, A, R))$

Step	Hyp	Ref	Expression
1		infcl.1	$⊢ φ \to R Or A$
2		infcl.2	$⊢ φ \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))$
3		cnvso	$⊢ R Or A \leftrightarrow R^{-1} Or A$
4	1 3	sylib	$⊢ φ \to R^{-1} Or A$
5	1 2	infcllem	$⊢ φ \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))$
6	4 5	supub	$⊢ φ \to (C \in B \to \neg sup (B, A, R^{-1}) R^{-1} C)$
7	6	imp	$⊢ (φ \land C \in B) \to \neg sup (B, A, R^{-1}) R^{-1} C$
8		df-inf	$⊢ sup (B, A, R) = sup (B, A, R^{-1})$
9	8	a1i	$⊢ (φ \land C \in B) \to sup (B, A, R) = sup (B, A, R^{-1})$
10	9	breq2d	$⊢ (φ \land C \in B) \to (C R sup (B, A, R) \leftrightarrow C R sup (B, A, R^{-1}))$
11	4 5	supcl	$⊢ φ \to sup (B, A, R^{-1}) \in A$
12		brcnvg	$⊢ (sup (B, A, R^{-1}) \in A \land C \in B) \to (sup (B, A, R^{-1}) R^{-1} C \leftrightarrow C R sup (B, A, R^{-1}))$
13	12	bicomd	$⊢ (sup (B, A, R^{-1}) \in A \land C \in B) \to (C R sup (B, A, R^{-1}) \leftrightarrow sup (B, A, R^{-1}) R^{-1} C)$
14	11 13	sylan	$⊢ (φ \land C \in B) \to (C R sup (B, A, R^{-1}) \leftrightarrow sup (B, A, R^{-1}) R^{-1} C)$
15	10 14	bitrd	$⊢ (φ \land C \in B) \to (C R sup (B, A, R) \leftrightarrow sup (B, A, R^{-1}) R^{-1} C)$
16	7 15	mtbird	$⊢ (φ \land C \in B) \to \neg C R sup (B, A, R)$
17	16	ex	$⊢ φ \to (C \in B \to \neg C R sup (B, A, R))$

Metamath Proof Explorer