Theorem chnlei

Description: Equivalent expressions for "not less than" in the Hilbert lattice. (Contributed by NM, 5-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ch0le.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	chjcl.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	chnlei	$$⊢\neg B\subseteq A\leftrightarrow A\subset A{\vee }_{\mathscr{H}}B$$

Proof

Step	Hyp	Ref	Expression
1		ch0le.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		chjcl.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	chub1i	$$⊢A\subseteq A{\vee }_{\mathscr{H}}B$$
4	3	biantrur	$$⊢\neg A=A{\vee }_{\mathscr{H}}B\leftrightarrow \left(A\subseteq A{\vee }_{\mathscr{H}}B\wedge \neg A=A{\vee }_{\mathscr{H}}B\right)$$
5	2 1	chlejb1i	$$⊢B\subseteq A\leftrightarrow B{\vee }_{\mathscr{H}}A=A$$
6		eqcom	$$⊢B{\vee }_{\mathscr{H}}A=A\leftrightarrow A=B{\vee }_{\mathscr{H}}A$$
7	2 1	chjcomi	$$⊢B{\vee }_{\mathscr{H}}A=A{\vee }_{\mathscr{H}}B$$
8	7	eqeq2i	$$⊢A=B{\vee }_{\mathscr{H}}A\leftrightarrow A=A{\vee }_{\mathscr{H}}B$$
9	5 6 8	3bitri	$$⊢B\subseteq A\leftrightarrow A=A{\vee }_{\mathscr{H}}B$$
10	9	notbii	$$⊢\neg B\subseteq A\leftrightarrow \neg A=A{\vee }_{\mathscr{H}}B$$
11		dfpss2	$$⊢A\subset A{\vee }_{\mathscr{H}}B\leftrightarrow \left(A\subseteq A{\vee }_{\mathscr{H}}B\wedge \neg A=A{\vee }_{\mathscr{H}}B\right)$$
12	4 10 11	3bitr4i	$$⊢\neg B\subseteq A\leftrightarrow A\subset A{\vee }_{\mathscr{H}}B$$