Metamath Proof Explorer


Theorem suprlubrd

Description: Natural deduction form of specialized suprlub . (Contributed by Stanislas Polu, 9-Mar-2020)

Ref Expression
Hypotheses suprlubrd.1 φA
suprlubrd.2 φA
suprlubrd.3 φxyAyx
suprlubrd.4 φB
suprlubrd.5 φzAB<z
Assertion suprlubrd φB<supA<

Proof

Step Hyp Ref Expression
1 suprlubrd.1 φA
2 suprlubrd.2 φA
3 suprlubrd.3 φxyAyx
4 suprlubrd.4 φB
5 suprlubrd.5 φzAB<z
6 suprlub AAxyAyxBB<supA<zAB<z
7 1 2 3 4 6 syl31anc φB<supA<zAB<z
8 7 bicomd φzAB<zB<supA<
9 8 biimpd φzAB<zB<supA<
10 9 imp φzAB<zB<supA<
11 5 10 mpdan φB<supA<