Theorem 3dim2

Description: Construct 2 new layers on top of 2 given atoms. (Contributed by NM, 27-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	3dim2	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to \exists r\in A\exists s\in A\left(\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	1 2 3	3dim1	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\right)\to \exists u\in A\exists v\in A\exists w\in A\left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)$$
5	4	3adant2	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to \exists u\in A\exists v\in A\exists w\in A\left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)$$
6		simpl21	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P=Q\right)\to u\in A$$
7		simpl22	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P=Q\right)\to v\in A$$
8		simp31	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to Q\ne u$$
9	8	necomd	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to u\ne Q$$
10	9	adantr	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P=Q\right)\to u\ne Q$$
11		oveq1	$$⊢P=Q\to P\underset{\dot{}}{\vee }Q=Q\underset{\dot{}}{\vee }Q$$
12		simp11	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to K\in \mathrm{HL}$$
13		simp13	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to Q\in A$$
14	1 3	hlatjidm	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\right)\to Q\underset{\dot{}}{\vee }Q=Q$$
15	12 13 14	syl2anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to Q\underset{\dot{}}{\vee }Q=Q$$
16	11 15	sylan9eqr	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P=Q\right)\to P\underset{\dot{}}{\vee }Q=Q$$
17	16	breq2d	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P=Q\right)\to \left(u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow u\underset{\dot{}}{\le }Q\right)$$
18	17	notbid	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P=Q\right)\to \left(\neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow \neg u\underset{\dot{}}{\le }Q\right)$$
19		hlatl	$$⊢K\in \mathrm{HL}\to K\in \mathrm{AtLat}$$
20	12 19	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to K\in \mathrm{AtLat}$$
21		simp21	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to u\in A$$
22	2 3	atncmp	$$⊢\left(K\in \mathrm{AtLat}\wedge u\in A\wedge Q\in A\right)\to \left(\neg u\underset{\dot{}}{\le }Q\leftrightarrow u\ne Q\right)$$
23	20 21 13 22	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(\neg u\underset{\dot{}}{\le }Q\leftrightarrow u\ne Q\right)$$
24	23	adantr	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P=Q\right)\to \left(\neg u\underset{\dot{}}{\le }Q\leftrightarrow u\ne Q\right)$$
25	18 24	bitrd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P=Q\right)\to \left(\neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow u\ne Q\right)$$
26	10 25	mpbird	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P=Q\right)\to \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
27		simpl32	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P=Q\right)\to \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)$$
28	16	oveq1d	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P=Q\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u=Q\underset{\dot{}}{\vee }u$$
29	28	breq2d	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P=Q\right)\to \left(v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\leftrightarrow v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)$$
30	27 29	mtbird	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P=Q\right)\to \neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)$$
31		breq1	$$⊢r=u\to \left(r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
32	31	notbid	$$⊢r=u\to \left(\neg r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
33		oveq2	$$⊢r=u\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }r=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u$$
34	33	breq2d	$$⊢r=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 }Q\right)\underset{\dot{}}{\vee }u\right)\right)$$
35	34	notbid	$$⊢r=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 }Q\right)\underset{\dot{}}{\vee }u\right)\right)$$
36	32 35	anbi12d	$$⊢r=u\to \left(\left(\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(\neg u\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 }u\right)\right)\right)$$
37		breq1	$$⊢s=v\to \left(s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\leftrightarrow v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)$$
38	37	notbid	$$⊢s=v\to \left(\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\leftrightarrow \neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)$$
39	38	anbi2d	$$⊢s=v\to \left(\left(\neg u\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 }u\right)\right)\leftrightarrow \left(\neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)\right)$$
40	36 39	rspc2ev	$$⊢\left(u\in A\wedge v\in A\wedge \left(\neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)\right)\to \exists r\in A\exists s\in A\left(\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)$$
41	6 7 26 30 40	syl112anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P=Q\right)\to \exists r\in A\exists s\in A\left(\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)$$
42		simp22	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to v\in A$$
43		simp23	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to w\in A$$
44	42 43	jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(v\in A\wedge w\in A\right)$$
45	44	ad2antrr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\to \left(v\in A\wedge w\in A\right)$$
46		simpll1	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\to \left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)$$
47		simp32	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)$$
48		simp33	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)$$
49	21 47 48	3jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(u\in A\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)$$
50	49	ad2antrr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\to \left(u\in A\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)$$
51		simplr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\to P\ne Q$$
52		simpr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\to P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)$$
53	1 2 3	3dimlem2	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\wedge \left(P\ne Q\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\right)\to \left(P\ne Q\wedge \neg v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }v\right)\right)$$
54	46 50 51 52 53	syl112anc	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\to \left(P\ne Q\wedge \neg v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }v\right)\right)$$
55		3simpc	$$⊢\left(P\ne Q\wedge \neg v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }v\right)\right)\to \left(\neg v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }v\right)\right)$$
56	54 55	syl	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\to \left(\neg v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }v\right)\right)$$
57		breq1	$$⊢r=v\to \left(r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
58	57	notbid	$$⊢r=v\to \left(\neg r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow \neg v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
59		oveq2	$$⊢r=v\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }r=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }v$$
60	59	breq2d	$$⊢r=v\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 }Q\right)\underset{\dot{}}{\vee }v\right)\right)$$
61	60	notbid	$$⊢r=v\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 }Q\right)\underset{\dot{}}{\vee }v\right)\right)$$
62	58 61	anbi12d	$$⊢r=v\to \left(\left(\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(\neg v\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 }v\right)\right)\right)$$
63		breq1	$$⊢s=w\to \left(s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }v\right)\leftrightarrow w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }v\right)\right)$$
64	63	notbid	$$⊢s=w\to \left(\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }v\right)\leftrightarrow \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }v\right)\right)$$
65	64	anbi2d	$$⊢s=w\to \left(\left(\neg v\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 }v\right)\right)\leftrightarrow \left(\neg v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }v\right)\right)\right)$$
66	62 65	rspc2ev	$$⊢\left(v\in A\wedge w\in A\wedge \left(\neg v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \exists r\in A\exists s\in A\left(\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)$$
67	66	3expa	$$⊢\left(\left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \exists r\in A\exists s\in A\left(\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)$$
68	45 56 67	syl2anc	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\to \exists r\in A\exists s\in A\left(\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)$$
69	21 43	jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(u\in A\wedge w\in A\right)$$
70	69	ad3antrrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \left(u\in A\wedge w\in A\right)$$
71		simp1	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)$$
72	21 42	jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(u\in A\wedge v\in A\right)$$
73	8 48	jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(Q\ne u\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)$$
74	71 72 73	3jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\right)\wedge \left(Q\ne u\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)$$
75	74	ad3antrrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\right)\wedge \left(Q\ne u\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)$$
76		simpllr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to P\ne Q$$
77		simplr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)$$
78		simpr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)$$
79	1 2 3	3dimlem3	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\right)\wedge \left(Q\ne u\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge \left(P\ne Q\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(P\ne Q\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)$$
80	75 76 77 78 79	syl13anc	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \left(P\ne Q\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)$$
81		3simpc	$$⊢\left(P\ne Q\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)\to \left(\neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)$$
82	80 81	syl	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \left(\neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)$$
83		breq1	$$⊢s=w\to \left(s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\leftrightarrow w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)$$
84	83	notbid	$$⊢s=w\to \left(\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\leftrightarrow \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)$$
85	84	anbi2d	$$⊢s=w\to \left(\left(\neg u\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 }u\right)\right)\leftrightarrow \left(\neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)\right)$$
86	36 85	rspc2ev	$$⊢\left(u\in A\wedge w\in A\wedge \left(\neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)\right)\to \exists r\in A\exists s\in A\left(\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)$$
87	86	3expa	$$⊢\left(\left(u\in A\wedge w\in A\right)\wedge \left(\neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)\right)\to \exists r\in A\exists s\in A\left(\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)$$
88	70 82 87	syl2anc	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \exists r\in A\exists s\in A\left(\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)$$
89	72	ad3antrrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \left(u\in A\wedge v\in A\right)$$
90	8 47	jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)$$
91	71 72 90	3jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\right)$$
92	91	ad3antrrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\right)$$
93		simpllr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to P\ne Q$$
94		simplr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)$$
95		simpr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)$$
96	1 2 3	3dimlem4	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\right)\wedge \left(P\ne Q\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \left(P\ne Q\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)$$
97	92 93 94 95 96	syl121anc	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \left(P\ne Q\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)$$
98		3simpc	$$⊢\left(P\ne Q\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)\to \left(\neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)$$
99	97 98	syl	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \left(\neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)$$
100	40	3expa	$$⊢\left(\left(u\in A\wedge v\in A\right)\wedge \left(\neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }u\right)\right)\right)\to \exists r\in A\exists s\in A\left(\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)$$
101	89 99 100	syl2anc	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \exists r\in A\exists s\in A\left(\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)$$
102	88 101	pm2.61dan	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\right)\to \exists r\in A\exists s\in A\left(\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)$$
103	68 102	pm2.61dan	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\to \exists r\in A\exists s\in A\left(\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)$$
104	41 103	pm2.61dane	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\wedge w\in A\right)\wedge \left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \exists r\in A\exists s\in A\left(\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)$$
105	104	3exp	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to \left(\left(u\in A\wedge v\in A\wedge w\in A\right)\to \left(\left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \exists r\in A\exists s\in A\left(\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)\right)\right)$$
106	105	3expd	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to \left(u\in A\to \left(v\in A\to \left(w\in A\to \left(\left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \exists r\in A\exists s\in A\left(\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)\right)\right)\right)\right)$$
107	106	imp32	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\right)\right)\to \left(w\in A\to \left(\left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \exists r\in A\exists s\in A\left(\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)\right)\right)$$
108	107	rexlimdv	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(u\in A\wedge v\in A\right)\right)\to \left(\exists w\in A\left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \exists r\in A\exists s\in A\left(\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)\right)$$
109	108	rexlimdvva	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to \left(\exists u\in A\exists v\in A\exists w\in A\left(Q\ne u\wedge \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }u\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\vee }v\right)\right)\to \exists r\in A\exists s\in A\left(\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)\right)$$
110	5 109	mpd	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to \exists r\in A\exists s\in A\left(\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)$$