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 ⊢ Ⅎ _ x A
nfsup.2 ⊢ Ⅎ _ x B
nfsup.3 ⊢ Ⅎ _ x R
Assertion nfsup ⊢ Ⅎ _ x sup A B R

Proof

Step Hyp Ref Expression
1 nfsup.1 ⊢ Ⅎ _ x A
2 nfsup.2 ⊢ Ⅎ _ x B
3 nfsup.3 ⊢ Ⅎ _ x R
4 dfsup2 ⊢ sup A B R = ⋃ B ∖ R -1 A ∪ R B ∖ R -1 A
5 3 nfcnv ⊢ Ⅎ _ x R -1
6 5 1 nfima ⊢ Ⅎ _ x R -1 A
7 2 6 nfdif ⊢ Ⅎ _ x B ∖ R -1 A
8 3 7 nfima ⊢ Ⅎ _ x R B ∖ R -1 A
9 6 8 nfun ⊢ Ⅎ _ x R -1 A ∪ R B ∖ R -1 A
10 2 9 nfdif ⊢ Ⅎ _ x B ∖ R -1 A ∪ R B ∖ R -1 A
11 10 nfuni ⊢ Ⅎ _ x ⋃ B ∖ R -1 A ∪ R B ∖ R -1 A
12 4 11 nfcxfr ⊢ Ⅎ _ x sup A B R