Theorem stcltr1i

Description: Property of a strong classical state. (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}}$$
	stcltr1.3	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	stcltr1i	$$⊢\phi \to \left(\left(S\left(A\right)=1\to S\left(B\right)=1\right)\to A\subseteq 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		stcltr1.3	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
4		fveqeq2	$$⊢x=A\to \left(S\left(x\right)=1\leftrightarrow S\left(A\right)=1\right)$$
5	4	imbi1d	$$⊢x=A\to \left(\left(S\left(x\right)=1\to S\left(y\right)=1\right)\leftrightarrow \left(S\left(A\right)=1\to S\left(y\right)=1\right)\right)$$
6		sseq1	$$⊢x=A\to \left(x\subseteq y\leftrightarrow A\subseteq y\right)$$
7	5 6	imbi12d	$$⊢x=A\to \left(\left(\left(S\left(x\right)=1\to S\left(y\right)=1\right)\to x\subseteq y\right)\leftrightarrow \left(\left(S\left(A\right)=1\to S\left(y\right)=1\right)\to A\subseteq y\right)\right)$$
8		fveqeq2	$$⊢y=B\to \left(S\left(y\right)=1\leftrightarrow S\left(B\right)=1\right)$$
9	8	imbi2d	$$⊢y=B\to \left(\left(S\left(A\right)=1\to S\left(y\right)=1\right)\leftrightarrow \left(S\left(A\right)=1\to S\left(B\right)=1\right)\right)$$
10		sseq2	$$⊢y=B\to \left(A\subseteq y\leftrightarrow A\subseteq B\right)$$
11	9 10	imbi12d	$$⊢y=B\to \left(\left(\left(S\left(A\right)=1\to S\left(y\right)=1\right)\to A\subseteq y\right)\leftrightarrow \left(\left(S\left(A\right)=1\to S\left(B\right)=1\right)\to A\subseteq B\right)\right)$$
12	7 11	rspc2v	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\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)\to \left(\left(S\left(A\right)=1\to S\left(B\right)=1\right)\to A\subseteq B\right)\right)$$
13	2 3 12	mp2an	$$⊢\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)\to \left(\left(S\left(A\right)=1\to S\left(B\right)=1\right)\to A\subseteq B\right)$$
14	1 13	simplbiim	$$⊢\phi \to \left(\left(S\left(A\right)=1\to S\left(B\right)=1\right)\to A\subseteq B\right)$$