Theorem stcltrlem2

Description: Lemma for strong classical state theorem. (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
	stcltrlem1.3	|- B e. CH
Assertion	stcltrlem2	|- ( ph -> B C_ ( ( _|_ ` A ) vH ( A i^i B ) ) )

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		stcltrlem1.3	|- B e. CH
4	1 2 3	stcltrlem1	|- ( ph -> ( ( S ` B ) = 1 -> ( S ` ( ( _|_ ` A ) vH ( A i^i B ) ) ) = 1 ) )
5	2	choccli	|- ( _|_ ` A ) e. CH
6	2 3	chincli	|- ( A i^i B ) e. CH
7	5 6	chjcli	|- ( ( _|_ ` A ) vH ( A i^i B ) ) e. CH
8	1 3 7	stcltr1i	|- ( ph -> ( ( ( S ` B ) = 1 -> ( S ` ( ( _|_ ` A ) vH ( A i^i B ) ) ) = 1 ) -> B C_ ( ( _|_ ` A ) vH ( A i^i B ) ) ) )
9	4 8	mpd	|- ( ph -> B C_ ( ( _|_ ` A ) vH ( A i^i B ) ) )