Theorem 4atex

Description: Whenever there are at least 4 atoms under P .\/ Q (specifically, P , Q , r , and ( P .\/ Q ) ./\ W ), there are also at least 4 atoms under P .\/ S . This proves the statement in Lemma E of Crawley p. 114, last line, "...p \/ q/0 and hence p \/ s/0 contains at least four atoms..." Note that by cvlsupr2 , our ( P .\/ r ) = ( Q .\/ r ) is a shorter way to express r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) . (Contributed by NM, 27-May-2013)

	Ref	Expression
Hypotheses	4that.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	4that.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	4that.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	4that.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	4atex	$$⊢\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 S\in A\right)\wedge \left(P\ne Q\wedge \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 \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)$$

Proof

Step	Hyp	Ref	Expression
1		4that.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		4that.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		4that.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		4that.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
5		simp21l	$$⊢\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 S\in A\right)\wedge \left(P\ne Q\wedge \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$$
6	5	ad2antrr	$$⊢\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S=P\right)\to P\in A$$
7		simp21r	$$⊢\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 S\in A\right)\wedge \left(P\ne Q\wedge \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 P\underset{\dot{}}{\le }W$$
8	7	ad2antrr	$$⊢\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S=P\right)\to \neg P\underset{\dot{}}{\le }W$$
9		oveq1	$$⊢P=S\to P\underset{\dot{}}{\vee }P=S\underset{\dot{}}{\vee }P$$
10	9	eqcoms	$$⊢S=P\to P\underset{\dot{}}{\vee }P=S\underset{\dot{}}{\vee }P$$
11	10	adantl	$$⊢\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S=P\right)\to P\underset{\dot{}}{\vee }P=S\underset{\dot{}}{\vee }P$$
12		breq1	$$⊢z=P\to \left(z\underset{\dot{}}{\le }W\leftrightarrow P\underset{\dot{}}{\le }W\right)$$
13	12	notbid	$$⊢z=P\to \left(\neg z\underset{\dot{}}{\le }W\leftrightarrow \neg P\underset{\dot{}}{\le }W\right)$$
14		oveq2	$$⊢z=P\to P\underset{\dot{}}{\vee }z=P\underset{\dot{}}{\vee }P$$
15		oveq2	$$⊢z=P\to S\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }P$$
16	14 15	eqeq12d	$$⊢z=P\to \left(P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\leftrightarrow P\underset{\dot{}}{\vee }P=S\underset{\dot{}}{\vee }P\right)$$
17	13 16	anbi12d	$$⊢z=P\to \left(\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\leftrightarrow \left(\neg P\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }P=S\underset{\dot{}}{\vee }P\right)\right)$$
18	17	rspcev	$$⊢\left(P\in A\wedge \left(\neg P\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }P=S\underset{\dot{}}{\vee }P\right)\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)$$
19	6 8 11 18	syl12anc	$$⊢\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S=P\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)$$
20		simpl3r	$$⊢\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)$$
21	20	ad2antrr	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S=Q\right)\to \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)$$
22		breq1	$$⊢r=z\to \left(r\underset{\dot{}}{\le }W\leftrightarrow z\underset{\dot{}}{\le }W\right)$$
23	22	notbid	$$⊢r=z\to \left(\neg r\underset{\dot{}}{\le }W\leftrightarrow \neg z\underset{\dot{}}{\le }W\right)$$
24		oveq2	$$⊢r=z\to P\underset{\dot{}}{\vee }r=P\underset{\dot{}}{\vee }z$$
25		oveq2	$$⊢r=z\to Q\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }z$$
26	24 25	eqeq12d	$$⊢r=z\to \left(P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\leftrightarrow P\underset{\dot{}}{\vee }z=Q\underset{\dot{}}{\vee }z\right)$$
27	23 26	anbi12d	$$⊢r=z\to \left(\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\leftrightarrow \left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=Q\underset{\dot{}}{\vee }z\right)\right)$$
28	27	cbvrexvw	$$⊢\exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\leftrightarrow \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=Q\underset{\dot{}}{\vee }z\right)$$
29		oveq1	$$⊢S=Q\to S\underset{\dot{}}{\vee }z=Q\underset{\dot{}}{\vee }z$$
30	29	eqeq2d	$$⊢S=Q\to \left(P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\leftrightarrow P\underset{\dot{}}{\vee }z=Q\underset{\dot{}}{\vee }z\right)$$
31	30	anbi2d	$$⊢S=Q\to \left(\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\leftrightarrow \left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=Q\underset{\dot{}}{\vee }z\right)\right)$$
32	31	rexbidv	$$⊢S=Q\to \left(\exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\leftrightarrow \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=Q\underset{\dot{}}{\vee }z\right)\right)$$
33	28 32	bitr4id	$$⊢S=Q\to \left(\exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\leftrightarrow \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)$$
34	33	adantl	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S=Q\right)\to \left(\exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\leftrightarrow \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\right)$$
35	21 34	mpbid	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S=Q\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)$$
36		simp22l	$$⊢\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 S\in A\right)\wedge \left(P\ne Q\wedge \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$$
37	36	ad3antrrr	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S\ne Q\right)\to Q\in A$$
38		simp22r	$$⊢\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 S\in A\right)\wedge \left(P\ne Q\wedge \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 Q\underset{\dot{}}{\le }W$$
39	38	ad3antrrr	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S\ne Q\right)\to \neg Q\underset{\dot{}}{\le }W$$
40		simp3l	$$⊢\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 S\in A\right)\wedge \left(P\ne Q\wedge \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$$
41	40	necomd	$$⊢\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 S\in A\right)\wedge \left(P\ne Q\wedge \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\ne P$$
42	41	ad3antrrr	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S\ne Q\right)\to Q\ne P$$
43		simpr	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S\ne Q\right)\to S\ne Q$$
44	43	necomd	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S\ne Q\right)\to Q\ne S$$
45		simpllr	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S\ne Q\right)\to S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
46		simp1l	$$⊢\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 S\in A\right)\wedge \left(P\ne Q\wedge \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}$$
47		hlcvl	$$⊢K\in \mathrm{HL}\to K\in \mathrm{CvLat}$$
48	46 47	syl	$$⊢\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 S\in A\right)\wedge \left(P\ne Q\wedge \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{CvLat}$$
49	48	ad3antrrr	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S\ne Q\right)\to K\in \mathrm{CvLat}$$
50		simp23	$$⊢\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 S\in A\right)\wedge \left(P\ne Q\wedge \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 S\in A$$
51	50	ad3antrrr	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S\ne Q\right)\to S\in A$$
52	5	ad3antrrr	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S\ne Q\right)\to P\in A$$
53		simplr	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S\ne Q\right)\to S\ne P$$
54	1 2 3	cvlatexch1	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(S\in A\wedge Q\in A\wedge P\in A\right)\wedge S\ne P\right)\to \left(S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\to Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\right)$$
55	49 51 37 52 53 54	syl131anc	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S\ne Q\right)\to \left(S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\to Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\right)$$
56	45 55	mpd	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S\ne Q\right)\to Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)$$
57	53	necomd	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S\ne Q\right)\to P\ne S$$
58	3 1 2	cvlsupr2	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge S\in A\wedge Q\in A\right)\wedge P\ne S\right)\to \left(P\underset{\dot{}}{\vee }Q=S\underset{\dot{}}{\vee }Q\leftrightarrow \left(Q\ne P\wedge Q\ne S\wedge Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\right)\right)$$
59	49 52 51 37 57 58	syl131anc	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S\ne Q\right)\to \left(P\underset{\dot{}}{\vee }Q=S\underset{\dot{}}{\vee }Q\leftrightarrow \left(Q\ne P\wedge Q\ne S\wedge Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\right)\right)$$
60	42 44 56 59	mpbir3and	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S\ne Q\right)\to P\underset{\dot{}}{\vee }Q=S\underset{\dot{}}{\vee }Q$$
61		breq1	$$⊢z=Q\to \left(z\underset{\dot{}}{\le }W\leftrightarrow Q\underset{\dot{}}{\le }W\right)$$
62	61	notbid	$$⊢z=Q\to \left(\neg z\underset{\dot{}}{\le }W\leftrightarrow \neg Q\underset{\dot{}}{\le }W\right)$$
63		oveq2	$$⊢z=Q\to P\underset{\dot{}}{\vee }z=P\underset{\dot{}}{\vee }Q$$
64		oveq2	$$⊢z=Q\to S\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }Q$$
65	63 64	eqeq12d	$$⊢z=Q\to \left(P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\leftrightarrow P\underset{\dot{}}{\vee }Q=S\underset{\dot{}}{\vee }Q\right)$$
66	62 65	anbi12d	$$⊢z=Q\to \left(\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)\leftrightarrow \left(\neg Q\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }Q=S\underset{\dot{}}{\vee }Q\right)\right)$$
67	66	rspcev	$$⊢\left(Q\in A\wedge \left(\neg Q\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }Q=S\underset{\dot{}}{\vee }Q\right)\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)$$
68	37 39 60 67	syl12anc	$$⊢\left(\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\wedge S\ne Q\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)$$
69	35 68	pm2.61dane	$$⊢\left(\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge S\ne P\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)$$
70	19 69	pm2.61dane	$$⊢\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)$$
71		simpl1	$$⊢\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
72		simpl2	$$⊢\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to \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 S\in A\right)$$
73		simpl3l	$$⊢\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to P\ne Q$$
74		simpr	$$⊢\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
75		simpl3r	$$⊢\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)$$
76	1 2 3 4	4atexlem7	$$⊢\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 S\in A\right)\wedge \left(P\ne Q\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \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 \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)$$
77	71 72 73 74 75 76	syl113anc	$$⊢\left(\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 S\in A\right)\wedge \left(P\ne Q\wedge \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)\wedge \neg S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)$$
78	70 77	pm2.61dan	$$⊢\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 S\in A\right)\wedge \left(P\ne Q\wedge \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 \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)$$