Theorem atsseq

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

	Ref	Expression
Assertion	atsseq	$$⊢\left(A\in \mathrm{HAtoms}\wedge B\in \mathrm{HAtoms}\right)\to \left(A\subseteq B\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		atne0	$$⊢A\in \mathrm{HAtoms}\to A\ne 0_{\mathscr{H}}$$
2	1	ad2antrr	$$⊢\left(\left(A\in \mathrm{HAtoms}\wedge B\in \mathrm{HAtoms}\right)\wedge A\subseteq B\right)\to A\ne 0_{\mathscr{H}}$$
3		atelch	$$⊢A\in \mathrm{HAtoms}\to A\in {\mathbf{C}}_{\mathscr{H}}$$
4		atss	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in \mathrm{HAtoms}\right)\to \left(A\subseteq B\to \left(A=B\vee A=0_{\mathscr{H}}\right)\right)$$
5	3 4	sylan	$$⊢\left(A\in \mathrm{HAtoms}\wedge B\in \mathrm{HAtoms}\right)\to \left(A\subseteq B\to \left(A=B\vee A=0_{\mathscr{H}}\right)\right)$$
6	5	imp	$$⊢\left(\left(A\in \mathrm{HAtoms}\wedge B\in \mathrm{HAtoms}\right)\wedge A\subseteq B\right)\to \left(A=B\vee A=0_{\mathscr{H}}\right)$$
7	6	ord	$$⊢\left(\left(A\in \mathrm{HAtoms}\wedge B\in \mathrm{HAtoms}\right)\wedge A\subseteq B\right)\to \left(\neg A=B\to A=0_{\mathscr{H}}\right)$$
8	7	necon1ad	$$⊢\left(\left(A\in \mathrm{HAtoms}\wedge B\in \mathrm{HAtoms}\right)\wedge A\subseteq B\right)\to \left(A\ne 0_{\mathscr{H}}\to A=B\right)$$
9	2 8	mpd	$$⊢\left(\left(A\in \mathrm{HAtoms}\wedge B\in \mathrm{HAtoms}\right)\wedge A\subseteq B\right)\to A=B$$
10	9	ex	$$⊢\left(A\in \mathrm{HAtoms}\wedge B\in \mathrm{HAtoms}\right)\to \left(A\subseteq B\to A=B\right)$$
11		eqimss	$$⊢A=B\to A\subseteq B$$
12	10 11	impbid1	$$⊢\left(A\in \mathrm{HAtoms}\wedge B\in \mathrm{HAtoms}\right)\to \left(A\subseteq B\leftrightarrow A=B\right)$$