Theorem cdleme28a

Description: Lemma for cdleme25b . TODO: FIX COMMENT. (Contributed by NM, 4-Feb-2013)

	Ref	Expression
Hypotheses	cdleme26.b	$$⊢B={\mathrm{Base}}_K$$
	cdleme26.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdleme26.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdleme26.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdleme26.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdleme26.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdleme27.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
	cdleme27.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)$$
	cdleme27.z	$$⊢Z=\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme27.n	$$⊢N=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Z\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme27.d	$$⊢D=\left(\iota u\in B|\forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=N\right)\right)$$
	cdleme27.c	$$⊢C=if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),D,F\right)$$
	cdleme27.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)$$
	cdleme27.o	$$⊢O=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Z\underset{\dot{}}{\vee }\left(\left(t\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme27.e	$$⊢E=\left(\iota u\in B|\forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=O\right)\right)$$
	cdleme27.y	$$⊢Y=if\left(t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),E,G\right)$$
	cdleme28a.v	$$⊢V=\left(s\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }\left(X\underset{\dot{}}{\wedge }W\right)$$
Assertion	cdleme28a	$$⊢\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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \left(C\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cdleme26.b	$$⊢B={\mathrm{Base}}_K$$
2		cdleme26.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		cdleme26.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		cdleme26.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		cdleme26.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		cdleme26.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
7		cdleme27.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
8		cdleme27.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)$$
9		cdleme27.z	$$⊢Z=\left(z\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
10		cdleme27.n	$$⊢N=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Z\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
11		cdleme27.d	$$⊢D=\left(\iota u\in B|\forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=N\right)\right)$$
12		cdleme27.c	$$⊢C=if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),D,F\right)$$
13		cdleme27.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)$$
14		cdleme27.o	$$⊢O=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(Z\underset{\dot{}}{\vee }\left(\left(t\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
15		cdleme27.e	$$⊢E=\left(\iota u\in B|\forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=O\right)\right)$$
16		cdleme27.y	$$⊢Y=if\left(t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),E,G\right)$$
17		cdleme28a.v	$$⊢V=\left(s\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }\left(X\underset{\dot{}}{\wedge }W\right)$$
18		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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to K\in \mathrm{HL}$$
19	18	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to K\in \mathrm{Lat}$$
20		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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to W\in H$$
21		simp12	$$⊢\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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
22		simp13	$$⊢\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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)$$
23		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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \left(s\in A\wedge \neg s\underset{\dot{}}{\le }W\right)$$
24		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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to P\ne Q$$
25	1 2 3 4 5 6 7 8 9 10 11 12	cdleme27cl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\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 P\ne Q\right)\right)\to C\in B$$
26	18 20 21 22 23 24 25	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to C\in B$$
27		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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)$$
28	1 2 3 4 5 6 7 13 9 14 15 16	cdleme27cl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\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(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge P\ne Q\right)\right)\to Y\in B$$
29	18 20 21 22 27 24 28	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to Y\in B$$
30		simp11	$$⊢\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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
31	30 23 27	3jca	$$⊢\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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \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 \neg t\underset{\dot{}}{\le }W\right)\right)$$
32		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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)$$
33		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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to s\ne t$$
34		simp32l	$$⊢\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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X$$
35		simp32r	$$⊢\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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X$$
36	33 34 35	3jca	$$⊢\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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \left(s\ne t\wedge s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)$$
37	1 2 3 4 5 6 17	cdleme23b	$$⊢\left(\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 \neg t\underset{\dot{}}{\le }W\right)\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\wedge \left(s\ne t\wedge s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\right)\to V\in A$$
38	31 32 36 37	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to V\in A$$
39	1 5	atbase	$$⊢V\in A\to V\in B$$
40	38 39	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to V\in B$$
41	1 3	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge Y\in B\wedge V\in B\right)\to Y\underset{\dot{}}{\vee }V\in B$$
42	19 29 40 41	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to Y\underset{\dot{}}{\vee }V\in B$$
43		simp33l	$$⊢\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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to X\in B$$
44	1 6	lhpbase	$$⊢W\in H\to W\in B$$
45	20 44	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to W\in B$$
46	1 4	latmcl	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge W\in B\right)\to X\underset{\dot{}}{\wedge }W\in B$$
47	19 43 45 46	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to X\underset{\dot{}}{\wedge }W\in B$$
48	1 3	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge Y\in B\wedge X\underset{\dot{}}{\wedge }W\in B\right)\to Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\in B$$
49	19 29 47 48	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\in B$$
50	1 2 3 4 5 6 17	cdleme23c	$$⊢\left(\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 \neg t\underset{\dot{}}{\le }W\right)\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\wedge \left(s\ne t\wedge s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\right)\to s\underset{\dot{}}{\le }\left(t\underset{\dot{}}{\vee }V\right)$$
51	31 32 36 50	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to s\underset{\dot{}}{\le }\left(t\underset{\dot{}}{\vee }V\right)$$
52	33 51	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \left(s\ne t\wedge s\underset{\dot{}}{\le }\left(t\underset{\dot{}}{\vee }V\right)\right)$$
53	1 2 3 4 5 6 17	cdleme23a	$$⊢\left(\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 \neg t\underset{\dot{}}{\le }W\right)\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\wedge \left(s\ne t\wedge s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\right)\to V\underset{\dot{}}{\le }W$$
54	31 32 36 53	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to V\underset{\dot{}}{\le }W$$
55	38 54	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
56	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	cdleme27a	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge P\ne Q\wedge \left(s\in A\wedge \neg s\underset{\dot{}}{\le }W\right)\right)\wedge \left(\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)\wedge \left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(s\ne t\wedge s\underset{\dot{}}{\le }\left(t\underset{\dot{}}{\vee }V\right)\right)\wedge \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\right)\to C\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{\vee }V\right)$$
57	30 24 23 21 22 27 52 55 56	syl332anc	$$⊢\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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to C\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{\vee }V\right)$$
58		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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to s\in A$$
59		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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to t\in A$$
60	1 3 5	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge s\in A\wedge t\in A\right)\to s\underset{\dot{}}{\vee }t\in B$$
61	18 58 59 60	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to s\underset{\dot{}}{\vee }t\in B$$
62	1 2 4	latmle2	$$⊢\left(K\in \mathrm{Lat}\wedge s\underset{\dot{}}{\vee }t\in B\wedge X\underset{\dot{}}{\wedge }W\in B\right)\to \left(\left(s\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }\left(X\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\wedge }W\right)$$
63	19 61 47 62	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \left(\left(s\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }\left(X\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\wedge }W\right)$$
64	17 63	eqbrtrid	$$⊢\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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to V\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\wedge }W\right)$$
65	1 2 3	latjlej2	$$⊢\left(K\in \mathrm{Lat}\wedge \left(V\in B\wedge X\underset{\dot{}}{\wedge }W\in B\wedge Y\in B\right)\right)\to \left(V\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\wedge }W\right)\to \left(Y\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\right)$$
66	19 40 47 29 65	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \left(V\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\wedge }W\right)\to \left(Y\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\right)$$
67	64 66	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \left(Y\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)$$
68	1 2 19 26 42 49 57 67	lattrd	$$⊢\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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to C\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)$$
69	1 2 3	latlej2	$$⊢\left(K\in \mathrm{Lat}\wedge Y\in B\wedge X\underset{\dot{}}{\wedge }W\in B\right)\to \left(X\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)$$
70	19 29 47 69	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \left(X\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)$$
71	1 2 3	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(C\in B\wedge X\underset{\dot{}}{\wedge }W\in B\wedge Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\in B\right)\right)\to \left(\left(C\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\wedge \left(X\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\right)\leftrightarrow \left(C\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\right)$$
72	19 26 47 49 71	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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \left(\left(C\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\wedge \left(X\underset{\dot{}}{\wedge }W\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\right)\leftrightarrow \left(C\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\right)$$
73	68 70 72	mpbi2and	$$⊢\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(P\ne Q\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(s\ne t\wedge \left(s\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\wedge t\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)=X\right)\wedge \left(X\in B\wedge \neg X\underset{\dot{}}{\le }W\right)\right)\right)\to \left(C\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)\underset{\dot{}}{\le }\left(Y\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }W\right)\right)$$