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 ⊢ Ⅎ 𝑥 𝐴
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 ( 𝐴 , 𝐵 , 𝑅 )