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 \in HAtoms \land B \in HAtoms) \to (A \neq B \leftrightarrow A \cap B = 0_{ℋ})$

Step	Hyp	Ref	Expression
1		atsseq	$⊢ (B \in HAtoms \land A \in HAtoms) \to (B \subseteq A \leftrightarrow B = A)$
2		eqcom	$⊢ B = A \leftrightarrow A = B$
3	1 2	bitrdi	$⊢ (B \in HAtoms \land A \in HAtoms) \to (B \subseteq A \leftrightarrow A = B)$
4	3	ancoms	$⊢ (A \in HAtoms \land B \in HAtoms) \to (B \subseteq A \leftrightarrow A = B)$
5	4	necon3bbid	$⊢ (A \in HAtoms \land B \in HAtoms) \to (\neg B \subseteq A \leftrightarrow A \neq B)$
6		atelch	$⊢ A \in HAtoms \to A \in C_{ℋ}$
7		atnssm0	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (\neg B \subseteq A \leftrightarrow A \cap B = 0_{ℋ})$
8	6 7	sylan	$⊢ (A \in HAtoms \land B \in HAtoms) \to (\neg B \subseteq A \leftrightarrow A \cap B = 0_{ℋ})$
9	5 8	bitr3d	$⊢ (A \in HAtoms \land B \in HAtoms) \to (A \neq B \leftrightarrow A \cap B = 0_{ℋ})$

Metamath Proof Explorer