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