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 ⊢A∈Cℋ
Assertion atcvati ⊢B∈HAtoms∧C∈HAtoms→A≠0ℋ∧A⊂B∨ℋC→A∈HAtoms

Proof

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