Theorem infexd

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

	Ref	Expression
Hypothesis	infexd.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
Assertion	infexd	⊢ ( 𝜑 → inf ( 𝐵 , 𝐴 , 𝑅 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		infexd.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2		df-inf	⊢ inf ( 𝐵 , 𝐴 , 𝑅 ) = sup ( 𝐵 , 𝐴 , ◡ 𝑅 )
3		cnvso	⊢ ( 𝑅 Or 𝐴 ↔ ◡ 𝑅 Or 𝐴 )
4	1 3	sylib	⊢ ( 𝜑 → ◡ 𝑅 Or 𝐴 )
5	4	supexd	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ∈ V )
6	2 5	eqeltrid	⊢ ( 𝜑 → inf ( 𝐵 , 𝐴 , 𝑅 ) ∈ V )