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