This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( \/H ` (/) ) = 0H

Proof

Step Hyp Ref Expression
1 0ss 
 |-  (/) C_ { 0H }
2 0ss 
 |-  (/) C_ CH
3 h0elch 
 |-  0H e. CH
4 snssi 
 |-  ( 0H e. CH -> { 0H } C_ CH )
5 3 4 ax-mp 
 |-  { 0H } C_ CH
6 chsupss 
 |-  ( ( (/) C_ CH /\ { 0H } C_ CH ) -> ( (/) C_ { 0H } -> ( \/H ` (/) ) C_ ( \/H ` { 0H } ) ) )
7 2 5 6 mp2an 
 |-  ( (/) C_ { 0H } -> ( \/H ` (/) ) C_ ( \/H ` { 0H } ) )
8 1 7 ax-mp 
 |-  ( \/H ` (/) ) C_ ( \/H ` { 0H } )
9 chsupsn 
 |-  ( 0H e. CH -> ( \/H ` { 0H } ) = 0H )
10 3 9 ax-mp 
 |-  ( \/H ` { 0H } ) = 0H
11 8 10 sseqtri 
 |-  ( \/H ` (/) ) C_ 0H
12 chsupcl 
 |-  ( (/) C_ CH -> ( \/H ` (/) ) e. CH )
13 2 12 ax-mp 
 |-  ( \/H ` (/) ) e. CH
14 13 chle0i 
 |-  ( ( \/H ` (/) ) C_ 0H <-> ( \/H ` (/) ) = 0H )
15 11 14 mpbi 
 |-  ( \/H ` (/) ) = 0H