Theorem cdleme26ee

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 4th line on p. 115. F , N , O represent f(z), f_z(s), f_z(t) respectively. When t \/ v = p \/ q, f_z(s) <_ f_z(t) \/ v. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013)

	Ref	Expression
Hypotheses	cdleme26.b	$$⊢B={\mathrm{Base}}_K$$
	cdleme26.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdleme26.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdleme26.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdleme26.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdleme26.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdleme26e.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
	cdleme26e.f	$$⊢F=\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)$$
	cdleme26e.n	$$⊢N=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme26e.o	$$⊢O=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme26e.i	$$⊢I=\left(\iota u\in B|\forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=N\right)\right)$$
	cdleme26e.e	$$⊢E=\left(\iota u\in B|\forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=O\right)\right)$$
Assertion	cdleme26ee	$$⊢\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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\to I\underset{\dot{}}{\le }\left(E\underset{\dot{}}{\vee }V\right)$$

Proof

Step	Hyp	Ref	Expression
1		cdleme26.b	$$⊢B={\mathrm{Base}}_K$$
2		cdleme26.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		cdleme26.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		cdleme26.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		cdleme26.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		cdleme26.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
7		cdleme26e.u	$$⊢U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }W$$
8		cdleme26e.f	$$⊢F=\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		cdleme26e.n	$$⊢N=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
10		cdleme26e.o	$$⊢O=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(F\underset{\dot{}}{\vee }\left(\left(T\underset{\dot{}}{\vee }z\right)\underset{\dot{}}{\wedge }W\right)\right)$$
11		cdleme26e.i	$$⊢I=\left(\iota u\in B|\forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=N\right)\right)$$
12		cdleme26e.e	$$⊢E=\left(\iota u\in B|\forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=O\right)\right)$$
13		simp11l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\to K\in \mathrm{HL}$$
14		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(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\to W\in H$$
15		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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
16		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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\to \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)$$
17		simp3l1	$$⊢\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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\to P\ne Q$$
18	2 3 5 6	cdlemb2	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge P\ne Q\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
19	13 14 15 16 17 18	syl221anc	$$⊢\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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
20		nfv	$$⊢Ⅎz\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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)$$
21		nfra1	$$⊢Ⅎz\forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=N\right)$$
22		nfcv	$$⊢\underset{\_}{Ⅎ}zB$$
23	21 22	nfriota	$$⊢\underset{\_}{Ⅎ}z\left(\iota u\in B|\forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=N\right)\right)$$
24	11 23	nfcxfr	$$⊢\underset{\_}{Ⅎ}zI$$
25		nfcv	$$⊢\underset{\_}{Ⅎ}z\underset{\dot{}}{\le }$$
26		nfra1	$$⊢Ⅎz\forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=O\right)$$
27	26 22	nfriota	$$⊢\underset{\_}{Ⅎ}z\left(\iota u\in B|\forall z\in A\left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to u=O\right)\right)$$
28	12 27	nfcxfr	$$⊢\underset{\_}{Ⅎ}zE$$
29		nfcv	$$⊢\underset{\_}{Ⅎ}z\underset{\dot{}}{\vee }$$
30		nfcv	$$⊢\underset{\_}{Ⅎ}zV$$
31	28 29 30	nfov	$$⊢\underset{\_}{Ⅎ}z\left(E\underset{\dot{}}{\vee }V\right)$$
32	24 25 31	nfbr	$$⊢ℲzI\underset{\dot{}}{\le }\left(E\underset{\dot{}}{\vee }V\right)$$
33		simp111	$$⊢\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(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\wedge z\in A\wedge \left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
34		simp112	$$⊢\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(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\wedge z\in A\wedge \left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
35		simp113	$$⊢\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(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\wedge z\in A\wedge \left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)$$
36		simp121	$$⊢\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(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\wedge z\in A\wedge \left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)$$
37		simp122	$$⊢\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(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\wedge z\in A\wedge \left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(T\in A\wedge \neg T\underset{\dot{}}{\le }W\right)$$
38		simp123	$$⊢\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(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\wedge z\in A\wedge \left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
39		simp13l	$$⊢\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(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\wedge z\in A\wedge \left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
40		simp13r	$$⊢\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(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\wedge z\in A\wedge \left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q$$
41		simp3r	$$⊢\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(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\wedge z\in A\wedge \left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
42	40 41	jca	$$⊢\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(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\wedge z\in A\wedge \left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
43		simp2	$$⊢\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(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\wedge z\in A\wedge \left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to z\in A$$
44		simp3l	$$⊢\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(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\wedge z\in A\wedge \left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \neg z\underset{\dot{}}{\le }W$$
45	43 44	jca	$$⊢\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(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\wedge z\in A\wedge \left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)$$
46	1 2 3 4 5 6 7 8 9 10 11 12	cdleme26e	$$⊢\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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge \left(z\in A\wedge \neg z\underset{\dot{}}{\le }W\right)\right)\right)\to I\underset{\dot{}}{\le }\left(E\underset{\dot{}}{\vee }V\right)$$
47	33 34 35 36 37 38 39 42 45 46	syl333anc	$$⊢\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(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\wedge z\in A\wedge \left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\to I\underset{\dot{}}{\le }\left(E\underset{\dot{}}{\vee }V\right)$$
48	47	3exp	$$⊢\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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\to \left(z\in A\to \left(\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to I\underset{\dot{}}{\le }\left(E\underset{\dot{}}{\vee }V\right)\right)\right)$$
49	20 32 48	rexlimd	$$⊢\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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\to \left(\exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge \neg z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to I\underset{\dot{}}{\le }\left(E\underset{\dot{}}{\vee }V\right)\right)$$
50	19 49	mpd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(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(V\in A\wedge V\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge T\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge T\underset{\dot{}}{\vee }V=P\underset{\dot{}}{\vee }Q\right)\right)\to I\underset{\dot{}}{\le }\left(E\underset{\dot{}}{\vee }V\right)$$