Theorem nfinf

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

	Ref	Expression
Hypotheses	nfinf.1	|- F/_ x A
	nfinf.2	|- F/_ x B
	nfinf.3	|- F/_ x R
Assertion	nfinf	|- F/_ x inf ( A , B , R )

Proof

Step	Hyp	Ref	Expression
1		nfinf.1	|- F/_ x A
2		nfinf.2	|- F/_ x B
3		nfinf.3	|- F/_ x R
4		df-inf	|- inf ( A , B , R ) = sup ( A , B , `' R )
5	3	nfcnv	|- F/_ x `' R
6	1 2 5	nfsup	|- F/_ x sup ( A , B , `' R )
7	4 6	nfcxfr	|- F/_ x inf ( A , B , R )