Metamath Proof Explorer


Theorem chm1i

Description: Meet with lattice one in CH . (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis ch0le.1
|- A e. CH
Assertion chm1i
|- ( A i^i ~H ) = A

Proof

Step Hyp Ref Expression
1 ch0le.1
 |-  A e. CH
2 1 chssii
 |-  A C_ ~H
3 df-ss
 |-  ( A C_ ~H <-> ( A i^i ~H ) = A )
4 2 3 mpbi
 |-  ( A i^i ~H ) = A