Theorem cdleme37m

Description: Part of proof of Lemma E in Crawley p. 113. Show that f(x) is one-to-one on P .\/ Q line. TODO: FIX COMMENT. (Contributed by NM, 13-Mar-2013)

	Ref	Expression
Hypotheses	cdleme37.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdleme37.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdleme37.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdleme37.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdleme37.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdleme37.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
	cdleme37.e	$$⊢E=\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)$$
	cdleme37.d	$$⊢D=\left(u\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme37.v	$$⊢V=\left(t\underset{\dot{}}{\vee }E\right)\underset{\dot{}}{\wedge }W$$
	cdleme37.x	$$⊢X=\left(u\underset{\dot{}}{\vee }D\right)\underset{\dot{}}{\wedge }W$$
	cdleme37.c	$$⊢C=\left(S\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\wedge }\left(E\underset{\dot{}}{\vee }\left(\left(t\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme37.g	$$⊢G=\left(S\underset{\dot{}}{\vee }X\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(u\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
Assertion	cdleme37m	$$⊢\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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to C=G$$

Proof

Step	Hyp	Ref	Expression
1		cdleme37.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		cdleme37.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		cdleme37.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		cdleme37.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		cdleme37.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		cdleme37.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
7		cdleme37.e	$$⊢E=\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)$$
8		cdleme37.d	$$⊢D=\left(u\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\wedge }W\right)\right)$$
9		cdleme37.v	$$⊢V=\left(t\underset{\dot{}}{\vee }E\right)\underset{\dot{}}{\wedge }W$$
10		cdleme37.x	$$⊢X=\left(u\underset{\dot{}}{\vee }D\right)\underset{\dot{}}{\wedge }W$$
11		cdleme37.c	$$⊢C=\left(S\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\wedge }\left(E\underset{\dot{}}{\vee }\left(\left(t\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
12		cdleme37.g	$$⊢G=\left(S\underset{\dot{}}{\vee }X\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(u\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
13		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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)$$
14		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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)$$
15		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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to \left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)$$
16		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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to \left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)$$
17		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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to P\ne Q$$
18		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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
19		simp33r	$$⊢\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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
20		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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
21	18 19 20	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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to \left(\neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
22		eqid	$$⊢\left(S\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W=\left(S\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W$$
23		eqid	$$⊢\left(S\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\wedge }W=\left(S\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\wedge }W$$
24		eqid	$$⊢\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(E\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(E\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)\right)$$
25		eqid	$$⊢\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\wedge }W\right)\right)$$
26	1 2 3 4 5 6 7 8 22 23 24 25	cdleme21k	$$⊢\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(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(\neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(E\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\wedge }W\right)\right)$$
27	13 14 15 16 17 21 26	syl132anc	$$⊢\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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(E\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\wedge }W\right)\right)$$
28		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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
29		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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to P\in A$$
30		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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to Q\in A$$
31	1 2 3 4 5 6	cdleme4	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge Q\in A\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to P\underset{\dot{}}{\vee }Q=S\underset{\dot{}}{\vee }U$$
32	28 29 30 14 20 31	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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to P\underset{\dot{}}{\vee }Q=S\underset{\dot{}}{\vee }U$$
33	1 2 3 4 5 6 7	cdleme2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge Q\in A\wedge \left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\right)\right)\to \left(t\underset{\dot{}}{\vee }E\right)\underset{\dot{}}{\wedge }W=U$$
34	28 29 30 15 33	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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to \left(t\underset{\dot{}}{\vee }E\right)\underset{\dot{}}{\wedge }W=U$$
35	9 34	syl5eq	$$⊢\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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to V=U$$
36	35	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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to S\underset{\dot{}}{\vee }V=S\underset{\dot{}}{\vee }U$$
37	32 36	eqtr4d	$$⊢\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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to P\underset{\dot{}}{\vee }Q=S\underset{\dot{}}{\vee }V$$
38		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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to K\in \mathrm{HL}$$
39		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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to S\in A$$
40	15	simpld	$$⊢\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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to t\in A$$
41	2 4	hlatjcom	$$⊢\left(K\in \mathrm{HL}\wedge S\in A\wedge t\in A\right)\to S\underset{\dot{}}{\vee }t=t\underset{\dot{}}{\vee }S$$
42	38 39 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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to S\underset{\dot{}}{\vee }t=t\underset{\dot{}}{\vee }S$$
43	42	oveq1d	$$⊢\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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to \left(S\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W=\left(t\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W$$
44	43	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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to E\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)=E\underset{\dot{}}{\vee }\left(\left(t\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)$$
45	37 44	oveq12d	$$⊢\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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(E\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(S\underset{\dot{}}{\vee }V\right)\underset{\dot{}}{\wedge }\left(E\underset{\dot{}}{\vee }\left(\left(t\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
46	11 45	eqtr4id	$$⊢\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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to C=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(E\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)\right)$$
47	1 2 3 4 5 6 8	cdleme2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge Q\in A\wedge \left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\right)\right)\to \left(u\underset{\dot{}}{\vee }D\right)\underset{\dot{}}{\wedge }W=U$$
48	28 29 30 16 47	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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to \left(u\underset{\dot{}}{\vee }D\right)\underset{\dot{}}{\wedge }W=U$$
49	10 48	syl5eq	$$⊢\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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to X=U$$
50	49	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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to S\underset{\dot{}}{\vee }X=S\underset{\dot{}}{\vee }U$$
51	32 50	eqtr4d	$$⊢\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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to P\underset{\dot{}}{\vee }Q=S\underset{\dot{}}{\vee }X$$
52	16	simpld	$$⊢\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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to u\in A$$
53	2 4	hlatjcom	$$⊢\left(K\in \mathrm{HL}\wedge S\in A\wedge u\in A\right)\to S\underset{\dot{}}{\vee }u=u\underset{\dot{}}{\vee }S$$
54	38 39 52 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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to S\underset{\dot{}}{\vee }u=u\underset{\dot{}}{\vee }S$$
55	54	oveq1d	$$⊢\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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to \left(S\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\wedge }W=\left(u\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W$$
56	55	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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to D\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\wedge }W\right)=D\underset{\dot{}}{\vee }\left(\left(u\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)$$
57	51 56	oveq12d	$$⊢\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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(S\underset{\dot{}}{\vee }X\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(u\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
58	12 57	eqtr4id	$$⊢\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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to G=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }u\right)\underset{\dot{}}{\wedge }W\right)\right)$$
59	27 46 58	3eqtr4d	$$⊢\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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(t\in A\wedge \neg t\underset{\dot{}}{\le }W\right)\wedge \neg t\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(\left(u\in A\wedge \neg u\underset{\dot{}}{\le }W\right)\wedge \neg u\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)\to C=G$$