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 e. CH -> ( 0H C. A <-> A =/= 0H ) )

Proof

Step	Hyp	Ref	Expression
1		df-pss	|- ( 0H C. A <-> ( 0H C_ A /\ 0H =/= A ) )
2		necom	|- ( 0H =/= A <-> A =/= 0H )
3		ch0le	|- ( A e. CH -> 0H C_ A )
4	3	biantrurd	|- ( A e. CH -> ( 0H =/= A <-> ( 0H C_ A /\ 0H =/= A ) ) )
5	2 4	bitr3id	|- ( A e. CH -> ( A =/= 0H <-> ( 0H C_ A /\ 0H =/= A ) ) )
6	1 5	bitr4id	|- ( A e. CH -> ( 0H C. A <-> A =/= 0H ) )