This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )