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 ) )