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	⊢ 𝐴 ∈ Cℋ
Assertion	atcvat2i	⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( ¬ 𝐵 = 𝐶 ∧ 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) → 𝐴 ∈ HAtoms ) )

Proof

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