eqinf

Description: Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 2-Sep-2020)

		Ref	Expression
	Hypothesis	infexd.1	$⊢ φ \to R Or A$
	Assertion	eqinf	$⊢ φ \to ((C \in A \land \forall y \in B \neg y R C \land \forall y \in A (C R y \to \exists z \in B z R y)) \to sup (B, A, R) = C)$

Proof

Step	Hyp	Ref	Expression
1		infexd.1	$⊢ φ \to R Or A$
2		df-inf	$⊢ sup (B, A, R) = sup (B, A, R^{-1})$
3		cnvso	$⊢ R Or A \leftrightarrow R^{-1} Or A$
4	1 3	sylib	$⊢ φ \to R^{-1} Or A$
5	4	eqsup	$⊢ φ \to ((C \in A \land \forall y \in B \neg C R^{-1} y \land \forall y \in A (y R^{-1} C \to \exists z \in B y R^{-1} z)) \to sup (B, A, R^{-1}) = C)$
6		brcnvg	$⊢ (C \in A \land y \in V) \to (C R^{-1} y \leftrightarrow y R C)$
7	6	bicomd	$⊢ (C \in A \land y \in V) \to (y R C \leftrightarrow C R^{-1} y)$
8	7	elvd	$⊢ C \in A \to (y R C \leftrightarrow C R^{-1} y)$
9	8	notbid	$⊢ C \in A \to (\neg y R C \leftrightarrow \neg C R^{-1} y)$
10	9	ralbidv	$⊢ C \in A \to (\forall y \in B \neg y R C \leftrightarrow \forall y \in B \neg C R^{-1} y)$
11		vex	$⊢ y \in V$
12		brcnvg	$⊢ (y \in V \land C \in A) \to (y R^{-1} C \leftrightarrow C R y)$
13	11 12	mpan	$⊢ C \in A \to (y R^{-1} C \leftrightarrow C R y)$
14	13	bicomd	$⊢ C \in A \to (C R y \leftrightarrow y R^{-1} C)$
15		vex	$⊢ z \in V$
16	11 15	brcnv	$⊢ y R^{-1} z \leftrightarrow z R y$
17	16	a1i	$⊢ C \in A \to (y R^{-1} z \leftrightarrow z R y)$
18	17	bicomd	$⊢ C \in A \to (z R y \leftrightarrow y R^{-1} z)$
19	18	rexbidv	$⊢ C \in A \to (\exists z \in B z R y \leftrightarrow \exists z \in B y R^{-1} z)$
20	14 19	imbi12d	$⊢ C \in A \to ((C R y \to \exists z \in B z R y) \leftrightarrow (y R^{-1} C \to \exists z \in B y R^{-1} z))$
21	20	ralbidv	$⊢ C \in A \to (\forall y \in A (C R y \to \exists z \in B z R y) \leftrightarrow \forall y \in A (y R^{-1} C \to \exists z \in B y R^{-1} z))$
22	10 21	anbi12d	$⊢ C \in A \to ((\forall y \in B \neg y R C \land \forall y \in A (C R y \to \exists z \in B z R y)) \leftrightarrow (\forall y \in B \neg C R^{-1} y \land \forall y \in A (y R^{-1} C \to \exists z \in B y R^{-1} z)))$
23	22	pm5.32i	$⊢ (C \in A \land (\forall y \in B \neg y R C \land \forall y \in A (C R y \to \exists z \in B z R y))) \leftrightarrow (C \in A \land (\forall y \in B \neg C R^{-1} y \land \forall y \in A (y R^{-1} C \to \exists z \in B y R^{-1} z)))$
24		3anass	$⊢ (C \in A \land \forall y \in B \neg y R C \land \forall y \in A (C R y \to \exists z \in B z R y)) \leftrightarrow (C \in A \land (\forall y \in B \neg y R C \land \forall y \in A (C R y \to \exists z \in B z R y)))$
25		3anass	$⊢ (C \in A \land \forall y \in B \neg C R^{-1} y \land \forall y \in A (y R^{-1} C \to \exists z \in B y R^{-1} z)) \leftrightarrow (C \in A \land (\forall y \in B \neg C R^{-1} y \land \forall y \in A (y R^{-1} C \to \exists z \in B y R^{-1} z)))$
26	23 24 25	3bitr4i	$⊢ (C \in A \land \forall y \in B \neg y R C \land \forall y \in A (C R y \to \exists z \in B z R y)) \leftrightarrow (C \in A \land \forall y \in B \neg C R^{-1} y \land \forall y \in A (y R^{-1} C \to \exists z \in B y R^{-1} z))$
27	26	biimpi	$⊢ (C \in A \land \forall y \in B \neg y R C \land \forall y \in A (C R y \to \exists z \in B z R y)) \to (C \in A \land \forall y \in B \neg C R^{-1} y \land \forall y \in A (y R^{-1} C \to \exists z \in B y R^{-1} z))$
28	5 27	impel	$⊢ (φ \land (C \in A \land \forall y \in B \neg y R C \land \forall y \in A (C R y \to \exists z \in B z R y))) \to sup (B, A, R^{-1}) = C$
29	2 28	syl5eq	$⊢ (φ \land (C \in A \land \forall y \in B \neg y R C \land \forall y \in A (C R y \to \exists z \in B z R y))) \to sup (B, A, R) = C$
30	29	ex	$⊢ φ \to ((C \in A \land \forall y \in B \neg y R C \land \forall y \in A (C R y \to \exists z \in B z R y)) \to sup (B, A, R) = C)$

Metamath Proof Explorer

Theorem eqinf

Proof