Theorem infexd

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

	Ref	Expression
Hypothesis	infexd.1	|- ( ph -> R Or A )
Assertion	infexd	|- ( ph -> inf ( B , A , R ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		infexd.1	|- ( ph -> R Or A )
2		df-inf	|- inf ( B , A , R ) = sup ( B , A , `' R )
3		cnvso	|- ( R Or A <-> `' R Or A )
4	1 3	sylib	|- ( ph -> `' R Or A )
5	4	supexd	|- ( ph -> sup ( B , A , `' R ) e. _V )
6	2 5	eqeltrid	|- ( ph -> inf ( B , A , R ) e. _V )