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	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐴 ≠ 0ℋ ) → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		neeq1	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝐴 ≠ 0ℋ ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ≠ 0ℋ ) )
2		sseq2	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) )
3	2	rexbidv	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 ↔ ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) )
4	1 3	imbi12d	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ( 𝐴 ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 ) ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ) ) )
5		h0elch	⊢ 0ℋ ∈ Cℋ
6	5	elimel	⊢ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∈ Cℋ
7	6	hatomici	⊢ ( if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) )
8	4 7	dedth	⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ≠ 0ℋ → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 ) )
9	8	imp	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐴 ≠ 0ℋ ) → ∃ 𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 )