Metamath Proof Explorer


Theorem ch0pss

Description: The zero subspace is a proper subset of nonzero Hilbert lattice elements. (Contributed by NM, 9-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion ch0pss A C 0 A A 0

Proof

Step Hyp Ref Expression
1 df-pss 0 A 0 A 0 A
2 necom 0 A A 0
3 ch0le A C 0 A
4 3 biantrurd A C 0 A 0 A 0 A
5 2 4 bitr3id A C A 0 0 A 0 A
6 1 5 bitr4id A C 0 A A 0