Theorem cdleme20j

Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 114. D , F , Y , G represent s_2, f(s), t_2, f(t). We show s_2 =/= t_2. (Contributed by NM, 18-Nov-2012)

	Ref	Expression
Hypotheses	cdleme19.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdleme19.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdleme19.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdleme19.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdleme19.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdleme19.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
	cdleme19.f	$$⊢F=\left(S\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme19.g	$$⊢G=\left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme19.d	$$⊢D=\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W$$
	cdleme19.y	$$⊢Y=\left(R\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W$$
	cdleme20.v	$$⊢V=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W$$
Assertion	cdleme20j	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to D\ne Y$$

Proof

Step	Hyp	Ref	Expression
1		cdleme19.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		cdleme19.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		cdleme19.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		cdleme19.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		cdleme19.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		cdleme19.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
7		cdleme19.f	$$⊢F=\left(S\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
8		cdleme19.g	$$⊢G=\left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)$$
9		cdleme19.d	$$⊢D=\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W$$
10		cdleme19.y	$$⊢Y=\left(R\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W$$
11		cdleme20.v	$$⊢V=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W$$
12		simp33	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
13		simp11l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to K\in \mathrm{HL}$$
14		simp22l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to S\in A$$
15		simp21l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to R\in A$$
16		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
17	16 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge R\in A\wedge S\in A\right)\to R\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K$$
18	13 15 14 17	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to R\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K$$
19		simp11r	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to W\in H$$
20	16 5	lhpbase	$$⊢W\in H\to W\in {\mathrm{Base}}_K$$
21	19 20	syl	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to W\in {\mathrm{Base}}_K$$
22	1 2 4	hlatlej2	$$⊢\left(K\in \mathrm{HL}\wedge R\in A\wedge S\in A\right)\to S\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)$$
23	13 15 14 22	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to S\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)$$
24	16 1 2 3 4	atmod2i1	$$⊢\left(K\in \mathrm{HL}\wedge \left(S\in A\wedge R\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\wedge S\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }S\right)\right)\to \left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\vee }S=\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(W\underset{\dot{}}{\vee }S\right)$$
25	13 14 18 21 23 24	syl131anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\vee }S=\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(W\underset{\dot{}}{\vee }S\right)$$
26		simp22	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)$$
27		eqid	$$⊢\mathrm{1.}\left(K\right)=\mathrm{1.}\left(K\right)$$
28	1 2 27 4 5	lhpjat1	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to W\underset{\dot{}}{\vee }S=\mathrm{1.}\left(K\right)$$
29	13 19 26 28	syl21anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to W\underset{\dot{}}{\vee }S=\mathrm{1.}\left(K\right)$$
30	29	oveq2d	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(W\underset{\dot{}}{\vee }S\right)=\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\mathrm{1.}\left(K\right)$$
31		hlol	$$⊢K\in \mathrm{HL}\to K\in \mathrm{OL}$$
32	13 31	syl	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to K\in \mathrm{OL}$$
33	16 3 27	olm11	$$⊢\left(K\in \mathrm{OL}\wedge R\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K\right)\to \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\mathrm{1.}\left(K\right)=R\underset{\dot{}}{\vee }S$$
34	32 18 33	syl2anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\mathrm{1.}\left(K\right)=R\underset{\dot{}}{\vee }S$$
35	25 30 34	3eqtrd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\vee }S=R\underset{\dot{}}{\vee }S$$
36	35	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to \left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\vee }S=R\underset{\dot{}}{\vee }S$$
37		simp1	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)$$
38		simp23	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)$$
39		simp21	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)$$
40		simp31	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(P\ne Q\wedge S\ne T\right)$$
41		simp321	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
42		simp322	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
43	41 42	jca	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
44		simp323	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
45	1 2 3 4 5 6 7 8 9 10 11	cdleme20d	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(F\underset{\dot{}}{\vee }G\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }Y\right)=V$$
46	37 26 38 39 40 43 44 45	syl133anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(F\underset{\dot{}}{\vee }G\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }Y\right)=V$$
47	13	hllatd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to K\in \mathrm{Lat}$$
48		simp12l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to P\in A$$
49		simp13l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to Q\in A$$
50	1 2 3 4 5 6 7 16	cdleme1b	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge Q\in A\wedge S\in A\right)\right)\to F\in {\mathrm{Base}}_K$$
51	13 19 48 49 14 50	syl23anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to F\in {\mathrm{Base}}_K$$
52		simp23l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to T\in A$$
53	1 2 3 4 5 6 8 16	cdleme1b	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge Q\in A\wedge T\in A\right)\right)\to G\in {\mathrm{Base}}_K$$
54	13 19 48 49 52 53	syl23anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to G\in {\mathrm{Base}}_K$$
55	16 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge F\in {\mathrm{Base}}_K\wedge G\in {\mathrm{Base}}_K\right)\to F\underset{\dot{}}{\vee }G\in {\mathrm{Base}}_K$$
56	47 51 54 55	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to F\underset{\dot{}}{\vee }G\in {\mathrm{Base}}_K$$
57		simp22r	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \neg S\underset{\dot{}}{\le }W$$
58	1 2 3 4 5 9	cdlemeda	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to D\in A$$
59	13 19 14 57 15 44 41 58	syl223anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to D\in A$$
60		simp23r	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \neg T\underset{\dot{}}{\le }W$$
61	1 2 3 4 5 10	cdlemeda	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\wedge \left(R\in A\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to Y\in A$$
62	13 19 52 60 15 44 42 61	syl223anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to Y\in A$$
63	16 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge D\in A\wedge Y\in A\right)\to D\underset{\dot{}}{\vee }Y\in {\mathrm{Base}}_K$$
64	13 59 62 63	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to D\underset{\dot{}}{\vee }Y\in {\mathrm{Base}}_K$$
65	16 1 3	latmle2	$$⊢\left(K\in \mathrm{Lat}\wedge F\underset{\dot{}}{\vee }G\in {\mathrm{Base}}_K\wedge D\underset{\dot{}}{\vee }Y\in {\mathrm{Base}}_K\right)\to \left(\left(F\underset{\dot{}}{\vee }G\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }Y\right)\right)\underset{\dot{}}{\le }\left(D\underset{\dot{}}{\vee }Y\right)$$
66	47 56 64 65	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(\left(F\underset{\dot{}}{\vee }G\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }Y\right)\right)\underset{\dot{}}{\le }\left(D\underset{\dot{}}{\vee }Y\right)$$
67	46 66	eqbrtrrd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to V\underset{\dot{}}{\le }\left(D\underset{\dot{}}{\vee }Y\right)$$
68	67	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to V\underset{\dot{}}{\le }\left(D\underset{\dot{}}{\vee }Y\right)$$
69	2 4	hlatjidm	$$⊢\left(K\in \mathrm{HL}\wedge D\in A\right)\to D\underset{\dot{}}{\vee }D=D$$
70	13 59 69	syl2anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to D\underset{\dot{}}{\vee }D=D$$
71		oveq2	$$⊢D=Y\to D\underset{\dot{}}{\vee }D=D\underset{\dot{}}{\vee }Y$$
72	70 71	sylan9req	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to D=D\underset{\dot{}}{\vee }Y$$
73	68 72	breqtrrd	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to V\underset{\dot{}}{\le }D$$
74		hlatl	$$⊢K\in \mathrm{HL}\to K\in \mathrm{AtLat}$$
75	13 74	syl	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to K\in \mathrm{AtLat}$$
76		simp31r	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to S\ne T$$
77	1 2 3 4 5 11	lhpat2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge S\ne T\right)\right)\to V\in A$$
78	13 19 14 57 52 76 77	syl222anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to V\in A$$
79	1 4	atcmp	$$⊢\left(K\in \mathrm{AtLat}\wedge V\in A\wedge D\in A\right)\to \left(V\underset{\dot{}}{\le }D\leftrightarrow V=D\right)$$
80	75 78 59 79	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(V\underset{\dot{}}{\le }D\leftrightarrow V=D\right)$$
81	80	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to \left(V\underset{\dot{}}{\le }D\leftrightarrow V=D\right)$$
82	73 81	mpbid	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to V=D$$
83	11 82	syl5reqr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to D=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W$$
84	9 83	eqtr3id	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W$$
85	16 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge S\in A\wedge T\in A\right)\to S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K$$
86	13 14 52 85	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K$$
87	16 1 3	latmle1	$$⊢\left(K\in \mathrm{Lat}\wedge S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\to \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
88	47 86 21 87	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
89	88	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
90	84 89	eqbrtrd	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to \left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
91	1 2 4	hlatlej1	$$⊢\left(K\in \mathrm{HL}\wedge S\in A\wedge T\in A\right)\to S\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
92	13 14 52 91	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to S\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
93	92	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to S\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
94	16 3	latmcl	$$⊢\left(K\in \mathrm{Lat}\wedge R\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\to \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\in {\mathrm{Base}}_K$$
95	47 18 21 94	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\in {\mathrm{Base}}_K$$
96	16 4	atbase	$$⊢S\in A\to S\in {\mathrm{Base}}_K$$
97	14 96	syl	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to S\in {\mathrm{Base}}_K$$
98	16 1 2	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\in {\mathrm{Base}}_K\wedge S\in {\mathrm{Base}}_K\wedge S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K\right)\right)\to \left(\left(\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge S\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\leftrightarrow \left(\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)$$
99	47 95 97 86 98	syl13anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(\left(\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge S\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\leftrightarrow \left(\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)$$
100	99	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to \left(\left(\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge S\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\leftrightarrow \left(\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)$$
101	90 93 100	mpbi2and	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to \left(\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
102	36 101	eqbrtrrd	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
103	16 4	atbase	$$⊢R\in A\to R\in {\mathrm{Base}}_K$$
104	15 103	syl	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to R\in {\mathrm{Base}}_K$$
105	16 1 2	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(R\in {\mathrm{Base}}_K\wedge S\in {\mathrm{Base}}_K\wedge S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K\right)\right)\to \left(\left(R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge S\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\leftrightarrow \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)$$
106	47 104 97 86 105	syl13anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(\left(R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge S\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\leftrightarrow \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)$$
107	106	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to \left(\left(R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge S\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\leftrightarrow \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)$$
108	102 107	mpbird	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to \left(R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge S\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)$$
109	108	simpld	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge D=Y\right)\to R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
110	109	ex	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(D=Y\to R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)$$
111	110	necon3bd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to \left(\neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\to D\ne Y\right)$$
112	12 111	mpd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\ne T\right)\wedge \left(\neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \neg R\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\to D\ne Y$$