Theorem hatomic

Description: A Hilbert lattice is atomic, i.e. any nonzero element is greater than or equal to some atom. Remark in Kalmbach p. 140. Also Definition 3.4-2 in MegPav2000 p. 2345 (PDF p. 8). (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	hatomic	|- ( ( A e. CH /\ A =/= 0H ) -> E. x e. HAtoms x C_ A )

Proof

Step	Hyp	Ref	Expression
1		neeq1	|- ( A = if ( A e. CH , A , 0H ) -> ( A =/= 0H <-> if ( A e. CH , A , 0H ) =/= 0H ) )
2		sseq2	|- ( A = if ( A e. CH , A , 0H ) -> ( x C_ A <-> x C_ if ( A e. CH , A , 0H ) ) )
3	2	rexbidv	|- ( A = if ( A e. CH , A , 0H ) -> ( E. x e. HAtoms x C_ A <-> E. x e. HAtoms x C_ if ( A e. CH , A , 0H ) ) )
4	1 3	imbi12d	|- ( A = if ( A e. CH , A , 0H ) -> ( ( A =/= 0H -> E. x e. HAtoms x C_ A ) <-> ( if ( A e. CH , A , 0H ) =/= 0H -> E. x e. HAtoms x C_ if ( A e. CH , A , 0H ) ) ) )
5		h0elch	|- 0H e. CH
6	5	elimel	|- if ( A e. CH , A , 0H ) e. CH
7	6	hatomici	|- ( if ( A e. CH , A , 0H ) =/= 0H -> E. x e. HAtoms x C_ if ( A e. CH , A , 0H ) )
8	4 7	dedth	|- ( A e. CH -> ( A =/= 0H -> E. x e. HAtoms x C_ A ) )
9	8	imp	|- ( ( A e. CH /\ A =/= 0H ) -> E. x e. HAtoms x C_ A )