Theorem 3dim1lem5

Description: Lemma for 3dim1 . (Contributed by NM, 26-Jul-2012)

	Ref	Expression
Hypotheses	3dim0.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	3dim0.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	3dim0.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	3dim1lem5	$$⊢\left(\left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(P\ne u\wedge \neg v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \exists q\in A\exists r\in A\exists s\in A\left(P\ne q\wedge \neg r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		3dim0.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
2		3dim0.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		3dim0.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		neeq2	$$⊢q=u\to \left(P\ne q\leftrightarrow P\ne u\right)$$
5		oveq2	$$⊢q=u\to P\underset{\dot{}}{\vee }q=P\underset{\dot{}}{\vee }u$$
6	5	breq2d	$$⊢q=u\to \left(r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }q\right)\leftrightarrow r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }u\right)\right)$$
7	6	notbid	$$⊢q=u\to \left(\neg r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }q\right)\leftrightarrow \neg r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }u\right)\right)$$
8	5	oveq1d	$$⊢q=u\to \left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r=\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }r$$
9	8	breq2d	$$⊢q=u\to \left(s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\leftrightarrow s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }r\right)\right)$$
10	9	notbid	$$⊢q=u\to \left(\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\leftrightarrow \neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }r\right)\right)$$
11	4 7 10	3anbi123d	$$⊢q=u\to \left(\left(P\ne q\wedge \neg r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(P\ne u\wedge \neg r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }u\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }r\right)\right)\right)$$
12		breq1	$$⊢r=v\to \left(r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }u\right)\leftrightarrow v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }u\right)\right)$$
13	12	notbid	$$⊢r=v\to \left(\neg r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }u\right)\leftrightarrow \neg v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }u\right)\right)$$
14		oveq2	$$⊢r=v\to \left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }r=\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v$$
15	14	breq2d	$$⊢r=v\to \left(s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }r\right)\leftrightarrow s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)$$
16	15	notbid	$$⊢r=v\to \left(\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }r\right)\leftrightarrow \neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)$$
17	13 16	3anbi23d	$$⊢r=v\to \left(\left(P\ne u\wedge \neg r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }u\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(P\ne u\wedge \neg v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }u\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)$$
18		breq1	$$⊢s=w\to \left(s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\leftrightarrow w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)$$
19	18	notbid	$$⊢s=w\to \left(\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\leftrightarrow \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)$$
20	19	3anbi3d	$$⊢s=w\to \left(\left(P\ne u\wedge \neg v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }u\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\leftrightarrow \left(P\ne u\wedge \neg v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)$$
21	11 17 20	rspc3ev	$$⊢\left(\left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(P\ne u\wedge \neg v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \exists q\in A\exists r\in A\exists s\in A\left(P\ne q\wedge \neg r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$