Theorem stcltr2i

Description: Property of a strong classical state. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	stcltr1.1	|- ( ph <-> ( S e. States /\ A. x e. CH A. y e. CH ( ( ( S ` x ) = 1 -> ( S ` y ) = 1 ) -> x C_ y ) ) )
	stcltr1.2	|- A e. CH
Assertion	stcltr2i	|- ( ph -> ( ( S ` A ) = 1 -> A = ~H ) )

Proof

Step	Hyp	Ref	Expression
1		stcltr1.1	|- ( ph <-> ( S e. States /\ A. x e. CH A. y e. CH ( ( ( S ` x ) = 1 -> ( S ` y ) = 1 ) -> x C_ y ) ) )
2		stcltr1.2	|- A e. CH
3		ax-1	|- ( ( S ` A ) = 1 -> ( ( S ` ~H ) = 1 -> ( S ` A ) = 1 ) )
4		helch	|- ~H e. CH
5	1 4 2	stcltr1i	|- ( ph -> ( ( ( S ` ~H ) = 1 -> ( S ` A ) = 1 ) -> ~H C_ A ) )
6	3 5	syl5	|- ( ph -> ( ( S ` A ) = 1 -> ~H C_ A ) )
7	2	chssii	|- A C_ ~H
8		eqss	|- ( A = ~H <-> ( A C_ ~H /\ ~H C_ A ) )
9	7 8	mpbiran	|- ( A = ~H <-> ~H C_ A )
10	6 9	syl6ibr	|- ( ph -> ( ( S ` A ) = 1 -> A = ~H ) )