Step |
Hyp |
Ref |
Expression |
1 |
|
stle.1 |
|- A e. CH |
2 |
|
stle.2 |
|- B e. CH |
3 |
|
inss1 |
|- ( A i^i B ) C_ A |
4 |
1 2
|
chincli |
|- ( A i^i B ) e. CH |
5 |
4 1
|
stlei |
|- ( S e. States -> ( ( A i^i B ) C_ A -> ( S ` ( A i^i B ) ) <_ ( S ` A ) ) ) |
6 |
3 5
|
mpi |
|- ( S e. States -> ( S ` ( A i^i B ) ) <_ ( S ` A ) ) |
7 |
|
breq1 |
|- ( ( S ` ( A i^i B ) ) = 1 -> ( ( S ` ( A i^i B ) ) <_ ( S ` A ) <-> 1 <_ ( S ` A ) ) ) |
8 |
6 7
|
syl5ibcom |
|- ( S e. States -> ( ( S ` ( A i^i B ) ) = 1 -> 1 <_ ( S ` A ) ) ) |
9 |
1
|
stge1i |
|- ( S e. States -> ( 1 <_ ( S ` A ) <-> ( S ` A ) = 1 ) ) |
10 |
8 9
|
sylibd |
|- ( S e. States -> ( ( S ` ( A i^i B ) ) = 1 -> ( S ` A ) = 1 ) ) |