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

Metamath Proof Explorer

Theorem infexd

Description: An infimum is a set. (Contributed by AV, 2-Sep-2020)

		Ref	Expression
	Hypothesis	infexd.1	$⊢ φ \to R Or A$
	Assertion	infexd	$⊢ φ \to inf (B, A, R) \in V$

Step	Hyp	Ref	Expression
1		infexd.1	$⊢ φ \to R Or A$
2		df-inf	$⊢ inf (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	supexd	$⊢ φ \to sup (B, A, R^{-1}) \in V$
6	2 5	eqeltrid	$⊢ φ \to inf (B, A, R) \in V$