This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sup0

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

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

Proof

Step	Hyp	Ref	Expression
1		sup0riota	$⊢ R Or A \to sup (\emptyset, A, R) = (ι x \in A \| \forall y \in A \neg y R x)$
2	1	3ad2ant1	$⊢ (R Or A \land (X \in A \land \forall y \in A \neg y R X) \land \exists! x \in A \forall y \in A \neg y R x) \to sup (\emptyset, A, R) = (ι x \in A \| \forall y \in A \neg y R x)$
3		simp2r	$⊢ (R Or A \land (X \in A \land \forall y \in A \neg y R X) \land \exists! x \in A \forall y \in A \neg y R x) \to \forall y \in A \neg y R X$
4		simpl	$⊢ (X \in A \land \forall y \in A \neg y R X) \to X \in A$
5	4	anim1i	$⊢ ((X \in A \land \forall y \in A \neg y R X) \land \exists! x \in A \forall y \in A \neg y R x) \to (X \in A \land \exists! x \in A \forall y \in A \neg y R x)$
6	5	3adant1	$⊢ (R Or A \land (X \in A \land \forall y \in A \neg y R X) \land \exists! x \in A \forall y \in A \neg y R x) \to (X \in A \land \exists! x \in A \forall y \in A \neg y R x)$
7		breq2	$⊢ x = X \to (y R x \leftrightarrow y R X)$
8	7	notbid	$⊢ x = X \to (\neg y R x \leftrightarrow \neg y R X)$
9	8	ralbidv	$⊢ x = X \to (\forall y \in A \neg y R x \leftrightarrow \forall y \in A \neg y R X)$
10	9	riota2	$⊢ (X \in A \land \exists! x \in A \forall y \in A \neg y R x) \to (\forall y \in A \neg y R X \leftrightarrow (ι x \in A \| \forall y \in A \neg y R x) = X)$
11	6 10	syl	$⊢ (R Or A \land (X \in A \land \forall y \in A \neg y R X) \land \exists! x \in A \forall y \in A \neg y R x) \to (\forall y \in A \neg y R X \leftrightarrow (ι x \in A \| \forall y \in A \neg y R x) = X)$
12	3 11	mpbid	$⊢ (R Or A \land (X \in A \land \forall y \in A \neg y R X) \land \exists! x \in A \forall y \in A \neg y R x) \to (ι x \in A \| \forall y \in A \neg y R x) = X$
13	2 12	eqtrd	$⊢ (R Or A \land (X \in A \land \forall y \in A \neg y R X) \land \exists! x \in A \forall y \in A \neg y R x) \to sup (\emptyset, A, R) = X$