This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ 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 ) )