Theorem nfsup 9489

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

Hypotheses

Ref	Expression
nfsup.1	⊢ Ⅎ𝑥𝐴
nfsup.2	⊢ Ⅎ𝑥𝐵
nfsup.3	⊢ Ⅎ𝑥𝑅

Assertion

Ref	Expression
nfsup	⊢ Ⅎ𝑥sup(𝐴, 𝐵, 𝑅)

Proof of Theorem nfsup

Step	Hyp	Ref	Expression
1		dfsup2 9482	. 2 ⊢ sup(𝐴, 𝐵, 𝑅) = ∪ (𝐵 ∖ ((◡𝑅 “ 𝐴) ∪ (𝑅 “ (𝐵 ∖ (◡𝑅 “ 𝐴)))))
2		nfsup.2	. . . 4 ⊢ Ⅎ𝑥𝐵
3		nfsup.3	. . . . . . 7 ⊢ Ⅎ𝑥𝑅
4	3	nfcnv 5892	. . . . . 6 ⊢ Ⅎ𝑥◡𝑅
5		nfsup.1	. . . . . 6 ⊢ Ⅎ𝑥𝐴
6	4, 5	nfima 6088	. . . . 5 ⊢ Ⅎ𝑥(◡𝑅 “ 𝐴)
7	2, 6	nfdif 4139	. . . . . 6 ⊢ Ⅎ𝑥(𝐵 ∖ (◡𝑅 “ 𝐴))
8	3, 7	nfima 6088	. . . . 5 ⊢ Ⅎ𝑥(𝑅 “ (𝐵 ∖ (◡𝑅 “ 𝐴)))
9	6, 8	nfun 4180	. . . 4 ⊢ Ⅎ𝑥((◡𝑅 “ 𝐴) ∪ (𝑅 “ (𝐵 ∖ (◡𝑅 “ 𝐴))))
10	2, 9	nfdif 4139	. . 3 ⊢ Ⅎ𝑥(𝐵 ∖ ((◡𝑅 “ 𝐴) ∪ (𝑅 “ (𝐵 ∖ (◡𝑅 “ 𝐴)))))
11	10	nfuni 4919	. 2 ⊢ Ⅎ𝑥∪ (𝐵 ∖ ((◡𝑅 “ 𝐴) ∪ (𝑅 “ (𝐵 ∖ (◡𝑅 “ 𝐴)))))
12	1, 11	nfcxfr 2901	1 ⊢ Ⅎ𝑥sup(𝐴, 𝐵, 𝑅)

Syntax hints:  Ⅎwnfc 2888   ∖ cdif 3960   ∪ cun 3961  ∪ cuni 4912  ^◡ccnv 5688   “ cima 5692  supcsup 9478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-xp 5695  df-cnv 5697  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-sup 9480

This theorem is referenced by:  nfinf  9520  itg2cnlem1  25811  esum2d  34074  nfwlim  35804  totbndbnd  37776  aomclem8  43050  binomcxplemdvbinom  44349  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  ssfiunibd  45260  uzub  45381  limsupubuz  45669  fourierdlem20  46083  fourierdlem31  46094  fourierdlem79  46141  sge0ltfirp  46356  pimdecfgtioc  46671  decsmflem  46722  smfsup  46770  smfsupxr  46772  smflimsup  46784