atsseq

Description: Two atoms in a subset relationship are equal. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	atsseq	$⊢ (A \in HAtoms \land B \in HAtoms) \to (A \subseteq B \leftrightarrow A = B)$

Step	Hyp	Ref	Expression
1		atne0	$⊢ A \in HAtoms \to A \neq 0_{ℋ}$
2	1	ad2antrr	$⊢ ((A \in HAtoms \land B \in HAtoms) \land A \subseteq B) \to A \neq 0_{ℋ}$
3		atelch	$⊢ A \in HAtoms \to A \in C_{ℋ}$
4		atss	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (A \subseteq B \to (A = B \lor A = 0_{ℋ}))$
5	3 4	sylan	$⊢ (A \in HAtoms \land B \in HAtoms) \to (A \subseteq B \to (A = B \lor A = 0_{ℋ}))$
6	5	imp	$⊢ ((A \in HAtoms \land B \in HAtoms) \land A \subseteq B) \to (A = B \lor A = 0_{ℋ})$
7	6	ord	$⊢ ((A \in HAtoms \land B \in HAtoms) \land A \subseteq B) \to (\neg A = B \to A = 0_{ℋ})$
8	7	necon1ad	$⊢ ((A \in HAtoms \land B \in HAtoms) \land A \subseteq B) \to (A \neq 0_{ℋ} \to A = B)$
9	2 8	mpd	$⊢ ((A \in HAtoms \land B \in HAtoms) \land A \subseteq B) \to A = B$
10	9	ex	$⊢ (A \in HAtoms \land B \in HAtoms) \to (A \subseteq B \to A = B)$
11		eqimss	$⊢ A = B \to A \subseteq B$
12	10 11	impbid1	$⊢ (A \in HAtoms \land B \in HAtoms) \to (A \subseteq B \leftrightarrow A = B)$

Metamath Proof Explorer