Theorem stcltr2i

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}}$$
Assertion	stcltr2i	$$⊢\phi \to \left(S\left(A\right)=1\to A=\mathscr{H}\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		ax-1	$$⊢S\left(A\right)=1\to \left(S\left(\mathscr{H}\right)=1\to S\left(A\right)=1\right)$$
4		helch	$$⊢\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}$$
5	1 4 2	stcltr1i	$$⊢\phi \to \left(\left(S\left(\mathscr{H}\right)=1\to S\left(A\right)=1\right)\to \mathscr{H}\subseteq A\right)$$
6	3 5	syl5	$$⊢\phi \to \left(S\left(A\right)=1\to \mathscr{H}\subseteq A\right)$$
7	2	chssii	$$⊢A\subseteq \mathscr{H}$$
8		eqss	$$⊢A=\mathscr{H}\leftrightarrow \left(A\subseteq \mathscr{H}\wedge \mathscr{H}\subseteq A\right)$$
9	7 8	mpbiran	$$⊢A=\mathscr{H}\leftrightarrow \mathscr{H}\subseteq A$$
10	6 9	imbitrrdi	$$⊢\phi \to \left(S\left(A\right)=1\to A=\mathscr{H}\right)$$