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

Metamath Proof Explorer

Theorem chj0i

Description: Join with lattice zero in CH . (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis ch0le.1 ⊢ A ∈ C ℋ
Assertion chj0i ⊢ A ∨ ℋ 0 ℋ = A

Proof

Step Hyp Ref Expression
1 ch0le.1 ⊢ A ∈ C ℋ
2 h0elch ⊢ 0 ℋ ∈ C ℋ
3 1 2 chjvali ⊢ A ∨ ℋ 0 ℋ = ⊥ ⁡ ⊥ ⁡ A ∪ 0 ℋ
4 1 ch0lei ⊢ 0 ℋ ⊆ A
5 ssequn2 ⊢ 0 ℋ ⊆ A ↔ A ∪ 0 ℋ = A
6 4 5 mpbi ⊢ A ∪ 0 ℋ = A
7 6 fveq2i ⊢ ⊥ ⁡ A ∪ 0 ℋ = ⊥ ⁡ A
8 7 fveq2i ⊢ ⊥ ⁡ ⊥ ⁡ A ∪ 0 ℋ = ⊥ ⁡ ⊥ ⁡ A
9 1 pjococi ⊢ ⊥ ⁡ ⊥ ⁡ A = A
10 3 8 9 3eqtri ⊢ A ∨ ℋ 0 ℋ = A