Theorem nfsup

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

	Ref	Expression
Hypotheses	nfsup.1	⊢ Ⅎ 𝑥 𝐴
	nfsup.2	⊢ Ⅎ 𝑥 𝐵
	nfsup.3	⊢ Ⅎ 𝑥 𝑅
Assertion	nfsup	⊢ Ⅎ 𝑥 sup ( 𝐴 , 𝐵 , 𝑅 )

Proof

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