Metamath Proof Explorer

Theorem infempty

Description: The infimum of an empty set under a base set which has a unique greatest element is the greatest element of the base set. (Contributed by AV, 4-Sep-2020)

		Ref	Expression
	Assertion	infempty	$⊢ (R Or A \land (X \in A \land \forall y \in A \neg X R y) \land \exists! x \in A \forall y \in A \neg x R y) \to inf (\emptyset, A, R) = X$

Proof

Step	Hyp	Ref	Expression
1		df-inf	$⊢ inf (\emptyset, A, R) = sup (\emptyset, A, R^{-1})$
2		cnvso	$⊢ R Or A \leftrightarrow R^{-1} Or A$
3		brcnvg	$⊢ (y \in A \land X \in A) \to (y R^{-1} X \leftrightarrow X R y)$
4	3	ancoms	$⊢ (X \in A \land y \in A) \to (y R^{-1} X \leftrightarrow X R y)$
5	4	bicomd	$⊢ (X \in A \land y \in A) \to (X R y \leftrightarrow y R^{-1} X)$
6	5	notbid	$⊢ (X \in A \land y \in A) \to (\neg X R y \leftrightarrow \neg y R^{-1} X)$
7	6	ralbidva	$⊢ X \in A \to (\forall y \in A \neg X R y \leftrightarrow \forall y \in A \neg y R^{-1} X)$
8	7	pm5.32i	$⊢ (X \in A \land \forall y \in A \neg X R y) \leftrightarrow (X \in A \land \forall y \in A \neg y R^{-1} X)$
9		brcnvg	$⊢ (y \in A \land x \in A) \to (y R^{-1} x \leftrightarrow x R y)$
10	9	ancoms	$⊢ (x \in A \land y \in A) \to (y R^{-1} x \leftrightarrow x R y)$
11	10	bicomd	$⊢ (x \in A \land y \in A) \to (x R y \leftrightarrow y R^{-1} x)$
12	11	notbid	$⊢ (x \in A \land y \in A) \to (\neg x R y \leftrightarrow \neg y R^{-1} x)$
13	12	ralbidva	$⊢ x \in A \to (\forall y \in A \neg x R y \leftrightarrow \forall y \in A \neg y R^{-1} x)$
14	13	reubiia	$⊢ \exists! x \in A \forall y \in A \neg x R y \leftrightarrow \exists! x \in A \forall y \in A \neg y R^{-1} x$
15		sup0	$⊢ (R^{-1} Or A \land (X \in A \land \forall y \in A \neg y R^{-1} X) \land \exists! x \in A \forall y \in A \neg y R^{-1} x) \to sup (\emptyset, A, R^{-1}) = X$
16	2 8 14 15	syl3anb	$⊢ (R Or A \land (X \in A \land \forall y \in A \neg X R y) \land \exists! x \in A \forall y \in A \neg x R y) \to sup (\emptyset, A, R^{-1}) = X$
17	1 16	eqtrid	$⊢ (R Or A \land (X \in A \land \forall y \in A \neg X R y) \land \exists! x \in A \forall y \in A \neg x R y) \to inf (\emptyset, A, R) = X$