This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ C ℋ ∧ A ≠ 0 ℋ → ∃ x ∈ HAtoms x ⊆ A

Proof

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