Metamath Proof Explorer


Theorem ubelsupr

Description: If U belongs to A and U is an upper bound, then U is the sup of A. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Assertion ubelsupr AUAxAxUU=supA<

Proof

Step Hyp Ref Expression
1 simp1 AUAxAxUA
2 simp2 AUAxAxUUA
3 2 ne0d AUAxAxUA
4 1 2 sseldd AUAxAxUU
5 simp3 AUAxAxUxAxU
6 brralrspcev UxAxUyxAxy
7 4 5 6 syl2anc AUAxAxUyxAxy
8 1 3 7 3jca AUAxAxUAAyxAxy
9 suprub AAyxAxyUAUsupA<
10 8 2 9 syl2anc AUAxAxUUsupA<
11 suprleub AAyxAxyUsupA<UxAxU
12 8 4 11 syl2anc AUAxAxUsupA<UxAxU
13 5 12 mpbird AUAxAxUsupA<U
14 suprcl AAyxAxysupA<
15 8 14 syl AUAxAxUsupA<
16 4 15 letri3d AUAxAxUU=supA<UsupA<supA<U
17 10 13 16 mpbir2and AUAxAxUU=supA<