atssma

Description: The meet with an atom's superset is the atom. (Contributed by NM, 12-Jun-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	atssma	$⊢ (A \in HAtoms \land B \in C_{ℋ}) \to (A \subseteq B \leftrightarrow A \cap B \in HAtoms)$

Step	Hyp	Ref	Expression
1		df-ss	$⊢ A \subseteq B \leftrightarrow A \cap B = A$
2	1	biimpi	$⊢ A \subseteq B \to A \cap B = A$
3	2	eleq1d	$⊢ A \subseteq B \to (A \cap B \in HAtoms \leftrightarrow A \in HAtoms)$
4	3	biimprcd	$⊢ A \in HAtoms \to (A \subseteq B \to A \cap B \in HAtoms)$
5	4	adantr	$⊢ (A \in HAtoms \land B \in C_{ℋ}) \to (A \subseteq B \to A \cap B \in HAtoms)$
6		incom	$⊢ A \cap B = B \cap A$
7	6	eleq1i	$⊢ A \cap B \in HAtoms \leftrightarrow B \cap A \in HAtoms$
8		atne0	$⊢ B \cap A \in HAtoms \to B \cap A \neq 0_{ℋ}$
9	8	neneqd	$⊢ B \cap A \in HAtoms \to \neg B \cap A = 0_{ℋ}$
10	7 9	sylbi	$⊢ A \cap B \in HAtoms \to \neg B \cap A = 0_{ℋ}$
11		atnssm0	$⊢ (B \in C_{ℋ} \land A \in HAtoms) \to (\neg A \subseteq B \leftrightarrow B \cap A = 0_{ℋ})$
12	11	ancoms	$⊢ (A \in HAtoms \land B \in C_{ℋ}) \to (\neg A \subseteq B \leftrightarrow B \cap A = 0_{ℋ})$
13	12	biimpd	$⊢ (A \in HAtoms \land B \in C_{ℋ}) \to (\neg A \subseteq B \to B \cap A = 0_{ℋ})$
14	13	con1d	$⊢ (A \in HAtoms \land B \in C_{ℋ}) \to (\neg B \cap A = 0_{ℋ} \to A \subseteq B)$
15	10 14	syl5	$⊢ (A \in HAtoms \land B \in C_{ℋ}) \to (A \cap B \in HAtoms \to A \subseteq B)$
16	5 15	impbid	$⊢ (A \in HAtoms \land B \in C_{ℋ}) \to (A \subseteq B \leftrightarrow A \cap B \in HAtoms)$

Metamath Proof Explorer