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