Metamath Proof Explorer


Theorem chsup0

Description: The supremum of the empty set. (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

Ref Expression
Assertion chsup0 = 0

Proof

Step Hyp Ref Expression
1 0ss 0
2 0ss C
3 h0elch 0 C
4 snssi 0 C 0 C
5 3 4 ax-mp 0 C
6 chsupss C 0 C 0 0
7 2 5 6 mp2an 0 0
8 1 7 ax-mp 0
9 chsupsn 0 C 0 = 0
10 3 9 ax-mp 0 = 0
11 8 10 sseqtri 0
12 chsupcl C C
13 2 12 ax-mp C
14 13 chle0i 0 = 0
15 11 14 mpbi = 0