Metamath Proof Explorer

Theorem atcvat2

Description: A Hilbert lattice element covered by the join of two distinct atoms is an atom. (Contributed by NM, 29-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atcvat2 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms ∧ C ∈ HAtoms → ¬ B = C ∧ A ⋖ ℋ B ∨ ℋ C → A ∈ HAtoms

Proof

Step Hyp Ref Expression
1 breq1 ⊢ A = if A ∈ C ℋ A 0 ℋ → A ⋖ ℋ B ∨ ℋ C ↔ if A ∈ C ℋ A 0 ℋ ⋖ ℋ B ∨ ℋ C
2 1 anbi2d ⊢ A = if A ∈ C ℋ A 0 ℋ → ¬ B = C ∧ A ⋖ ℋ B ∨ ℋ C ↔ ¬ B = C ∧ if A ∈ C ℋ A 0 ℋ ⋖ ℋ B ∨ ℋ C
3 eleq1 ⊢ A = if A ∈ C ℋ A 0 ℋ → A ∈ HAtoms ↔ if A ∈ C ℋ A 0 ℋ ∈ HAtoms
4 2 3 imbi12d ⊢ A = if A ∈ C ℋ A 0 ℋ → ¬ B = C ∧ A ⋖ ℋ B ∨ ℋ C → A ∈ HAtoms ↔ ¬ B = C ∧ if A ∈ C ℋ A 0 ℋ ⋖ ℋ B ∨ ℋ C → if A ∈ C ℋ A 0 ℋ ∈ HAtoms
5 4 imbi2d ⊢ A = if A ∈ C ℋ A 0 ℋ → B ∈ HAtoms ∧ C ∈ HAtoms → ¬ B = C ∧ A ⋖ ℋ B ∨ ℋ C → A ∈ HAtoms ↔ B ∈ HAtoms ∧ C ∈ HAtoms → ¬ B = C ∧ if A ∈ C ℋ A 0 ℋ ⋖ ℋ B ∨ ℋ C → if A ∈ C ℋ A 0 ℋ ∈ HAtoms
6 h0elch ⊢ 0 ℋ ∈ C ℋ
7 6 elimel ⊢ if A ∈ C ℋ A 0 ℋ ∈ C ℋ
8 7 atcvat2i ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → ¬ B = C ∧ if A ∈ C ℋ A 0 ℋ ⋖ ℋ B ∨ ℋ C → if A ∈ C ℋ A 0 ℋ ∈ HAtoms
9 5 8 dedth ⊢ A ∈ C ℋ → B ∈ HAtoms ∧ C ∈ HAtoms → ¬ B = C ∧ A ⋖ ℋ B ∨ ℋ C → A ∈ HAtoms
10 9 3impib ⊢ A ∈ C ℋ ∧ B ∈ HAtoms ∧ C ∈ HAtoms → ¬ B = C ∧ A ⋖ ℋ B ∨ ℋ C → A ∈ HAtoms