Theorem osumcllem8N

Description: Lemma for osumclN . (Contributed by NM, 24-Mar-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	osumcllem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	osumcllem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	osumcllem.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	osumcllem.p	$$⊢\underset{\dot{}}{+}={+}_{𝑃}\left(K\right)$$
	osumcllem.o	$$⊢\underset{\dot{}}{\perp }={\perp }_{𝑃}\left(K\right)$$
	osumcllem.c	$$⊢C=\mathrm{PSubCl}\left(K\right)$$
	osumcllem.m	$$⊢M=X\underset{\dot{}}{+}\left\{p\right\}$$
	osumcllem.u	$$⊢U=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\underset{\dot{}}{+}Y\right)\right)$$
Assertion	osumcllem8N	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\subseteq A\wedge Y\subseteq A\right)\wedge \left(X\subseteq \underset{\dot{}}{\perp }\left(Y\right)\wedge X\ne \varnothing \wedge p\in A\right)\wedge \neg p\in \left(X\underset{\dot{}}{+}Y\right)\right)\to Y\cap M=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		osumcllem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		osumcllem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		osumcllem.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		osumcllem.p	$$⊢\underset{\dot{}}{+}={+}_{𝑃}\left(K\right)$$
5		osumcllem.o	$$⊢\underset{\dot{}}{\perp }={\perp }_{𝑃}\left(K\right)$$
6		osumcllem.c	$$⊢C=\mathrm{PSubCl}\left(K\right)$$
7		osumcllem.m	$$⊢M=X\underset{\dot{}}{+}\left\{p\right\}$$
8		osumcllem.u	$$⊢U=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\underset{\dot{}}{+}Y\right)\right)$$
9		n0	$$⊢Y\cap M\ne \varnothing \leftrightarrow \exists qq\in \left(Y\cap M\right)$$
10	1 2 3 4 5 6 7 8	osumcllem7N	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\subseteq A\wedge Y\subseteq A\right)\wedge \left(X\subseteq \underset{\dot{}}{\perp }\left(Y\right)\wedge X\ne \varnothing \wedge p\in A\right)\wedge q\in \left(Y\cap M\right)\right)\to p\in \left(X\underset{\dot{}}{+}Y\right)$$
11	10	3expia	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\subseteq A\wedge Y\subseteq A\right)\wedge \left(X\subseteq \underset{\dot{}}{\perp }\left(Y\right)\wedge X\ne \varnothing \wedge p\in A\right)\right)\to \left(q\in \left(Y\cap M\right)\to p\in \left(X\underset{\dot{}}{+}Y\right)\right)$$
12	11	exlimdv	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\subseteq A\wedge Y\subseteq A\right)\wedge \left(X\subseteq \underset{\dot{}}{\perp }\left(Y\right)\wedge X\ne \varnothing \wedge p\in A\right)\right)\to \left(\exists qq\in \left(Y\cap M\right)\to p\in \left(X\underset{\dot{}}{+}Y\right)\right)$$
13	9 12	syl5bi	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\subseteq A\wedge Y\subseteq A\right)\wedge \left(X\subseteq \underset{\dot{}}{\perp }\left(Y\right)\wedge X\ne \varnothing \wedge p\in A\right)\right)\to \left(Y\cap M\ne \varnothing \to p\in \left(X\underset{\dot{}}{+}Y\right)\right)$$
14	13	necon1bd	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\subseteq A\wedge Y\subseteq A\right)\wedge \left(X\subseteq \underset{\dot{}}{\perp }\left(Y\right)\wedge X\ne \varnothing \wedge p\in A\right)\right)\to \left(\neg p\in \left(X\underset{\dot{}}{+}Y\right)\to Y\cap M=\varnothing \right)$$
15	14	3impia	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\subseteq A\wedge Y\subseteq A\right)\wedge \left(X\subseteq \underset{\dot{}}{\perp }\left(Y\right)\wedge X\ne \varnothing \wedge p\in A\right)\wedge \neg p\in \left(X\underset{\dot{}}{+}Y\right)\right)\to Y\cap M=\varnothing$$