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 {\mathbf{C}}_{\mathscr{H}}$$
Assertion	chj1i	$$⊢A{\vee }_{\mathscr{H}}\mathscr{H}=\mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		ch0le.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		helch	$$⊢\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	chjcli	$$⊢A{\vee }_{\mathscr{H}}\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}$$
4	3	chssii	$$⊢A{\vee }_{\mathscr{H}}\mathscr{H}\subseteq \mathscr{H}$$
5	2 1	chub2i	$$⊢\mathscr{H}\subseteq A{\vee }_{\mathscr{H}}\mathscr{H}$$
6	4 5	eqssi	$$⊢A{\vee }_{\mathscr{H}}\mathscr{H}=\mathscr{H}$$