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

Metamath Proof Explorer

Theorem atcvati

Description: A nonzero Hilbert lattice element less than the join of two atoms is an atom. (Contributed by NM, 28-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypothesis atoml.1 ⊢ 𝐴 ∈ Cℋ
Assertion atcvati ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) → 𝐴 ∈ HAtoms ) )

Proof

Step Hyp Ref Expression
1 atoml.1 ⊢ 𝐴 ∈ Cℋ
2 1 atcvatlem ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → ( ¬ 𝐵 ⊆ 𝐴 → 𝐴 ∈ HAtoms ) )
3 atelch ⊢ ( 𝐶 ∈ HAtoms → 𝐶 ∈ Cℋ )
4 atelch ⊢ ( 𝐵 ∈ HAtoms → 𝐵 ∈ Cℋ )
5 chjcom ⊢ ( ( 𝐶 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐶 ∨ℋ 𝐵 ) = ( 𝐵 ∨ℋ 𝐶 ) )
6 3 4 5 syl2an ⊢ ( ( 𝐶 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 𝐶 ∨ℋ 𝐵 ) = ( 𝐵 ∨ℋ 𝐶 ) )
7 6 psseq2d ⊢ ( ( 𝐶 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ⊊ ( 𝐶 ∨ℋ 𝐵 ) ↔ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) )
8 7 anbi2d ⊢ ( ( 𝐶 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( ( 𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ ( 𝐶 ∨ℋ 𝐵 ) ) ↔ ( 𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) )
9 1 atcvatlem ⊢ ( ( ( 𝐶 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) ∧ ( 𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ ( 𝐶 ∨ℋ 𝐵 ) ) ) → ( ¬ 𝐶 ⊆ 𝐴 → 𝐴 ∈ HAtoms ) )
10 9 ex ⊢ ( ( 𝐶 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( ( 𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ ( 𝐶 ∨ℋ 𝐵 ) ) → ( ¬ 𝐶 ⊆ 𝐴 → 𝐴 ∈ HAtoms ) ) )
11 8 10 sylbird ⊢ ( ( 𝐶 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ) → ( ( 𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) → ( ¬ 𝐶 ⊆ 𝐴 → 𝐴 ∈ HAtoms ) ) )
12 11 ancoms ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) → ( ¬ 𝐶 ⊆ 𝐴 → 𝐴 ∈ HAtoms ) ) )
13 12 imp ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → ( ¬ 𝐶 ⊆ 𝐴 → 𝐴 ∈ HAtoms ) )
14 chlub ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( ( 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) ↔ ( 𝐵 ∨ℋ 𝐶 ) ⊆ 𝐴 ) )
15 14 3comr ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) ↔ ( 𝐵 ∨ℋ 𝐶 ) ⊆ 𝐴 ) )
16 ssnpss ⊢ ( ( 𝐵 ∨ℋ 𝐶 ) ⊆ 𝐴 → ¬ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) )
17 15 16 biimtrdi ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ¬ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) )
18 17 con2d ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) → ¬ ( 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) ) )
19 ianor ⊢ ( ¬ ( 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) ↔ ( ¬ 𝐵 ⊆ 𝐴 ∨ ¬ 𝐶 ⊆ 𝐴 ) )
20 18 19 imbitrdi ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) → ( ¬ 𝐵 ⊆ 𝐴 ∨ ¬ 𝐶 ⊆ 𝐴 ) ) )
21 1 20 mp3an1 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) → ( ¬ 𝐵 ⊆ 𝐴 ∨ ¬ 𝐶 ⊆ 𝐴 ) ) )
22 4 3 21 syl2an ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) → ( ¬ 𝐵 ⊆ 𝐴 ∨ ¬ 𝐶 ⊆ 𝐴 ) ) )
23 22 imp ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) → ( ¬ 𝐵 ⊆ 𝐴 ∨ ¬ 𝐶 ⊆ 𝐴 ) )
24 23 adantrl ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → ( ¬ 𝐵 ⊆ 𝐴 ∨ ¬ 𝐶 ⊆ 𝐴 ) )
25 2 13 24 mpjaod ⊢ ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) ) → 𝐴 ∈ HAtoms )
26 25 ex ⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ ( 𝐵 ∨ℋ 𝐶 ) ) → 𝐴 ∈ HAtoms ) )