Theorem stcltrlem2

Description: Lemma for strong classical state theorem. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	stcltr1.1	$$⊢\phi \leftrightarrow \left(S\in \mathrm{States}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(\left(S\left(x\right)=1\to S\left(y\right)=1\right)\to x\subseteq y\right)\right)$$
	stcltr1.2	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	stcltrlem1.3	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	stcltrlem2	$$⊢\phi \to B\subseteq \perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap B\right)$$

Proof

Step	Hyp	Ref	Expression
1		stcltr1.1	$$⊢\phi \leftrightarrow \left(S\in \mathrm{States}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(\left(S\left(x\right)=1\to S\left(y\right)=1\right)\to x\subseteq y\right)\right)$$
2		stcltr1.2	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
3		stcltrlem1.3	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
4	1 2 3	stcltrlem1	$$⊢\phi \to \left(S\left(B\right)=1\to S\left(\perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\right)=1\right)$$
5	2	choccli	$$⊢\perp \left(A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
6	2 3	chincli	$$⊢A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
7	5 6	chjcli	$$⊢\perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
8	1 3 7	stcltr1i	$$⊢\phi \to \left(\left(S\left(B\right)=1\to S\left(\perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\right)=1\right)\to B\subseteq \perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
9	4 8	mpd	$$⊢\phi \to B\subseteq \perp \left(A\right){\vee }_{\mathscr{H}}\left(A\cap B\right)$$