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	3	simprbi	$$⊢A\subset B\to \neg B\subseteq A$$
5		iman	$$⊢\left(x\subseteq B\to x\subseteq A\right)\leftrightarrow \neg \left(x\subseteq B\wedge \neg x\subseteq A\right)$$
6	5	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)$$
7		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)$$
8		ssrab2	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq B\right\}\subseteq \mathrm{HAtoms}$$
9		atssch	$$⊢\mathrm{HAtoms}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
10	8 9	sstri	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq B\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
11		ssrab2	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq \mathrm{HAtoms}$$
12	11 9	sstri	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\subseteq {\mathbf{C}}_{\mathscr{H}}$$
13		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)$$
14	10 12 13	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)$$
15	2	hatomistici	$$⊢B={\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq B\right\}\right)$$
16	1	hatomistici	$$⊢A={\bigvee }_{\mathscr{H}}\left(\left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\right)$$
17	14 15 16	3sstr4g	$$⊢\left\{x\in \mathrm{HAtoms}|x\subseteq B\right\}\subseteq \left\{x\in \mathrm{HAtoms}|x\subseteq A\right\}\to B\subseteq A$$
18	7 17	sylbir	$$⊢\forall x\in \mathrm{HAtoms}\left(x\subseteq B\to x\subseteq A\right)\to B\subseteq A$$
19	6 18	sylbir	$$⊢\forall x\in \mathrm{HAtoms}\neg \left(x\subseteq B\wedge \neg x\subseteq A\right)\to B\subseteq A$$
20	19	con3i	$$⊢\neg B\subseteq A\to \neg \forall x\in \mathrm{HAtoms}\neg \left(x\subseteq B\wedge \neg x\subseteq A\right)$$
21		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)$$
22	20 21	sylibr	$$⊢\neg B\subseteq A\to \exists x\in \mathrm{HAtoms}\left(x\subseteq B\wedge \neg x\subseteq A\right)$$
23	4 22	syl	$$⊢A\subset B\to \exists x\in \mathrm{HAtoms}\left(x\subseteq B\wedge \neg x\subseteq A\right)$$