Theorem nfinf

Description: Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020)

	Ref	Expression
Hypotheses	nfinf.1	⊢ Ⅎ 𝑥 𝐴
	nfinf.2	⊢ Ⅎ 𝑥 𝐵
	nfinf.3	⊢ Ⅎ 𝑥 𝑅
Assertion	nfinf	⊢ Ⅎ 𝑥 inf ( 𝐴 , 𝐵 , 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		nfinf.1	⊢ Ⅎ 𝑥 𝐴
2		nfinf.2	⊢ Ⅎ 𝑥 𝐵
3		nfinf.3	⊢ Ⅎ 𝑥 𝑅
4		df-inf	⊢ inf ( 𝐴 , 𝐵 , 𝑅 ) = sup ( 𝐴 , 𝐵 , ◡ 𝑅 )
5	3	nfcnv	⊢ Ⅎ 𝑥 ◡ 𝑅
6	1 2 5	nfsup	⊢ Ⅎ 𝑥 sup ( 𝐴 , 𝐵 , ◡ 𝑅 )
7	4 6	nfcxfr	⊢ Ⅎ 𝑥 inf ( 𝐴 , 𝐵 , 𝑅 )