Theorem nfsup

Description: Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014)

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

Proof

Step	Hyp	Ref	Expression
1		nfsup.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfsup.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		nfsup.3	$$⊢\underset{\_}{Ⅎ}xR$$
4		dfsup2	$$⊢sup\left(A,B,R\right)=\bigcup \left(B\setminus \left(R^{-1}\left[A\right]\cup R\left[B\setminus R^{-1}\left[A\right]\right]\right)\right)$$
5	3	nfcnv	$$⊢\underset{\_}{Ⅎ}x{R}^{-1}$$
6	5 1	nfima	$$⊢\underset{\_}{Ⅎ}x{R}^{-1}\left[A\right]$$
7	2 6	nfdif	$$⊢\underset{\_}{Ⅎ}x\left(B\setminus R^{-1}\left[A\right]\right)$$
8	3 7	nfima	$$⊢\underset{\_}{Ⅎ}xR\left[B\setminus R^{-1}\left[A\right]\right]$$
9	6 8	nfun	$$⊢\underset{\_}{Ⅎ}x\left(R^{-1}\left[A\right]\cup R\left[B\setminus R^{-1}\left[A\right]\right]\right)$$
10	2 9	nfdif	$$⊢\underset{\_}{Ⅎ}x\left(B\setminus \left(R^{-1}\left[A\right]\cup R\left[B\setminus R^{-1}\left[A\right]\right]\right)\right)$$
11	10	nfuni	$$⊢\underset{\_}{Ⅎ}x\bigcup \left(B\setminus \left(R^{-1}\left[A\right]\cup R\left[B\setminus R^{-1}\left[A\right]\right]\right)\right)$$
12	4 11	nfcxfr	$$⊢\underset{\_}{Ⅎ}xsup\left(A,B,R\right)$$