Metamath Proof Explorer

Theorem atnemeq0

Description: The meet of distinct atoms is the zero subspace. (Contributed by NM, 25-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atnemeq0 ⊢ A ∈ HAtoms ∧ B ∈ HAtoms → A ≠ B ↔ A ∩ B = 0 ℋ

Proof

Step Hyp Ref Expression
1 atsseq ⊢ B ∈ HAtoms ∧ A ∈ HAtoms → B ⊆ A ↔ B = A
2 eqcom ⊢ B = A ↔ A = B
3 1 2 bitrdi ⊢ B ∈ HAtoms ∧ A ∈ HAtoms → B ⊆ A ↔ A = B
4 3 ancoms ⊢ A ∈ HAtoms ∧ B ∈ HAtoms → B ⊆ A ↔ A = B
5 4 necon3bbid ⊢ A ∈ HAtoms ∧ B ∈ HAtoms → ¬ B ⊆ A ↔ A ≠ B
6 atelch ⊢ A ∈ HAtoms → A ∈ C ℋ
7 atnssm0 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → ¬ B ⊆ A ↔ A ∩ B = 0 ℋ
8 6 7 sylan ⊢ A ∈ HAtoms ∧ B ∈ HAtoms → ¬ B ⊆ A ↔ A ∩ B = 0 ℋ
9 5 8 bitr3d ⊢ A ∈ HAtoms ∧ B ∈ HAtoms → A ≠ B ↔ A ∩ B = 0 ℋ