Metamath Proof Explorer


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 ) ) ) )