Metamath Proof Explorer


Theorem stm1i

Description: State of component of unit meet. (Contributed by NM, 11-Nov-1999) (New usage is discouraged.)

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

Proof

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