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

Metamath Proof Explorer

Theorem chj1i

Description: Join with Hilbert lattice one. (Contributed by NM, 6-Aug-2004) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	ch0le.1	$⊢ A \in C_{ℋ}$
	Assertion	chj1i	$⊢ A \lor_{ℋ} ℋ = ℋ$

Step	Hyp	Ref	Expression
1		ch0le.1	$⊢ A \in C_{ℋ}$
2		helch	$⊢ ℋ \in C_{ℋ}$
3	1 2	chjcli	$⊢ A \lor_{ℋ} ℋ \in C_{ℋ}$
4	3	chssii	$⊢ A \lor_{ℋ} ℋ \subseteq ℋ$
5	2 1	chub2i	$⊢ ℋ \subseteq A \lor_{ℋ} ℋ$
6	4 5	eqssi	$⊢ A \lor_{ℋ} ℋ = ℋ$