Theorem strb

Description: Strong state theorem (bidirectional version). (Contributed by NM, 7-Apr-2001) (New usage is discouraged.)

	Ref	Expression
Hypotheses	str.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	str.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	strb	$$⊢\forall f\in \mathrm{States}\left(f\left(A\right)=1\to f\left(B\right)=1\right)\leftrightarrow A\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		str.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		str.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	stri	$$⊢\forall f\in \mathrm{States}\left(f\left(A\right)=1\to f\left(B\right)=1\right)\to A\subseteq B$$
4	1 2	stlesi	$$⊢f\in \mathrm{States}\to \left(A\subseteq B\to \left(f\left(A\right)=1\to f\left(B\right)=1\right)\right)$$
5	4	com12	$$⊢A\subseteq B\to \left(f\in \mathrm{States}\to \left(f\left(A\right)=1\to f\left(B\right)=1\right)\right)$$
6	5	ralrimiv	$$⊢A\subseteq B\to \forall f\in \mathrm{States}\left(f\left(A\right)=1\to f\left(B\right)=1\right)$$
7	3 6	impbii	$$⊢\forall f\in \mathrm{States}\left(f\left(A\right)=1\to f\left(B\right)=1\right)\leftrightarrow A\subseteq B$$