Theorem chj0i

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

	Ref	Expression
Hypothesis	ch0le.1	⊢ 𝐴 ∈ Cℋ
Assertion	chj0i	⊢ ( 𝐴 ∨ℋ 0ℋ ) = 𝐴

Proof

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