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

Metamath Proof Explorer

Theorem chj0

Description: Join with Hilbert lattice zero. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion chj0 ⊢ A ∈ C ℋ → A ∨ ℋ 0 ℋ = A

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ A = if A ∈ C ℋ A 0 ℋ → A ∨ ℋ 0 ℋ = if A ∈ C ℋ A 0 ℋ ∨ ℋ 0 ℋ
2 id ⊢ A = if A ∈ C ℋ A 0 ℋ → A = if A ∈ C ℋ A 0 ℋ
3 1 2 eqeq12d ⊢ A = if A ∈ C ℋ A 0 ℋ → A ∨ ℋ 0 ℋ = A ↔ if A ∈ C ℋ A 0 ℋ ∨ ℋ 0 ℋ = if A ∈ C ℋ A 0 ℋ
4 h0elch ⊢ 0 ℋ ∈ C ℋ
5 4 elimel ⊢ if A ∈ C ℋ A 0 ℋ ∈ C ℋ
6 5 chj0i ⊢ if A ∈ C ℋ A 0 ℋ ∨ ℋ 0 ℋ = if A ∈ C ℋ A 0 ℋ
7 3 6 dedth ⊢ A ∈ C ℋ → A ∨ ℋ 0 ℋ = A