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 ( ∨ℋ ‘ ∅ ) = 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ℋ