Theorem nfsup

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

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

Proof

Step	Hyp	Ref	Expression
1		nfsup.1	|- F/_ x A
2		nfsup.2	|- F/_ x B
3		nfsup.3	|- F/_ x R
4		dfsup2	|- sup ( A , B , R ) = U. ( B \ ( ( `' R " A ) u. ( R " ( B \ ( `' R " A ) ) ) ) )
5	3	nfcnv	|- F/_ x `' R
6	5 1	nfima	|- F/_ x ( `' R " A )
7	2 6	nfdif	|- F/_ x ( B \ ( `' R " A ) )
8	3 7	nfima	|- F/_ x ( R " ( B \ ( `' R " A ) ) )
9	6 8	nfun	|- F/_ x ( ( `' R " A ) u. ( R " ( B \ ( `' R " A ) ) ) )
10	2 9	nfdif	|- F/_ x ( B \ ( ( `' R " A ) u. ( R " ( B \ ( `' R " A ) ) ) ) )
11	10	nfuni	|- F/_ x U. ( B \ ( ( `' R " A ) u. ( R " ( B \ ( `' R " A ) ) ) ) )
12	4 11	nfcxfr	|- F/_ x sup ( A , B , R )