Theorem hstrbi

Description: Strong CH-state theorem (bidirectional version). Theorem in Mayet3 p. 10 and its converse. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hstr.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	hstr.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	hstrbi	$$⊢\forall f\in \mathrm{CHStates}\left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)\leftrightarrow A\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		hstr.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		hstr.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	hstri	$$⊢\forall f\in \mathrm{CHStates}\left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)\to A\subseteq B$$
4		hstles	$$⊢\left(\left(f\in \mathrm{CHStates}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\subseteq B\right)\right)\to \left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)$$
5	2 4	mpanr1	$$⊢\left(\left(f\in \mathrm{CHStates}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge A\subseteq B\right)\to \left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)$$
6	1 5	mpanl2	$$⊢\left(f\in \mathrm{CHStates}\wedge A\subseteq B\right)\to \left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)$$
7	6	expcom	$$⊢A\subseteq B\to \left(f\in \mathrm{CHStates}\to \left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)\right)$$
8	7	ralrimiv	$$⊢A\subseteq B\to \forall f\in \mathrm{CHStates}\left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)$$
9	3 8	impbii	$$⊢\forall f\in \mathrm{CHStates}\left({norm}_{ℎ}\left(f\left(A\right)\right)=1\to {norm}_{ℎ}\left(f\left(B\right)\right)=1\right)\leftrightarrow A\subseteq B$$