Metamath Proof Explorer


Theorem nfinf

Description: Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020)

Ref Expression
Hypotheses nfinf.1 _xA
nfinf.2 _xB
nfinf.3 _xR
Assertion nfinf _xsupABR

Proof

Step Hyp Ref Expression
1 nfinf.1 _xA
2 nfinf.2 _xB
3 nfinf.3 _xR
4 df-inf supABR=supABR-1
5 3 nfcnv _xR-1
6 1 2 5 nfsup _xsupABR-1
7 4 6 nfcxfr _xsupABR