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