Theorem cdlemg17h

Description: TODO: fix comment. (Contributed by NM, 10-May-2013)

	Ref	Expression
Hypotheses	cdlemg12.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdlemg12.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdlemg12.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdlemg12.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdlemg12.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdlemg12.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	cdlemg12b.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
Assertion	cdlemg17h	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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(S=F\left(P\right)\vee S=F\left(Q\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cdlemg12.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		cdlemg12.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		cdlemg12.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		cdlemg12.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		cdlemg12.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		cdlemg12.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
7		cdlemg12b.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
8		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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 K\in \mathrm{HL}$$
9		simp23r	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)$$
10		simp11	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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(K\in \mathrm{HL}\wedge W\in H\right)$$
11		simp22l	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 F\in T$$
12		simp21l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 S\in A$$
13	1 4 5 6	ltrncnvat	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge S\in A\right)\to F^{-1}\left(S\right)\in A$$
14	10 11 12 13	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 F^{-1}\left(S\right)\in A$$
15		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
16	15 4	atbase	$$⊢F^{-1}\left(S\right)\in A\to F^{-1}\left(S\right)\in {\mathrm{Base}}_K$$
17	14 16	syl	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 F^{-1}\left(S\right)\in {\mathrm{Base}}_K$$
18		simp12l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 P\in A$$
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(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 Q\in A$$
20	15 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
21	8 18 19 20	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
22	15 1 5 6	ltrnle	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge \left(F^{-1}\left(S\right)\in {\mathrm{Base}}_K\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\right)\right)\to \left(F^{-1}\left(S\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow F\left(F^{-1}\left(S\right)\right)\underset{\dot{}}{\le }F\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
23	10 11 17 21 22	syl112anc	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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(F^{-1}\left(S\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow F\left(F^{-1}\left(S\right)\right)\underset{\dot{}}{\le }F\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
24	15 5 6	ltrn1o	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\right)\to F:{\mathrm{Base}}_K\underset{1-1\; onto}{⟶}{\mathrm{Base}}_K$$
25	10 11 24	syl2anc	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 F:{\mathrm{Base}}_K\underset{1-1\; onto}{⟶}{\mathrm{Base}}_K$$
26	15 4	atbase	$$⊢S\in A\to S\in {\mathrm{Base}}_K$$
27	12 26	syl	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 S\in {\mathrm{Base}}_K$$
28		f1ocnvfv2	$$⊢\left(F:{\mathrm{Base}}_K\underset{1-1\; onto}{⟶}{\mathrm{Base}}_K\wedge S\in {\mathrm{Base}}_K\right)\to F\left(F^{-1}\left(S\right)\right)=S$$
29	25 27 28	syl2anc	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 F\left(F^{-1}\left(S\right)\right)=S$$
30	15 4	atbase	$$⊢P\in A\to P\in {\mathrm{Base}}_K$$
31	18 30	syl	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 P\in {\mathrm{Base}}_K$$
32	15 4	atbase	$$⊢Q\in A\to Q\in {\mathrm{Base}}_K$$
33	19 32	syl	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 Q\in {\mathrm{Base}}_K$$
34	15 2 5 6	ltrnj	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge \left(P\in {\mathrm{Base}}_K\wedge Q\in {\mathrm{Base}}_K\right)\right)\to F\left(P\underset{\dot{}}{\vee }Q\right)=F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)$$
35	10 11 31 33 34	syl112anc	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 F\left(P\underset{\dot{}}{\vee }Q\right)=F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)$$
36	29 35	breq12d	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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(F\left(F^{-1}\left(S\right)\right)\underset{\dot{}}{\le }F\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)$$
37	23 36	bitr2d	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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(S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\leftrightarrow F^{-1}\left(S\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
38	9 37	mpbid	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 F^{-1}\left(S\right)\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
39		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(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 \neg \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)$$
40		simp23l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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 P\ne Q$$
41		simp21	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)$$
42	1 4 5 6	ltrncnvel	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge F\in T\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\to \left(F^{-1}\left(S\right)\in A\wedge \neg F^{-1}\left(S\right)\underset{\dot{}}{\le }W\right)$$
43	10 11 41 42	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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(F^{-1}\left(S\right)\in A\wedge \neg F^{-1}\left(S\right)\underset{\dot{}}{\le }W\right)$$
44	1 2 4	cdleme0nex	$$⊢\left(\left(K\in \mathrm{HL}\wedge F^{-1}\left(S\right)\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(F^{-1}\left(S\right)\in A\wedge \neg F^{-1}\left(S\right)\underset{\dot{}}{\le }W\right)\right)\to \left(F^{-1}\left(S\right)=P\vee F^{-1}\left(S\right)=Q\right)$$
45	8 38 39 18 19 40 43 44	syl331anc	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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(F^{-1}\left(S\right)=P\vee F^{-1}\left(S\right)=Q\right)$$
46		f1ocnvfvb	$$⊢\left(F:{\mathrm{Base}}_K\underset{1-1\; onto}{⟶}{\mathrm{Base}}_K\wedge P\in {\mathrm{Base}}_K\wedge S\in {\mathrm{Base}}_K\right)\to \left(F\left(P\right)=S\leftrightarrow F^{-1}\left(S\right)=P\right)$$
47	25 31 27 46	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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(F\left(P\right)=S\leftrightarrow F^{-1}\left(S\right)=P\right)$$
48		eqcom	$$⊢F\left(P\right)=S\leftrightarrow S=F\left(P\right)$$
49	47 48	bitr3di	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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(F^{-1}\left(S\right)=P\leftrightarrow S=F\left(P\right)\right)$$
50		f1ocnvfvb	$$⊢\left(F:{\mathrm{Base}}_K\underset{1-1\; onto}{⟶}{\mathrm{Base}}_K\wedge Q\in {\mathrm{Base}}_K\wedge S\in {\mathrm{Base}}_K\right)\to \left(F\left(Q\right)=S\leftrightarrow F^{-1}\left(S\right)=Q\right)$$
51	25 33 27 50	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\wedge \left(\left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \left(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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(F\left(Q\right)=S\leftrightarrow F^{-1}\left(S\right)=Q\right)$$
52		eqcom	$$⊢F\left(Q\right)=S\leftrightarrow S=F\left(Q\right)$$
53	51 52	bitr3di	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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(F^{-1}\left(S\right)=Q\leftrightarrow S=F\left(Q\right)\right)$$
54	49 53	orbi12d	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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(\left(F^{-1}\left(S\right)=P\vee F^{-1}\left(S\right)=Q\right)\leftrightarrow \left(S=F\left(P\right)\vee S=F\left(Q\right)\right)\right)$$
55	45 54	mpbid	$$⊢\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(F\in T\wedge G\in T\right)\wedge \left(P\ne Q\wedge S\underset{\dot{}}{\le }\left(F\left(P\right)\underset{\dot{}}{\vee }F\left(Q\right)\right)\right)\right)\wedge \left(G\left(P\right)\ne P\wedge R\left(G\right)\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(S=F\left(P\right)\vee S=F\left(Q\right)\right)$$