Theorem stji1i

Description: Join of components of Sasaki arrow ->1. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	stle.1	|- A e. CH
	stle.2	|- B e. CH
Assertion	stji1i	|- ( S e. States -> ( S ` ( ( _|_ ` A ) vH ( A i^i B ) ) ) = ( ( S ` ( _|_ ` A ) ) + ( S ` ( A i^i B ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		stle.1	|- A e. CH
2		stle.2	|- B e. CH
3	1	choccli	|- ( _|_ ` A ) e. CH
4	1 2	chincli	|- ( A i^i B ) e. CH
5	3 4	pm3.2i	|- ( ( _|_ ` A ) e. CH /\ ( A i^i B ) e. CH )
6		inss1	|- ( A i^i B ) C_ A
7	4 1	chsscon3i	|- ( ( A i^i B ) C_ A <-> ( _|_ ` A ) C_ ( _|_ ` ( A i^i B ) ) )
8	6 7	mpbi	|- ( _|_ ` A ) C_ ( _|_ ` ( A i^i B ) )
9		stj	|- ( S e. States -> ( ( ( ( _|_ ` A ) e. CH /\ ( A i^i B ) e. CH ) /\ ( _|_ ` A ) C_ ( _|_ ` ( A i^i B ) ) ) -> ( S ` ( ( _|_ ` A ) vH ( A i^i B ) ) ) = ( ( S ` ( _|_ ` A ) ) + ( S ` ( A i^i B ) ) ) ) )
10	5 8 9	mp2ani	|- ( S e. States -> ( S ` ( ( _|_ ` A ) vH ( A i^i B ) ) ) = ( ( S ` ( _|_ ` A ) ) + ( S ` ( A i^i B ) ) ) )