Theorem islvol5

Description: The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012)

	Ref	Expression
Hypotheses	islvol5.b	$$⊢B={\mathrm{Base}}_K$$
	islvol5.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	islvol5.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	islvol5.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	islvol5.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
Assertion	islvol5	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(X\in V\leftrightarrow \exists p\in A\exists q\in A\exists r\in A\exists s\in A\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		islvol5.b	$$⊢B={\mathrm{Base}}_K$$
2		islvol5.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		islvol5.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		islvol5.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		islvol5.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
6		eqid	$$⊢\mathrm{LPlanes}\left(K\right)=\mathrm{LPlanes}\left(K\right)$$
7	1 2 3 4 6 5	islvol3	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(X\in V\leftrightarrow \exists y\in \mathrm{LPlanes}\left(K\right)\exists s\in A\left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)$$
8		df-rex	$$⊢\exists y\in \mathrm{LPlanes}\left(K\right)\exists s\in A\left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\leftrightarrow \exists y\left(y\in \mathrm{LPlanes}\left(K\right)\wedge \exists s\in A\left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)$$
9		r19.41v	$$⊢\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(\exists s\in A\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
10		df-3an	$$⊢\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\leftrightarrow \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)$$
11	10	anbi2i	$$⊢\left(\exists s\in A\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(\exists s\in A\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
12		an13	$$⊢\left(\exists s\in A\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\wedge \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \exists s\in A\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)\right)$$
13	11 12	bitri	$$⊢\left(\exists s\in A\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\wedge \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \exists s\in A\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)\right)$$
14	9 13	bitri	$$⊢\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\wedge \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \exists s\in A\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)\right)$$
15	14	exbii	$$⊢\exists y\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists y\left(y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\wedge \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \exists s\in A\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)\right)$$
16		ovex	$$⊢\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\in \mathrm{V}$$
17		an12	$$⊢\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)\leftrightarrow \left(y\in B\wedge \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)$$
18		eleq1	$$⊢y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\to \left(y\in B\leftrightarrow \left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\in B\right)$$
19		breq2	$$⊢y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\to \left(s\underset{\dot{}}{\le }y\leftrightarrow s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
20	19	notbid	$$⊢y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\to \left(\neg s\underset{\dot{}}{\le }y\leftrightarrow \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
21		oveq1	$$⊢y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\to y\underset{\dot{}}{\vee }s=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s$$
22	21	eqeq2d	$$⊢y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\to \left(X=y\underset{\dot{}}{\vee }s\leftrightarrow X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)$$
23	20 22	anbi12d	$$⊢y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\to \left(\left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\leftrightarrow \left(\neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$
24	23	anbi2d	$$⊢y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\to \left(\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\leftrightarrow \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \left(\neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)\right)$$
25		anass	$$⊢\left(\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\leftrightarrow \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \left(\neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$
26		df-3an	$$⊢\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
27	26	bicomi	$$⊢\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
28	27	anbi1i	$$⊢\left(\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\leftrightarrow \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)$$
29	25 28	bitr3i	$$⊢\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \left(\neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)\leftrightarrow \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)$$
30	24 29	bitrdi	$$⊢y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\to \left(\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\leftrightarrow \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$
31	18 30	anbi12d	$$⊢y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\to \left(\left(y\in B\wedge \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)\leftrightarrow \left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\in B\wedge \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)\right)$$
32	17 31	bitrid	$$⊢y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\to \left(\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)\leftrightarrow \left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\in B\wedge \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)\right)$$
33	32	rexbidv	$$⊢y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\to \left(\exists s\in A\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)\leftrightarrow \exists s\in A\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\in B\wedge \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)\right)$$
34		r19.42v	$$⊢\exists s\in A\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)\leftrightarrow \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \exists s\in A\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)$$
35		r19.42v	$$⊢\exists s\in A\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\in B\wedge \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)\leftrightarrow \left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\in B\wedge \exists s\in A\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$
36	33 34 35	3bitr3g	$$⊢y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\to \left(\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \exists s\in A\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)\leftrightarrow \left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\in B\wedge \exists s\in A\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)\right)$$
37	16 36	ceqsexv	$$⊢\exists y\left(y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\wedge \left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)\wedge \exists s\in A\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)\right)\leftrightarrow \left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\in B\wedge \exists s\in A\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$
38	15 37	bitri	$$⊢\exists y\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\in B\wedge \exists s\in A\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$
39		hllat	$$⊢K\in \mathrm{HL}\to K\in \mathrm{Lat}$$
40	39	ad3antrrr	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge X\in B\right)\wedge \left(p\in A\wedge q\in A\right)\right)\wedge r\in A\right)\to K\in \mathrm{Lat}$$
41		simplll	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge X\in B\right)\wedge \left(p\in A\wedge q\in A\right)\right)\wedge r\in A\right)\to K\in \mathrm{HL}$$
42		simplrl	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge X\in B\right)\wedge \left(p\in A\wedge q\in A\right)\right)\wedge r\in A\right)\to p\in A$$
43		simplrr	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge X\in B\right)\wedge \left(p\in A\wedge q\in A\right)\right)\wedge r\in A\right)\to q\in A$$
44	1 3 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge p\in A\wedge q\in A\right)\to p\underset{\dot{}}{\vee }q\in B$$
45	41 42 43 44	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge X\in B\right)\wedge \left(p\in A\wedge q\in A\right)\right)\wedge r\in A\right)\to p\underset{\dot{}}{\vee }q\in B$$
46	1 4	atbase	$$⊢r\in A\to r\in B$$
47	46	adantl	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge X\in B\right)\wedge \left(p\in A\wedge q\in A\right)\right)\wedge r\in A\right)\to r\in B$$
48	1 3	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge p\underset{\dot{}}{\vee }q\in B\wedge r\in B\right)\to \left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\in B$$
49	40 45 47 48	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge X\in B\right)\wedge \left(p\in A\wedge q\in A\right)\right)\wedge r\in A\right)\to \left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\in B$$
50	49	biantrurd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge X\in B\right)\wedge \left(p\in A\wedge q\in A\right)\right)\wedge r\in A\right)\to \left(\exists s\in A\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\leftrightarrow \left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\in B\wedge \exists s\in A\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)\right)$$
51	38 50	bitr4id	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge X\in B\right)\wedge \left(p\in A\wedge q\in A\right)\right)\wedge r\in A\right)\to \left(\exists y\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists s\in A\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$
52	51	rexbidva	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\right)\wedge \left(p\in A\wedge q\in A\right)\right)\to \left(\exists r\in A\exists y\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists r\in A\exists s\in A\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$
53	52	2rexbidva	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\exists p\in A\exists q\in A\exists r\in A\exists y\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists p\in A\exists q\in A\exists r\in A\exists s\in A\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$
54		rexcom4	$$⊢\exists r\in A\exists y\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists y\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
55	54	rexbii	$$⊢\exists q\in A\exists r\in A\exists y\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists q\in A\exists y\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
56		rexcom4	$$⊢\exists q\in A\exists y\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists y\exists q\in A\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
57	55 56	bitri	$$⊢\exists q\in A\exists r\in A\exists y\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists y\exists q\in A\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
58	57	rexbii	$$⊢\exists p\in A\exists q\in A\exists r\in A\exists y\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists p\in A\exists y\exists q\in A\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
59		rexcom4	$$⊢\exists p\in A\exists y\exists q\in A\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists y\exists p\in A\exists q\in A\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
60	58 59	bitri	$$⊢\exists p\in A\exists q\in A\exists r\in A\exists y\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists y\exists p\in A\exists q\in A\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
61	53 60	bitr3di	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\exists p\in A\exists q\in A\exists r\in A\exists s\in A\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\leftrightarrow \exists y\exists p\in A\exists q\in A\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\right)$$
62		rexcom	$$⊢\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists s\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
63	62	rexbii	$$⊢\exists q\in A\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists q\in A\exists s\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
64		rexcom	$$⊢\exists q\in A\exists s\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists s\in A\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
65	63 64	bitri	$$⊢\exists q\in A\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists s\in A\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
66	65	rexbii	$$⊢\exists p\in A\exists q\in A\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists p\in A\exists s\in A\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
67		rexcom	$$⊢\exists p\in A\exists s\in A\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists s\in A\exists p\in A\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
68	66 67	bitri	$$⊢\exists p\in A\exists q\in A\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists s\in A\exists p\in A\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
69	1 2 3 4 6	islpln2	$$⊢K\in \mathrm{HL}\to \left(y\in \mathrm{LPlanes}\left(K\right)\leftrightarrow \left(y\in B\wedge \exists p\in A\exists q\in A\exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\right)$$
70	69	adantr	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(y\in \mathrm{LPlanes}\left(K\right)\leftrightarrow \left(y\in B\wedge \exists p\in A\exists q\in A\exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\right)$$
71	70	anbi1d	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\left(y\in \mathrm{LPlanes}\left(K\right)\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\leftrightarrow \left(\left(y\in B\wedge \exists p\in A\exists q\in A\exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)$$
72		r19.42v	$$⊢\exists p\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \exists q\in A\exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \exists p\in A\exists q\in A\exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
73		r19.42v	$$⊢\exists r\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
74	73	rexbii	$$⊢\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists q\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
75		r19.42v	$$⊢\exists q\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \exists q\in A\exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
76	74 75	bitri	$$⊢\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \exists q\in A\exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
77	76	rexbii	$$⊢\exists p\in A\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists p\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \exists q\in A\exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
78		an32	$$⊢\left(\left(y\in B\wedge \exists p\in A\exists q\in A\exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\leftrightarrow \left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \exists p\in A\exists q\in A\exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
79	72 77 78	3bitr4ri	$$⊢\left(\left(y\in B\wedge \exists p\in A\exists q\in A\exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\leftrightarrow \exists p\in A\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
80	71 79	bitrdi	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\left(y\in \mathrm{LPlanes}\left(K\right)\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\leftrightarrow \exists p\in A\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\right)$$
81	80	rexbidv	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\exists s\in A\left(y\in \mathrm{LPlanes}\left(K\right)\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\leftrightarrow \exists s\in A\exists p\in A\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\right)$$
82	68 81	bitr4id	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\exists p\in A\exists q\in A\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists s\in A\left(y\in \mathrm{LPlanes}\left(K\right)\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)$$
83		r19.42v	$$⊢\exists s\in A\left(y\in \mathrm{LPlanes}\left(K\right)\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\leftrightarrow \left(y\in \mathrm{LPlanes}\left(K\right)\wedge \exists s\in A\left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)$$
84	82 83	bitrdi	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\exists p\in A\exists q\in A\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(y\in \mathrm{LPlanes}\left(K\right)\wedge \exists s\in A\left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)$$
85	84	exbidv	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\exists y\exists p\in A\exists q\in A\exists r\in A\exists s\in A\left(\left(y\in B\wedge \left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge y=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists y\left(y\in \mathrm{LPlanes}\left(K\right)\wedge \exists s\in A\left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)$$
86	61 85	bitrd	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\exists p\in A\exists q\in A\exists r\in A\exists s\in A\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\leftrightarrow \exists y\left(y\in \mathrm{LPlanes}\left(K\right)\wedge \exists s\in A\left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\right)\right)$$
87	8 86	bitr4id	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\exists y\in \mathrm{LPlanes}\left(K\right)\exists s\in A\left(\neg s\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }s\right)\leftrightarrow \exists p\in A\exists q\in A\exists r\in A\exists s\in A\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$
88	7 87	bitrd	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(X\in V\leftrightarrow \exists p\in A\exists q\in A\exists r\in A\exists s\in A\left(\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge \neg s\underset{\dot{}}{\le }\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\wedge X=\left(\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\underset{\dot{}}{\vee }s\right)\right)$$