Theorem 3dim3

Description: Construct a new layer on top of 3 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	3dim3	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\to \exists s\in A\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\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	3dim2	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\wedge R\in A\right)\to \exists v\in A\exists w\in A\left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)$$
5	4	3adant3r1	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\to \exists v\in A\exists w\in A\left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)$$
6		simpl2l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P=Q\right)\to v\in A$$
7		simp3l	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)$$
8		simp1l	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to K\in \mathrm{HL}$$
9		simp1r2	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to Q\in A$$
10	1 3	hlatjidm	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\right)\to Q\underset{\dot{}}{\vee }Q=Q$$
11	8 9 10	syl2anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to Q\underset{\dot{}}{\vee }Q=Q$$
12	11	oveq1d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(Q\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R=Q\underset{\dot{}}{\vee }R$$
13	12	breq2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(v\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\leftrightarrow v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)$$
14	7 13	mtbird	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \neg v\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
15		oveq1	$$⊢P=Q\to P\underset{\dot{}}{\vee }Q=Q\underset{\dot{}}{\vee }Q$$
16	15	oveq1d	$$⊢P=Q\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R=\left(Q\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
17	16	breq2d	$$⊢P=Q\to \left(v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\leftrightarrow v\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)$$
18	17	notbid	$$⊢P=Q\to \left(\neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\leftrightarrow \neg v\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)$$
19	18	biimparc	$$⊢\left(\neg v\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\wedge P=Q\right)\to \neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
20	14 19	sylan	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\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 }R\right)$$
21		breq1	$$⊢s=v\to \left(s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\leftrightarrow v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)$$
22	21	notbid	$$⊢s=v\to \left(\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\leftrightarrow \neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)$$
23	22	rspcev	$$⊢\left(v\in A\wedge \neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \exists s\in A\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
24	6 20 23	syl2anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P=Q\right)\to \exists s\in A\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
25		simp2l	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to v\in A$$
26	25	ad2antrr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\to v\in A$$
27	7	ad2antrr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\to \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)$$
28	1 3	hlatjass	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R=P\underset{\dot{}}{\vee }\left(Q\underset{\dot{}}{\vee }R\right)$$
29	28	3ad2ant1	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R=P\underset{\dot{}}{\vee }\left(Q\underset{\dot{}}{\vee }R\right)$$
30	29	ad2antrr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R=P\underset{\dot{}}{\vee }\left(Q\underset{\dot{}}{\vee }R\right)$$
31	8	hllatd	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to K\in \mathrm{Lat}$$
32		simp1r1	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to P\in A$$
33		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
34	33 3	atbase	$$⊢P\in A\to P\in {\mathrm{Base}}_K$$
35	32 34	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to P\in {\mathrm{Base}}_K$$
36		simp1r3	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to R\in A$$
37	33 1 3	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\wedge R\in A\right)\to Q\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K$$
38	8 9 36 37	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to Q\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K$$
39	31 35 38	3jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(K\in \mathrm{Lat}\wedge P\in {\mathrm{Base}}_K\wedge Q\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\right)$$
40	39	adantr	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\to \left(K\in \mathrm{Lat}\wedge P\in {\mathrm{Base}}_K\wedge Q\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\right)$$
41	33 2 1	latleeqj1	$$⊢\left(K\in \mathrm{Lat}\wedge P\in {\mathrm{Base}}_K\wedge Q\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\right)\to \left(P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\leftrightarrow P\underset{\dot{}}{\vee }\left(Q\underset{\dot{}}{\vee }R\right)=Q\underset{\dot{}}{\vee }R\right)$$
42	40 41	syl	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\to \left(P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\leftrightarrow P\underset{\dot{}}{\vee }\left(Q\underset{\dot{}}{\vee }R\right)=Q\underset{\dot{}}{\vee }R\right)$$
43	42	biimpa	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\to P\underset{\dot{}}{\vee }\left(Q\underset{\dot{}}{\vee }R\right)=Q\underset{\dot{}}{\vee }R$$
44	30 43	eqtrd	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R=Q\underset{\dot{}}{\vee }R$$
45	44	breq2d	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\to \left(v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\leftrightarrow v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)$$
46	27 45	mtbird	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\to \neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
47	26 46 23	syl2anc	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\to \exists s\in A\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
48		simpl2r	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\to w\in A$$
49	48	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to w\in A$$
50	8 32 9	3jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)$$
51	50	ad3antrrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to \left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)$$
52	36 25	jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \left(R\in A\wedge v\in A\right)$$
53	52	ad3antrrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to \left(R\in A\wedge v\in A\right)$$
54		simpl3r	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\to \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)$$
55	54	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)$$
56		simplr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)$$
57		simpr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)$$
58	1 2 3	3dimlem3a	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge v\in A\right)\wedge \left(\neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
59	51 53 55 56 57 58	syl113anc	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
60		breq1	$$⊢s=w\to \left(s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\leftrightarrow w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)$$
61	60	notbid	$$⊢s=w\to \left(\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\leftrightarrow \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)$$
62	61	rspcev	$$⊢\left(w\in A\wedge \neg w\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \exists s\in A\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
63	49 59 62	syl2anc	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\wedge P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to \exists s\in A\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
64		simpl2l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\to v\in A$$
65	64	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to v\in A$$
66	50	ad3antrrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to \left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)$$
67	52	ad3antrrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to \left(R\in A\wedge v\in A\right)$$
68		simpl3l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\to \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)$$
69	68	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to \neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)$$
70		simplr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)$$
71		simpr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)$$
72	1 2 3	3dimlem4a	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge v\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
73	66 67 69 70 71 72	syl113anc	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to \neg v\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
74	65 73 23	syl2anc	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\wedge \neg P\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to \exists s\in A\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
75	63 74	pm2.61dan	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\wedge \neg P\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\to \exists s\in A\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
76	47 75	pm2.61dan	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\wedge P\ne Q\right)\to \exists s\in A\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
77	24 76	pm2.61dane	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\wedge \left(v\in A\wedge w\in A\right)\wedge \left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\right)\to \exists s\in A\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
78	77	3exp	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\to \left(\left(v\in A\wedge w\in A\right)\to \left(\left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to \exists s\in A\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)$$
79	78	rexlimdvv	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\to \left(\exists v\in A\exists w\in A\left(\neg v\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg w\underset{\dot{}}{\le }\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }v\right)\right)\to \exists s\in A\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)$$
80	5 79	mpd	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\to \exists s\in A\neg s\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$