Theorem cdleme18d

Description: Part of proof of Lemma E in Crawley p. 114, 4th sentence of 4th paragraph. F , G , D , E represent f(s), f_s(r), f(t), f_t(r) respectively. We show f_s(r) = f_t(r) for all possible r (which must equal p or q in the case of exactly 3 atoms in p \/ q/0 , i.e., when -. E. r e. A ... ). (Contributed by NM, 12-Nov-2012)

	Ref	Expression
Hypotheses	cdleme18d.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdleme18d.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdleme18d.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdleme18d.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdleme18d.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdleme18d.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
	cdleme18d.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)$$
	cdleme18d.g	$$⊢G=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme18d.d	$$⊢D=\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)$$
	cdleme18d.e	$$⊢E=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)$$
Assertion	cdleme18d	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to G=E$$

Proof

Step	Hyp	Ref	Expression
1		cdleme18d.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		cdleme18d.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		cdleme18d.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		cdleme18d.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		cdleme18d.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		cdleme18d.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
7		cdleme18d.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		cdleme18d.g	$$⊢G=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
9		cdleme18d.d	$$⊢D=\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)$$
10		cdleme18d.e	$$⊢E=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)$$
11		eleq1	$$⊢R=P\to \left(R\in A\leftrightarrow P\in A\right)$$
12		breq1	$$⊢R=P\to \left(R\underset{\dot{}}{\le }W\leftrightarrow P\underset{\dot{}}{\le }W\right)$$
13	12	notbid	$$⊢R=P\to \left(\neg R\underset{\dot{}}{\le }W\leftrightarrow \neg P\underset{\dot{}}{\le }W\right)$$
14	11 13	anbi12d	$$⊢R=P\to \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\leftrightarrow \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\right)$$
15	14	3anbi1d	$$⊢R=P\to \left(\left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\leftrightarrow \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\right)$$
16	15	3anbi2d	$$⊢R=P\to \left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\leftrightarrow \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(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\right)$$
17		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(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
18		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(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
19		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(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to Q\in A$$
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(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)$$
21		simp322	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
22		eqid	$$⊢\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
23	1 2 3 4 5 6 7 22	cdleme17d1	$$⊢\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 Q\in A\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=Q$$
24	17 18 19 20 21 23	syl131anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=Q$$
25		simp23	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)$$
26		simp323	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
27		eqid	$$⊢\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(P\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(P\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)$$
28	1 2 3 4 5 6 9 27	cdleme17d1	$$⊢\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 Q\in A\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)=Q$$
29	17 18 19 25 26 28	syl131anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)=Q$$
30	24 29	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(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)$$
31	16 30	biimtrdi	$$⊢R=P\to \left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
32	8 10	eqeq12i	$$⊢G=E\leftrightarrow \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)$$
33		oveq1	$$⊢R=P\to R\underset{\dot{}}{\vee }S=P\underset{\dot{}}{\vee }S$$
34	33	oveq1d	$$⊢R=P\to \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W=\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W$$
35	34	oveq2d	$$⊢R=P\to F\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)=F\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)$$
36	35	oveq2d	$$⊢R=P\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
37		oveq1	$$⊢R=P\to R\underset{\dot{}}{\vee }T=P\underset{\dot{}}{\vee }T$$
38	37	oveq1d	$$⊢R=P\to \left(R\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W=\left(P\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W$$
39	38	oveq2d	$$⊢R=P\to D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)=D\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)$$
40	39	oveq2d	$$⊢R=P\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(R\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(P\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)$$
41	36 40	eqeq12d	$$⊢R=P\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)\leftrightarrow \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
42	32 41	bitrid	$$⊢R=P\to \left(G=E\leftrightarrow \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
43	31 42	sylibrd	$$⊢R=P\to \left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to G=E\right)$$
44	43	com12	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(R=P\to G=E\right)$$
45		eleq1	$$⊢R=Q\to \left(R\in A\leftrightarrow Q\in A\right)$$
46		breq1	$$⊢R=Q\to \left(R\underset{\dot{}}{\le }W\leftrightarrow Q\underset{\dot{}}{\le }W\right)$$
47	46	notbid	$$⊢R=Q\to \left(\neg R\underset{\dot{}}{\le }W\leftrightarrow \neg Q\underset{\dot{}}{\le }W\right)$$
48	45 47	anbi12d	$$⊢R=Q\to \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\leftrightarrow \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)$$
49	48	3anbi1d	$$⊢R=Q\to \left(\left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\leftrightarrow \left(\left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\right)$$
50		breq1	$$⊢R=Q\to \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
51	50	3anbi1d	$$⊢R=Q\to \left(\left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\leftrightarrow \left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)$$
52	51	3anbi2d	$$⊢R=Q\to \left(\left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(P\ne Q\wedge \left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)$$
53	49 52	3anbi23d	$$⊢R=Q\to \left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\leftrightarrow \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(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\right)$$
54		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(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to K\in \mathrm{HL}$$
55		simp11r	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to W\in H$$
56		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(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
57		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(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)$$
58		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(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)$$
59		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(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to P\ne Q$$
60		simp322	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
61		simp33	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)$$
62		eqid	$$⊢\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
63	1 2 3 4 5 6 7 62	cdleme18c	$$⊢\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)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=P$$
64	54 55 56 57 58 59 60 61 63	syl233anc	$$⊢\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(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=P$$
65		simp23	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)$$
66		simp323	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
67		eqid	$$⊢\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(Q\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(Q\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)$$
68	1 2 3 4 5 6 9 67	cdleme18c	$$⊢\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)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \neg T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)=P$$
69	54 55 56 57 65 59 66 61 68	syl233anc	$$⊢\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(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)=P$$
70	64 69	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(\left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)$$
71	53 70	biimtrdi	$$⊢R=Q\to \left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
72		oveq1	$$⊢R=Q\to R\underset{\dot{}}{\vee }S=Q\underset{\dot{}}{\vee }S$$
73	72	oveq1d	$$⊢R=Q\to \left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W=\left(Q\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W$$
74	73	oveq2d	$$⊢R=Q\to F\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)=F\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)$$
75	74	oveq2d	$$⊢R=Q\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
76		oveq1	$$⊢R=Q\to R\underset{\dot{}}{\vee }T=Q\underset{\dot{}}{\vee }T$$
77	76	oveq1d	$$⊢R=Q\to \left(R\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W=\left(Q\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W$$
78	77	oveq2d	$$⊢R=Q\to D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)=D\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)$$
79	78	oveq2d	$$⊢R=Q\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(R\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(Q\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)$$
80	75 79	eqeq12d	$$⊢R=Q\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)\leftrightarrow \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
81	32 80	bitrid	$$⊢R=Q\to \left(G=E\leftrightarrow \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(Q\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
82	71 81	sylibrd	$$⊢R=Q\to \left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to G=E\right)$$
83	82	com12	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(R=Q\to G=E\right)$$
84		simp11l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to K\in \mathrm{HL}$$
85		simp321	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
86		simp33	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)$$
87		simp12l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to P\in A$$
88		simp13l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to Q\in A$$
89		simp31	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to P\ne Q$$
90		simp21l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to R\in A$$
91		simp21r	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \neg R\underset{\dot{}}{\le }W$$
92	1 2 4	cdleme0nex	$$⊢\left(\left(K\in \mathrm{HL}\wedge R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge P\ne Q\right)\wedge \left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\right)\to \left(R=P\vee R=Q\right)$$
93	84 85 86 87 88 89 90 91 92	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(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(R=P\vee R=Q\right)$$
94	44 83 93	mpjaod	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(R\in A\wedge \neg R\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge \left(R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\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)\wedge \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to G=E$$