Theorem infexd

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

	Ref	Expression
Hypothesis	infexd.1	$$⊢\phi \to R\mathrm{Or}A$$
Assertion	infexd	$$⊢\phi \to inf\left(B,A,R\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		infexd.1	$$⊢\phi \to R\mathrm{Or}A$$
2		df-inf	$$⊢inf\left(B,A,R\right)=sup\left(B,A,R^{-1}\right)$$
3		cnvso	$$⊢R\mathrm{Or}A\leftrightarrow R^{-1}\mathrm{Or}A$$
4	1 3	sylib	$$⊢\phi \to R^{-1}\mathrm{Or}A$$
5	4	supexd	$$⊢\phi \to sup\left(B,A,R^{-1}\right)\in \mathrm{V}$$
6	2 5	eqeltrid	$$⊢\phi \to inf\left(B,A,R\right)\in \mathrm{V}$$