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 A U A x A x U U = sup A <

Proof

Step Hyp Ref Expression
1 simp1 A U A x A x U A
2 simp2 A U A x A x U U A
3 2 ne0d A U A x A x U A
4 1 2 sseldd A U A x A x U U
5 simp3 A U A x A x U x A x U
6 brralrspcev U x A x U y x A x y
7 4 5 6 syl2anc A U A x A x U y x A x y
8 1 3 7 3jca A U A x A x U A A y x A x y
9 suprub A A y x A x y U A U sup A <
10 8 2 9 syl2anc A U A x A x U U sup A <
11 suprleub A A y x A x y U sup A < U x A x U
12 8 4 11 syl2anc A U A x A x U sup A < U x A x U
13 5 12 mpbird A U A x A x U sup A < U
14 suprcl A A y x A x y sup A <
15 8 14 syl A U A x A x U sup A <
16 4 15 letri3d A U A x A x U U = sup A < U sup A < sup A < U
17 10 13 16 mpbir2and A U A x A x U U = sup A <