Theorem cdleme21e

Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 115, 3rd line. Y , G , O , E , B , Z represent s_2, f(s), f_s(r), z_2, f(z), f_z(r) respectively. We prove that if u <_ s \/ z, then f_t(r) = f_z(r). (Contributed by NM, 29-Nov-2012)

	Ref	Expression
Hypotheses	cdleme21.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdleme21.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdleme21.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdleme21.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdleme21.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdleme21.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
	cdleme21.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)$$
	cdleme21.b	$$⊢B=\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)$$
	cdleme21.d	$$⊢D=\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W$$
	cdleme21.e	$$⊢E=\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W$$
	cdleme21d.n	$$⊢N=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }D\right)$$
	cdleme21d.z	$$⊢Z=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(B\underset{\dot{}}{\vee }E\right)$$
	cdleme21.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)$$
	cdleme21.y	$$⊢Y=\left(R\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W$$
	cdleme21.o	$$⊢O=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(G\underset{\dot{}}{\vee }Y\right)$$
Assertion	cdleme21e	$$⊢\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to O=Z$$

Proof

Step	Hyp	Ref	Expression
1		cdleme21.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		cdleme21.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		cdleme21.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		cdleme21.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		cdleme21.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		cdleme21.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
7		cdleme21.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		cdleme21.b	$$⊢B=\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)$$
9		cdleme21.d	$$⊢D=\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W$$
10		cdleme21.e	$$⊢E=\left(R\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W$$
11		cdleme21d.n	$$⊢N=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }D\right)$$
12		cdleme21d.z	$$⊢Z=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(B\underset{\dot{}}{\vee }E\right)$$
13		cdleme21.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		cdleme21.y	$$⊢Y=\left(R\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W$$
15		cdleme21.o	$$⊢O=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(G\underset{\dot{}}{\vee }Y\right)$$
16		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(\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
17		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(\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
18		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(\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)$$
19		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(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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)$$
20		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(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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)$$
21		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(\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)$$
22		simp231	$$⊢\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to P\ne Q$$
23		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(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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to Q\in A$$
24		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(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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to S\in A$$
25		simp232	$$⊢\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
26	24 22 25	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(\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to \left(S\in A\wedge P\ne Q\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
27		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(\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
28	21	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(\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to z\in A$$
29		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(\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z$$
30	1 2 3 4 5 6	cdleme21at	$$⊢\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 Q\in A\right)\wedge \left(\left(S\in A\wedge P\ne Q\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(z\in A\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\to T\ne z$$
31	16 17 23 26 27 28 29 30	syl322anc	$$⊢\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to T\ne z$$
32	22 31	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(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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to \left(P\ne Q\wedge T\ne z\right)$$
33		simp233	$$⊢\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
34		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(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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to K\in \mathrm{HL}$$
35		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(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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to P\in A$$
36	1 2 4	cdleme21b	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(S\in A\wedge P\ne Q\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(z\in A\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\to \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
37	34 35 23 24 22 25 28 29 36	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(\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
38		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(\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
39	33 37 38	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(\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to \left(\neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
40		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(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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)$$
41	22 25 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(\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to \left(P\ne Q\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)$$
42	1 2 3 4 5 6	cdleme21ct	$$⊢\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 Q\in A\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(P\ne Q\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\to \neg U\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }z\right)$$
43	16 17 23 40 20 41 21 29 42	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(\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to \neg U\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }z\right)$$
44		eqid	$$⊢\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W=\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W$$
45	1 2 3 4 5 6 13 8 14 10 44 15 12	cdleme20	$$⊢\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(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge T\ne z\right)\wedge \left(\neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg z\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 U\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }z\right)\right)\right)\to O=Z$$
46	16 17 18 19 20 21 32 39 43 45	syl333anc	$$⊢\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(P\ne Q\wedge \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)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\wedge \left(\left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)\right)\to O=Z$$