Metamath Proof Explorer

Theorem atcvat2i

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

Ref Expression
Hypothesis atoml.1 ⊢ A ∈ C ℋ
Assertion atcvat2i ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → ¬ B = C ∧ A ⋖ ℋ B ∨ ℋ C → A ∈ HAtoms

Proof

Step Hyp Ref Expression
1 atoml.1 ⊢ A ∈ C ℋ
2 atcv1 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms ∧ C ∈ HAtoms ∧ A ⋖ ℋ B ∨ ℋ C → A = 0 ℋ ↔ B = C
3 1 2 mp3anl1 ⊢ B ∈ HAtoms ∧ C ∈ HAtoms ∧ A ⋖ ℋ B ∨ ℋ C → A = 0 ℋ ↔ B = C
4 3 necon3abid ⊢ B ∈ HAtoms ∧ C ∈ HAtoms ∧ A ⋖ ℋ B ∨ ℋ C → A ≠ 0 ℋ ↔ ¬ B = C
5 atelch ⊢ B ∈ HAtoms → B ∈ C ℋ
6 atelch ⊢ C ∈ HAtoms → C ∈ C ℋ
7 chjcl ⊢ B ∈ C ℋ ∧ C ∈ C ℋ → B ∨ ℋ C ∈ C ℋ
8 5 6 7 syl2an ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → B ∨ ℋ C ∈ C ℋ
9 cvpss ⊢ A ∈ C ℋ ∧ B ∨ ℋ C ∈ C ℋ → A ⋖ ℋ B ∨ ℋ C → A ⊂ B ∨ ℋ C
10 1 8 9 sylancr ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → A ⋖ ℋ B ∨ ℋ C → A ⊂ B ∨ ℋ C
11 1 atcvati ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → A ≠ 0 ℋ ∧ A ⊂ B ∨ ℋ C → A ∈ HAtoms
12 11 expcomd ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → A ⊂ B ∨ ℋ C → A ≠ 0 ℋ → A ∈ HAtoms
13 10 12 syld ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → A ⋖ ℋ B ∨ ℋ C → A ≠ 0 ℋ → A ∈ HAtoms
14 13 imp ⊢ B ∈ HAtoms ∧ C ∈ HAtoms ∧ A ⋖ ℋ B ∨ ℋ C → A ≠ 0 ℋ → A ∈ HAtoms
15 4 14 sylbird ⊢ B ∈ HAtoms ∧ C ∈ HAtoms ∧ A ⋖ ℋ B ∨ ℋ C → ¬ B = C → A ∈ HAtoms
16 15 ex ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → A ⋖ ℋ B ∨ ℋ C → ¬ B = C → A ∈ HAtoms
17 16 com23 ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → ¬ B = C → A ⋖ ℋ B ∨ ℋ C → A ∈ HAtoms
18 17 impd ⊢ B ∈ HAtoms ∧ C ∈ HAtoms → ¬ B = C ∧ A ⋖ ℋ B ∨ ℋ C → A ∈ HAtoms