Theorem elat2

Description: Expanded membership relation for the set of atoms, i.e. the predicate "is an atom (of the Hilbert lattice)." An atom is a nonzero element of a lattice such that anything less than it is zero, i.e. it is the smallest nonzero element of the lattice. (Contributed by NM, 9-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	elat2	$$⊢A\in \mathrm{HAtoms}\leftrightarrow \left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(A\ne 0_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq A\to \left(x=A\vee x=0_{\mathscr{H}}\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ela	$$⊢A\in \mathrm{HAtoms}\leftrightarrow \left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge 0_{\mathscr{H}}{⋖}_{\mathscr{H}}A\right)$$
2		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
3		cvbr2	$$⊢\left(0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(0_{\mathscr{H}}{⋖}_{\mathscr{H}}A\leftrightarrow \left(0_{\mathscr{H}}\subset A\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(0_{\mathscr{H}}\subset x\wedge x\subseteq A\right)\to x=A\right)\right)\right)$$
4	2 3	mpan	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(0_{\mathscr{H}}{⋖}_{\mathscr{H}}A\leftrightarrow \left(0_{\mathscr{H}}\subset A\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(0_{\mathscr{H}}\subset x\wedge x\subseteq A\right)\to x=A\right)\right)\right)$$
5		ch0pss	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(0_{\mathscr{H}}\subset A\leftrightarrow A\ne 0_{\mathscr{H}}\right)$$
6		ch0pss	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(0_{\mathscr{H}}\subset x\leftrightarrow x\ne 0_{\mathscr{H}}\right)$$
7	6	imbi1d	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(0_{\mathscr{H}}\subset x\to x=A\right)\leftrightarrow \left(x\ne 0_{\mathscr{H}}\to x=A\right)\right)$$
8	7	imbi2d	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(x\subseteq A\to \left(0_{\mathscr{H}}\subset x\to x=A\right)\right)\leftrightarrow \left(x\subseteq A\to \left(x\ne 0_{\mathscr{H}}\to x=A\right)\right)\right)$$
9		impexp	$$⊢\left(\left(0_{\mathscr{H}}\subset x\wedge x\subseteq A\right)\to x=A\right)\leftrightarrow \left(0_{\mathscr{H}}\subset x\to \left(x\subseteq A\to x=A\right)\right)$$
10		bi2.04	$$⊢\left(0_{\mathscr{H}}\subset x\to \left(x\subseteq A\to x=A\right)\right)\leftrightarrow \left(x\subseteq A\to \left(0_{\mathscr{H}}\subset x\to x=A\right)\right)$$
11	9 10	bitri	$$⊢\left(\left(0_{\mathscr{H}}\subset x\wedge x\subseteq A\right)\to x=A\right)\leftrightarrow \left(x\subseteq A\to \left(0_{\mathscr{H}}\subset x\to x=A\right)\right)$$
12		orcom	$$⊢\left(x=A\vee x=0_{\mathscr{H}}\right)\leftrightarrow \left(x=0_{\mathscr{H}}\vee x=A\right)$$
13		neor	$$⊢\left(x=0_{\mathscr{H}}\vee x=A\right)\leftrightarrow \left(x\ne 0_{\mathscr{H}}\to x=A\right)$$
14	12 13	bitri	$$⊢\left(x=A\vee x=0_{\mathscr{H}}\right)\leftrightarrow \left(x\ne 0_{\mathscr{H}}\to x=A\right)$$
15	14	imbi2i	$$⊢\left(x\subseteq A\to \left(x=A\vee x=0_{\mathscr{H}}\right)\right)\leftrightarrow \left(x\subseteq A\to \left(x\ne 0_{\mathscr{H}}\to x=A\right)\right)$$
16	8 11 15	3bitr4g	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(\left(0_{\mathscr{H}}\subset x\wedge x\subseteq A\right)\to x=A\right)\leftrightarrow \left(x\subseteq A\to \left(x=A\vee x=0_{\mathscr{H}}\right)\right)\right)$$
17	16	ralbiia	$$⊢\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(0_{\mathscr{H}}\subset x\wedge x\subseteq A\right)\to x=A\right)\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq A\to \left(x=A\vee x=0_{\mathscr{H}}\right)\right)$$
18	17	a1i	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(0_{\mathscr{H}}\subset x\wedge x\subseteq A\right)\to x=A\right)\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq A\to \left(x=A\vee x=0_{\mathscr{H}}\right)\right)\right)$$
19	5 18	anbi12d	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(0_{\mathscr{H}}\subset A\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(0_{\mathscr{H}}\subset x\wedge x\subseteq A\right)\to x=A\right)\right)\leftrightarrow \left(A\ne 0_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq A\to \left(x=A\vee x=0_{\mathscr{H}}\right)\right)\right)\right)$$
20	4 19	bitr2d	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(A\ne 0_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq A\to \left(x=A\vee x=0_{\mathscr{H}}\right)\right)\right)\leftrightarrow 0_{\mathscr{H}}{⋖}_{\mathscr{H}}A\right)$$
21	20	pm5.32i	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(A\ne 0_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq A\to \left(x=A\vee x=0_{\mathscr{H}}\right)\right)\right)\right)\leftrightarrow \left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge 0_{\mathscr{H}}{⋖}_{\mathscr{H}}A\right)$$
22	1 21	bitr4i	$$⊢A\in \mathrm{HAtoms}\leftrightarrow \left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(A\ne 0_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq A\to \left(x=A\vee x=0_{\mathscr{H}}\right)\right)\right)\right)$$