Theorem chpssati

Description: Two Hilbert lattice elements in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (Contributed by NM, 10-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	chpssat.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	chpssat.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	chpssati	$$⊢A\subset B\to \exists x\in \mathrm{HAtoms}\left(x\subseteq B\wedge \neg x\subseteq A\right)$$

Proof

Step	Hyp	Ref	Expression
1		chpssat.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		chpssat.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		dfpss3	$$⊢A\subset B\leftrightarrow \left(A\subseteq B\wedge \neg B\subseteq A\right)$$
4		iman	$$⊢\left(x\subseteq B\to x\subseteq A\right)\leftrightarrow \neg \left(x\subseteq B\wedge \neg x\subseteq A\right)$$
5	4	ralbii	$$⊢\forall x\in \mathrm{HAtoms}\left(x\subseteq B\to x\subseteq A\right)\leftrightarrow \forall x\in \mathrm{HAtoms}\neg \left(x\subseteq B\wedge \neg x\subseteq A\right)$$
6		ss2rab	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq B\right\}\subseteq \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\leftrightarrow \forall x\in \mathrm{HAtoms}\left(x\subseteq B\to x\subseteq A\right)$$
7		ssrab2	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq B\right\}\subseteq \mathrm{HAtoms}$$
8		atssch	$$⊢\mathrm{HAtoms}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
9	7 8	sstri	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq B\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
10		ssrab2	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq \mathrm{HAtoms}$$
11	10 8	sstri	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
12		chsupss	$$⊢\left(\left\{x\in \mathrm{HAtoms}|x\subseteq B\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}\wedge \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left\{x\in \mathrm{HAtoms}|x\subseteq B\right\}\subseteq \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\to {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq B\right\}\right)\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)\right)$$
13	9 11 12	mp2an	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq B\right\}\subseteq \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\to {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq B\right\}\right)\subseteq {\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$
14	2	hatomistici	$$⊢B={\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq B\right\}\right)$$
15	1	hatomistici	$$⊢A={\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$
16	13 14 15	3sstr4g	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq B\right\}\subseteq \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\to B\subseteq A$$
17	6 16	sylbir	$$⊢\forall x\in \mathrm{HAtoms}\left(x\subseteq B\to x\subseteq A\right)\to B\subseteq A$$
18	5 17	sylbir	$$⊢\forall x\in \mathrm{HAtoms}\neg \left(x\subseteq B\wedge \neg x\subseteq A\right)\to B\subseteq A$$
19	18	con3i	$$⊢\neg B\subseteq A\to \neg \forall x\in \mathrm{HAtoms}\neg \left(x\subseteq B\wedge \neg x\subseteq A\right)$$
20		dfrex2	$$⊢\exists x\in \mathrm{HAtoms}\left(x\subseteq B\wedge \neg x\subseteq A\right)\leftrightarrow \neg \forall x\in \mathrm{HAtoms}\neg \left(x\subseteq B\wedge \neg x\subseteq A\right)$$
21	19 20	sylibr	$$⊢\neg B\subseteq A\to \exists x\in \mathrm{HAtoms}\left(x\subseteq B\wedge \neg x\subseteq A\right)$$
22	3 21	simplbiim	$$⊢A\subset B\to \exists x\in \mathrm{HAtoms}\left(x\subseteq B\wedge \neg x\subseteq A\right)$$