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ℋ