Metamath Proof Explorer

Theorem elat2

Description: Expanded membership relation for the set of atoms, i.e. the predicate "is an atom (of the Hilbert lattice)." An atom is a nonzero element of a lattice such that anything less than it is zero, i.e. it is the smallest nonzero element of the lattice. (Contributed by NM, 9-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion elat2 ( 𝐴 ∈ HAtoms ↔ ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ≠ 0ℋ ∧ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐴 → ( 𝑥 = 𝐴 ∨ 𝑥 = 0ℋ ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ela ⊢ ( 𝐴 ∈ HAtoms ↔ ( 𝐴 ∈ Cℋ ∧ 0ℋ ⋖ℋ 𝐴 ) )
2 h0elch ⊢ 0ℋ ∈ Cℋ
3 cvbr2 ⊢ ( ( 0ℋ ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 0ℋ ⋖ℋ 𝐴 ↔ ( 0ℋ ⊊ 𝐴 ∧ ∀ 𝑥 ∈ Cℋ ( ( 0ℋ ⊊ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 = 𝐴 ) ) ) )
4 2 3 mpan ⊢ ( 𝐴 ∈ Cℋ → ( 0ℋ ⋖ℋ 𝐴 ↔ ( 0ℋ ⊊ 𝐴 ∧ ∀ 𝑥 ∈ Cℋ ( ( 0ℋ ⊊ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 = 𝐴 ) ) ) )
5 ch0pss ⊢ ( 𝐴 ∈ Cℋ → ( 0ℋ ⊊ 𝐴 ↔ 𝐴 ≠ 0ℋ ) )
6 ch0pss ⊢ ( 𝑥 ∈ Cℋ → ( 0ℋ ⊊ 𝑥 ↔ 𝑥 ≠ 0ℋ ) )
7 6 imbi1d ⊢ ( 𝑥 ∈ Cℋ → ( ( 0ℋ ⊊ 𝑥 → 𝑥 = 𝐴 ) ↔ ( 𝑥 ≠ 0ℋ → 𝑥 = 𝐴 ) ) )
8 7 imbi2d ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝑥 ⊆ 𝐴 → ( 0ℋ ⊊ 𝑥 → 𝑥 = 𝐴 ) ) ↔ ( 𝑥 ⊆ 𝐴 → ( 𝑥 ≠ 0ℋ → 𝑥 = 𝐴 ) ) ) )
9 impexp ⊢ ( ( ( 0ℋ ⊊ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 = 𝐴 ) ↔ ( 0ℋ ⊊ 𝑥 → ( 𝑥 ⊆ 𝐴 → 𝑥 = 𝐴 ) ) )
10 bi2.04 ⊢ ( ( 0ℋ ⊊ 𝑥 → ( 𝑥 ⊆ 𝐴 → 𝑥 = 𝐴 ) ) ↔ ( 𝑥 ⊆ 𝐴 → ( 0ℋ ⊊ 𝑥 → 𝑥 = 𝐴 ) ) )
11 9 10 bitri ⊢ ( ( ( 0ℋ ⊊ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 = 𝐴 ) ↔ ( 𝑥 ⊆ 𝐴 → ( 0ℋ ⊊ 𝑥 → 𝑥 = 𝐴 ) ) )
12 orcom ⊢ ( ( 𝑥 = 𝐴 ∨ 𝑥 = 0ℋ ) ↔ ( 𝑥 = 0ℋ ∨ 𝑥 = 𝐴 ) )
13 neor ⊢ ( ( 𝑥 = 0ℋ ∨ 𝑥 = 𝐴 ) ↔ ( 𝑥 ≠ 0ℋ → 𝑥 = 𝐴 ) )
14 12 13 bitri ⊢ ( ( 𝑥 = 𝐴 ∨ 𝑥 = 0ℋ ) ↔ ( 𝑥 ≠ 0ℋ → 𝑥 = 𝐴 ) )
15 14 imbi2i ⊢ ( ( 𝑥 ⊆ 𝐴 → ( 𝑥 = 𝐴 ∨ 𝑥 = 0ℋ ) ) ↔ ( 𝑥 ⊆ 𝐴 → ( 𝑥 ≠ 0ℋ → 𝑥 = 𝐴 ) ) )
16 8 11 15 3bitr4g ⊢ ( 𝑥 ∈ Cℋ → ( ( ( 0ℋ ⊊ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 = 𝐴 ) ↔ ( 𝑥 ⊆ 𝐴 → ( 𝑥 = 𝐴 ∨ 𝑥 = 0ℋ ) ) ) )
17 16 ralbiia ⊢ ( ∀ 𝑥 ∈ Cℋ ( ( 0ℋ ⊊ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 = 𝐴 ) ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐴 → ( 𝑥 = 𝐴 ∨ 𝑥 = 0ℋ ) ) )
18 17 a1i ⊢ ( 𝐴 ∈ Cℋ → ( ∀ 𝑥 ∈ Cℋ ( ( 0ℋ ⊊ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 = 𝐴 ) ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐴 → ( 𝑥 = 𝐴 ∨ 𝑥 = 0ℋ ) ) ) )
19 5 18 anbi12d ⊢ ( 𝐴 ∈ Cℋ → ( ( 0ℋ ⊊ 𝐴 ∧ ∀ 𝑥 ∈ Cℋ ( ( 0ℋ ⊊ 𝑥 ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 = 𝐴 ) ) ↔ ( 𝐴 ≠ 0ℋ ∧ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐴 → ( 𝑥 = 𝐴 ∨ 𝑥 = 0ℋ ) ) ) ) )
20 4 19 bitr2d ⊢ ( 𝐴 ∈ Cℋ → ( ( 𝐴 ≠ 0ℋ ∧ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐴 → ( 𝑥 = 𝐴 ∨ 𝑥 = 0ℋ ) ) ) ↔ 0ℋ ⋖ℋ 𝐴 ) )
21 20 pm5.32i ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ≠ 0ℋ ∧ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐴 → ( 𝑥 = 𝐴 ∨ 𝑥 = 0ℋ ) ) ) ) ↔ ( 𝐴 ∈ Cℋ ∧ 0ℋ ⋖ℋ 𝐴 ) )
22 1 21 bitr4i ⊢ ( 𝐴 ∈ HAtoms ↔ ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ≠ 0ℋ ∧ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐴 → ( 𝑥 = 𝐴 ∨ 𝑥 = 0ℋ ) ) ) ) )