Theorem chrelat2i

Description: A consequence of relative atomicity. (Contributed by NM, 30-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	chrelat2i	$$⊢\neg A\subseteq B\leftrightarrow \exists x\in \mathrm{HAtoms}\left(x\subseteq A\wedge \neg x\subseteq B\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		nssinpss	$$⊢\neg A\subseteq B\leftrightarrow A\cap B\subset A$$
4	1 2	chincli	$$⊢A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
5	4 1	chrelati	$$⊢A\cap B\subset A\to \exists x\in \mathrm{HAtoms}\left(A\cap B\subset \left(A\cap B\right){\vee }_{\mathscr{H}}x\wedge \left(A\cap B\right){\vee }_{\mathscr{H}}x\subseteq A\right)$$
6		atelch	$$⊢x\in \mathrm{HAtoms}\to x\in {\mathbf{C}}_{\mathscr{H}}$$
7		chlub	$$⊢\left(A\cap B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(A\cap B\subseteq A\wedge x\subseteq A\right)\leftrightarrow \left(A\cap B\right){\vee }_{\mathscr{H}}x\subseteq A\right)$$
8	4 1 7	mp3an13	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(A\cap B\subseteq A\wedge x\subseteq A\right)\leftrightarrow \left(A\cap B\right){\vee }_{\mathscr{H}}x\subseteq A\right)$$
9		simpr	$$⊢\left(A\cap B\subseteq A\wedge x\subseteq A\right)\to x\subseteq A$$
10	8 9	syl6bir	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(A\cap B\right){\vee }_{\mathscr{H}}x\subseteq A\to x\subseteq A\right)$$
11	10	adantld	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(A\cap B\subset \left(A\cap B\right){\vee }_{\mathscr{H}}x\wedge \left(A\cap B\right){\vee }_{\mathscr{H}}x\subseteq A\right)\to x\subseteq A\right)$$
12		ssin	$$⊢\left(x\subseteq A\wedge x\subseteq B\right)\leftrightarrow x\subseteq A\cap B$$
13	12	notbii	$$⊢\neg \left(x\subseteq A\wedge x\subseteq B\right)\leftrightarrow \neg x\subseteq A\cap B$$
14		chnle	$$⊢\left(A\cap B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\neg x\subseteq A\cap B\leftrightarrow A\cap B\subset \left(A\cap B\right){\vee }_{\mathscr{H}}x\right)$$
15	4 14	mpan	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\neg x\subseteq A\cap B\leftrightarrow A\cap B\subset \left(A\cap B\right){\vee }_{\mathscr{H}}x\right)$$
16	13 15	bitrid	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\neg \left(x\subseteq A\wedge x\subseteq B\right)\leftrightarrow A\cap B\subset \left(A\cap B\right){\vee }_{\mathscr{H}}x\right)$$
17	16 8	anbi12d	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(\neg \left(x\subseteq A\wedge x\subseteq B\right)\wedge \left(A\cap B\subseteq A\wedge x\subseteq A\right)\right)\leftrightarrow \left(A\cap B\subset \left(A\cap B\right){\vee }_{\mathscr{H}}x\wedge \left(A\cap B\right){\vee }_{\mathscr{H}}x\subseteq A\right)\right)$$
18		pm3.21	$$⊢x\subseteq B\to \left(x\subseteq A\to \left(x\subseteq A\wedge x\subseteq B\right)\right)$$
19		orcom	$$⊢\left(\left(x\subseteq A\wedge x\subseteq B\right)\vee \neg x\subseteq A\right)\leftrightarrow \left(\neg x\subseteq A\vee \left(x\subseteq A\wedge x\subseteq B\right)\right)$$
20		pm4.55	$$⊢\neg \left(\neg \left(x\subseteq A\wedge x\subseteq B\right)\wedge x\subseteq A\right)\leftrightarrow \left(\left(x\subseteq A\wedge x\subseteq B\right)\vee \neg x\subseteq A\right)$$
21		imor	$$⊢\left(x\subseteq A\to \left(x\subseteq A\wedge x\subseteq B\right)\right)\leftrightarrow \left(\neg x\subseteq A\vee \left(x\subseteq A\wedge x\subseteq B\right)\right)$$
22	19 20 21	3bitr4ri	$$⊢\left(x\subseteq A\to \left(x\subseteq A\wedge x\subseteq B\right)\right)\leftrightarrow \neg \left(\neg \left(x\subseteq A\wedge x\subseteq B\right)\wedge x\subseteq A\right)$$
23	18 22	sylib	$$⊢x\subseteq B\to \neg \left(\neg \left(x\subseteq A\wedge x\subseteq B\right)\wedge x\subseteq A\right)$$
24	23	con2i	$$⊢\left(\neg \left(x\subseteq A\wedge x\subseteq B\right)\wedge x\subseteq A\right)\to \neg x\subseteq B$$
25	24	adantrl	$$⊢\left(\neg \left(x\subseteq A\wedge x\subseteq B\right)\wedge \left(A\cap B\subseteq A\wedge x\subseteq A\right)\right)\to \neg x\subseteq B$$
26	17 25	syl6bir	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(A\cap B\subset \left(A\cap B\right){\vee }_{\mathscr{H}}x\wedge \left(A\cap B\right){\vee }_{\mathscr{H}}x\subseteq A\right)\to \neg x\subseteq B\right)$$
27	11 26	jcad	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(A\cap B\subset \left(A\cap B\right){\vee }_{\mathscr{H}}x\wedge \left(A\cap B\right){\vee }_{\mathscr{H}}x\subseteq A\right)\to \left(x\subseteq A\wedge \neg x\subseteq B\right)\right)$$
28	6 27	syl	$$⊢x\in \mathrm{HAtoms}\to \left(\left(A\cap B\subset \left(A\cap B\right){\vee }_{\mathscr{H}}x\wedge \left(A\cap B\right){\vee }_{\mathscr{H}}x\subseteq A\right)\to \left(x\subseteq A\wedge \neg x\subseteq B\right)\right)$$
29	28	reximia	$$⊢\exists x\in \mathrm{HAtoms}\left(A\cap B\subset \left(A\cap B\right){\vee }_{\mathscr{H}}x\wedge \left(A\cap B\right){\vee }_{\mathscr{H}}x\subseteq A\right)\to \exists x\in \mathrm{HAtoms}\left(x\subseteq A\wedge \neg x\subseteq B\right)$$
30	5 29	syl	$$⊢A\cap B\subset A\to \exists x\in \mathrm{HAtoms}\left(x\subseteq A\wedge \neg x\subseteq B\right)$$
31	3 30	sylbi	$$⊢\neg A\subseteq B\to \exists x\in \mathrm{HAtoms}\left(x\subseteq A\wedge \neg x\subseteq B\right)$$
32		sstr2	$$⊢x\subseteq A\to \left(A\subseteq B\to x\subseteq B\right)$$
33	32	com12	$$⊢A\subseteq B\to \left(x\subseteq A\to x\subseteq B\right)$$
34	33	ralrimivw	$$⊢A\subseteq B\to \forall x\in \mathrm{HAtoms}\left(x\subseteq A\to x\subseteq B\right)$$
35		iman	$$⊢\left(x\subseteq A\to x\subseteq B\right)\leftrightarrow \neg \left(x\subseteq A\wedge \neg x\subseteq B\right)$$
36	35	ralbii	$$⊢\forall x\in \mathrm{HAtoms}\left(x\subseteq A\to x\subseteq B\right)\leftrightarrow \forall x\in \mathrm{HAtoms}\neg \left(x\subseteq A\wedge \neg x\subseteq B\right)$$
37		ralnex	$$⊢\forall x\in \mathrm{HAtoms}\neg \left(x\subseteq A\wedge \neg x\subseteq B\right)\leftrightarrow \neg \exists x\in \mathrm{HAtoms}\left(x\subseteq A\wedge \neg x\subseteq B\right)$$
38	36 37	bitri	$$⊢\forall x\in \mathrm{HAtoms}\left(x\subseteq A\to x\subseteq B\right)\leftrightarrow \neg \exists x\in \mathrm{HAtoms}\left(x\subseteq A\wedge \neg x\subseteq B\right)$$
39	34 38	sylib	$$⊢A\subseteq B\to \neg \exists x\in \mathrm{HAtoms}\left(x\subseteq A\wedge \neg x\subseteq B\right)$$
40	39	con2i	$$⊢\exists x\in \mathrm{HAtoms}\left(x\subseteq A\wedge \neg x\subseteq B\right)\to \neg A\subseteq B$$
41	31 40	impbii	$$⊢\neg A\subseteq B\leftrightarrow \exists x\in \mathrm{HAtoms}\left(x\subseteq A\wedge \neg x\subseteq B\right)$$