Theorem nfinf

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

	Ref	Expression
Hypotheses	nfinf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	nfinf.2	$$⊢\underset{\_}{Ⅎ}xB$$
	nfinf.3	$$⊢\underset{\_}{Ⅎ}xR$$
Assertion	nfinf	$$⊢\underset{\_}{Ⅎ}xsup\left(A,B,R\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfinf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfinf.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		nfinf.3	$$⊢\underset{\_}{Ⅎ}xR$$
4		df-inf	$$⊢sup\left(A,B,R\right)=sup\left(A,B,R^{-1}\right)$$
5	3	nfcnv	$$⊢\underset{\_}{Ⅎ}x{R}^{-1}$$
6	1 2 5	nfsup	$$⊢\underset{\_}{Ⅎ}xsup\left(A,B,R^{-1}\right)$$
7	4 6	nfcxfr	$$⊢\underset{\_}{Ⅎ}xsup\left(A,B,R\right)$$