Theorem lvoli2

Description: The join of 4 different atoms is a lattice volume. (Contributed by NM, 8-Jul-2012)

	Ref	Expression
Hypotheses	lvoli2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lvoli2.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	lvoli2.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	lvoli2.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
Assertion	lvoli2	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\in V$$

Proof

Step	Hyp	Ref	Expression
1		lvoli2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		lvoli2.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		lvoli2.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		lvoli2.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
5		simp12	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to P\in A$$
6		simp13	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to Q\in A$$
7		simp3	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to \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)$$
8		eqidd	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S$$
9		neeq1	$$⊢p=P\to \left(p\ne q\leftrightarrow P\ne q\right)$$
10		oveq1	$$⊢p=P\to p\underset{\dot{}}{\vee }q=P\underset{\dot{}}{\vee }q$$
11	10	breq2d	$$⊢p=P\to \left(R\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\leftrightarrow R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }q\right)\right)$$
12	11	notbid	$$⊢p=P\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 }q\right)\right)$$
13	10	oveq1d	$$⊢p=P\to \left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R=\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R$$
14	13	breq2d	$$⊢p=P\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 }R\right)\right)$$
15	14	notbid	$$⊢p=P\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 }R\right)\right)$$
16	9 12 15	3anbi123d	$$⊢p=P\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 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)\right)$$
17	13	oveq1d	$$⊢p=P\to \left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S$$
18	17	eqeq2d	$$⊢p=P\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\leftrightarrow \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)$$
19	16 18	anbi12d	$$⊢p=P\to \left(\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\leftrightarrow \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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\right)$$
20		neeq2	$$⊢q=Q\to \left(P\ne q\leftrightarrow P\ne Q\right)$$
21		oveq2	$$⊢q=Q\to P\underset{\dot{}}{\vee }q=P\underset{\dot{}}{\vee }Q$$
22	21	breq2d	$$⊢q=Q\to \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }q\right)\leftrightarrow R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
23	22	notbid	$$⊢q=Q\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 }Q\right)\right)$$
24	21	oveq1d	$$⊢q=Q\to \left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
25	24	breq2d	$$⊢q=Q\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 }R\right)\right)$$
26	25	notbid	$$⊢q=Q\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 }R\right)\right)$$
27	20 23 26	3anbi123d	$$⊢q=Q\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 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)\right)$$
28	24	oveq1d	$$⊢q=Q\to \left(\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S$$
29	28	eqeq2d	$$⊢q=Q\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\leftrightarrow \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)$$
30	27 29	anbi12d	$$⊢q=Q\to \left(\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\leftrightarrow \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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\right)$$
31	19 30	rspc2ev	$$⊢\left(P\in A\wedge Q\in A\wedge \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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\right)\to \exists p\in A\exists q\in A\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)$$
32	5 6 7 8 31	syl112anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to \exists p\in A\exists q\in A\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)$$
33	32	3exp	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to \left(\left(R\in A\wedge S\in A\right)\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)\to \exists p\in A\exists q\in A\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\right)\right)$$
34		simplrl	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\right)\wedge \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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\right)\to R\in A$$
35		simplrr	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\right)\wedge \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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\right)\to S\in A$$
36		simpr	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\right)\wedge \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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\right)\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)$$
37		breq1	$$⊢r=R\to \left(r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\leftrightarrow R\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)$$
38	37	notbid	$$⊢r=R\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 }q\right)\right)$$
39		oveq2	$$⊢r=R\to \left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R$$
40	39	breq2d	$$⊢r=R\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 }R\right)\right)$$
41	40	notbid	$$⊢r=R\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 }R\right)\right)$$
42	38 41	3anbi23d	$$⊢r=R\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 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)\right)$$
43	39	oveq1d	$$⊢r=R\to \left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }s$$
44	43	eqeq2d	$$⊢r=R\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\leftrightarrow \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }s\right)$$
45	42 44	anbi12d	$$⊢r=R\to \left(\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\leftrightarrow \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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }s\right)\right)$$
46		breq1	$$⊢s=S\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 }R\right)\right)$$
47	46	notbid	$$⊢s=S\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 }R\right)\right)$$
48	47	3anbi3d	$$⊢s=S\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 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)\right)$$
49		oveq2	$$⊢s=S\to \left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }s=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S$$
50	49	eqeq2d	$$⊢s=S\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }s\leftrightarrow \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)$$
51	48 50	anbi12d	$$⊢s=S\to \left(\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }s\right)\leftrightarrow \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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\right)$$
52	45 51	rspc2ev	$$⊢\left(R\in A\wedge S\in A\wedge \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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\right)\to \exists r\in A\exists s\in A\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)$$
53	34 35 36 52	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\right)\wedge \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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\right)\to \exists r\in A\exists s\in A\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)$$
54	53	ex	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\right)\to \left(\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\to \exists r\in A\exists s\in A\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$
55	54	reximdv	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\right)\to \left(\exists q\in A\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\to \exists q\in A\exists r\in A\exists s\in A\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$
56	55	reximdv	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\right)\to \left(\exists p\in A\exists q\in A\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\to \exists p\in A\exists q\in A\exists r\in A\exists s\in A\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$
57	56	ex	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to \left(\left(R\in A\wedge S\in A\right)\to \left(\exists p\in A\exists q\in A\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\to \exists p\in A\exists q\in A\exists r\in A\exists s\in A\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)\right)$$
58	33 57	syldd	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to \left(\left(R\in A\wedge S\in A\right)\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)\to \exists p\in A\exists q\in A\exists r\in A\exists s\in A\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)\right)$$
59	58	3imp	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to \exists p\in A\exists q\in A\exists r\in A\exists s\in A\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)$$
60		simp11	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to K\in \mathrm{HL}$$
61	60	hllatd	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to K\in \mathrm{Lat}$$
62		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
63	62 2 3	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
64	63	3ad2ant1	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
65		simp2l	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to R\in A$$
66	62 3	atbase	$$⊢R\in A\to R\in {\mathrm{Base}}_K$$
67	65 66	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to R\in {\mathrm{Base}}_K$$
68	62 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\wedge R\in {\mathrm{Base}}_K\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K$$
69	61 64 67 68	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K$$
70		simp2r	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to S\in A$$
71	62 3	atbase	$$⊢S\in A\to S\in {\mathrm{Base}}_K$$
72	70 71	syl	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to S\in {\mathrm{Base}}_K$$
73	62 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\wedge S\in {\mathrm{Base}}_K\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K$$
74	61 69 72 73	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K$$
75	62 1 2 3 4	islvol5	$$⊢\left(K\in \mathrm{HL}\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\in V\leftrightarrow \exists p\in A\exists q\in A\exists r\in A\exists s\in A\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$
76	60 74 75	syl2anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\in V\leftrightarrow \exists p\in A\exists q\in A\exists r\in A\exists s\in A\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)\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$
77	59 76	mpbird	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \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)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\in V$$