Theorem stm1i

Description: State of component of unit meet. (Contributed by NM, 11-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	stle.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	stle.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	stm1i	$$⊢S\in \mathrm{States}\to \left(S\left(A\cap B\right)=1\to S\left(A\right)=1\right)$$

Proof

Step	Hyp	Ref	Expression
1		stle.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		stle.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		inss1	$$⊢A\cap B\subseteq A$$
4	1 2	chincli	$$⊢A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
5	4 1	stlei	$$⊢S\in \mathrm{States}\to \left(A\cap B\subseteq A\to S\left(A\cap B\right)\le S\left(A\right)\right)$$
6	3 5	mpi	$$⊢S\in \mathrm{States}\to S\left(A\cap B\right)\le S\left(A\right)$$
7		breq1	$$⊢S\left(A\cap B\right)=1\to \left(S\left(A\cap B\right)\le S\left(A\right)\leftrightarrow 1\le S\left(A\right)\right)$$
8	6 7	syl5ibcom	$$⊢S\in \mathrm{States}\to \left(S\left(A\cap B\right)=1\to 1\le S\left(A\right)\right)$$
9	1	stge1i	$$⊢S\in \mathrm{States}\to \left(1\le S\left(A\right)\leftrightarrow S\left(A\right)=1\right)$$
10	8 9	sylibd	$$⊢S\in \mathrm{States}\to \left(S\left(A\cap B\right)=1\to S\left(A\right)=1\right)$$