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 ℋ