Theorem islpln5

Description: The predicate "is a lattice plane" in terms of atoms. (Contributed by NM, 24-Jun-2012)

	Ref	Expression
Hypotheses	islpln5.b	$$⊢B={\mathrm{Base}}_K$$
	islpln5.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	islpln5.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	islpln5.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	islpln5.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
Assertion	islpln5	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(X\in P\leftrightarrow \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 X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		islpln5.b	$$⊢B={\mathrm{Base}}_K$$
2		islpln5.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		islpln5.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		islpln5.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		islpln5.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
6		eqid	$$⊢\mathrm{LLines}\left(K\right)=\mathrm{LLines}\left(K\right)$$
7	1 2 3 4 6 5	islpln3	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(X\in P\leftrightarrow \exists y\in \mathrm{LLines}\left(K\right)\exists r\in A\left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)$$
8		df-rex	$$⊢\exists y\in \mathrm{LLines}\left(K\right)\exists r\in A\left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\leftrightarrow \exists y\left(y\in \mathrm{LLines}\left(K\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)$$
9		r19.41v	$$⊢\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \left(\exists r\in A\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)$$
10		an13	$$⊢\left(\exists r\in A\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \left(y=p\underset{\dot{}}{\vee }q\wedge \left(p\ne q\wedge \exists r\in A\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)\right)$$
11	9 10	bitri	$$⊢\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \left(y=p\underset{\dot{}}{\vee }q\wedge \left(p\ne q\wedge \exists r\in A\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)\right)$$
12	11	exbii	$$⊢\exists y\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \exists y\left(y=p\underset{\dot{}}{\vee }q\wedge \left(p\ne q\wedge \exists r\in A\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)\right)$$
13		ovex	$$⊢p\underset{\dot{}}{\vee }q\in \mathrm{V}$$
14		an12	$$⊢\left(p\ne q\wedge \left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)\leftrightarrow \left(y\in B\wedge \left(p\ne q\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)$$
15		eleq1	$$⊢y=p\underset{\dot{}}{\vee }q\to \left(y\in B\leftrightarrow p\underset{\dot{}}{\vee }q\in B\right)$$
16		breq2	$$⊢y=p\underset{\dot{}}{\vee }q\to \left(r\underset{\dot{}}{\le }y\leftrightarrow r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)$$
17	16	notbid	$$⊢y=p\underset{\dot{}}{\vee }q\to \left(\neg r\underset{\dot{}}{\le }y\leftrightarrow \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\right)$$
18		oveq1	$$⊢y=p\underset{\dot{}}{\vee }q\to y\underset{\dot{}}{\vee }r=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r$$
19	18	eqeq2d	$$⊢y=p\underset{\dot{}}{\vee }q\to \left(X=y\underset{\dot{}}{\vee }r\leftrightarrow X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)$$
20	17 19	anbi12d	$$⊢y=p\underset{\dot{}}{\vee }q\to \left(\left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\leftrightarrow \left(\neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
21	20	anbi2d	$$⊢y=p\underset{\dot{}}{\vee }q\to \left(\left(p\ne q\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(p\ne q\wedge \left(\neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\right)$$
22		3anass	$$⊢\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\leftrightarrow \left(p\ne q\wedge \left(\neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
23	21 22	bitr4di	$$⊢y=p\underset{\dot{}}{\vee }q\to \left(\left(p\ne q\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\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 X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
24	15 23	anbi12d	$$⊢y=p\underset{\dot{}}{\vee }q\to \left(\left(y\in B\wedge \left(p\ne q\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)\leftrightarrow \left(p\underset{\dot{}}{\vee }q\in B\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\right)$$
25	14 24	syl5bb	$$⊢y=p\underset{\dot{}}{\vee }q\to \left(\left(p\ne q\wedge \left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)\leftrightarrow \left(p\underset{\dot{}}{\vee }q\in B\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\right)$$
26	25	rexbidv	$$⊢y=p\underset{\dot{}}{\vee }q\to \left(\exists r\in A\left(p\ne q\wedge \left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)\leftrightarrow \exists r\in A\left(p\underset{\dot{}}{\vee }q\in B\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\right)$$
27		r19.42v	$$⊢\exists r\in A\left(p\ne q\wedge \left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)\leftrightarrow \left(p\ne q\wedge \exists r\in A\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)$$
28		r19.42v	$$⊢\exists r\in A\left(p\underset{\dot{}}{\vee }q\in B\wedge \left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(p\underset{\dot{}}{\vee }q\in B\wedge \exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
29	26 27 28	3bitr3g	$$⊢y=p\underset{\dot{}}{\vee }q\to \left(\left(p\ne q\wedge \exists r\in A\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)\leftrightarrow \left(p\underset{\dot{}}{\vee }q\in B\wedge \exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\right)$$
30	13 29	ceqsexv	$$⊢\exists y\left(y=p\underset{\dot{}}{\vee }q\wedge \left(p\ne q\wedge \exists r\in A\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)\right)\leftrightarrow \left(p\underset{\dot{}}{\vee }q\in B\wedge \exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
31	12 30	bitri	$$⊢\exists y\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \left(p\underset{\dot{}}{\vee }q\in B\wedge \exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
32		simpll	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\right)\wedge \left(p\in A\wedge q\in A\right)\right)\to K\in \mathrm{HL}$$
33		simprl	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\right)\wedge \left(p\in A\wedge q\in A\right)\right)\to p\in A$$
34		simprr	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\right)\wedge \left(p\in A\wedge q\in A\right)\right)\to q\in A$$
35	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$$
36	32 33 34 35	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge X\in B\right)\wedge \left(p\in A\wedge q\in A\right)\right)\to p\underset{\dot{}}{\vee }q\in B$$
37	36	biantrurd	$$⊢\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\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\leftrightarrow \left(p\underset{\dot{}}{\vee }q\in B\wedge \exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\right)$$
38	31 37	bitr4id	$$⊢\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 y\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \exists r\in A\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
39	38	2rexbidva	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\exists p\in A\exists q\in A\exists y\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \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 X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
40		rexcom4	$$⊢\exists q\in A\exists y\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \exists y\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)$$
41	40	rexbii	$$⊢\exists p\in A\exists q\in A\exists y\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \exists p\in A\exists y\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)$$
42		rexcom4	$$⊢\exists p\in A\exists y\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \exists y\exists p\in A\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)$$
43	41 42	bitri	$$⊢\exists p\in A\exists q\in A\exists y\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \exists y\exists p\in A\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)$$
44	39 43	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\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\leftrightarrow \exists y\exists p\in A\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\right)$$
45		rexcom	$$⊢\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \exists r\in A\exists q\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)$$
46	45	rexbii	$$⊢\exists p\in A\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \exists p\in A\exists r\in A\exists q\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)$$
47		rexcom	$$⊢\exists p\in A\exists r\in A\exists q\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \exists r\in A\exists p\in A\exists q\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)$$
48	46 47	bitri	$$⊢\exists p\in A\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \exists r\in A\exists p\in A\exists q\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)$$
49	1 3 4 6	islln2	$$⊢K\in \mathrm{HL}\to \left(y\in \mathrm{LLines}\left(K\right)\leftrightarrow \left(y\in B\wedge \exists p\in A\exists q\in A\left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\right)$$
50	49	adantr	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(y\in \mathrm{LLines}\left(K\right)\leftrightarrow \left(y\in B\wedge \exists p\in A\exists q\in A\left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\right)$$
51	50	anbi1d	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\left(y\in \mathrm{LLines}\left(K\right)\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(\left(y\in B\wedge \exists p\in A\exists q\in A\left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)$$
52		r19.42v	$$⊢\exists p\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \exists q\in A\left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \exists p\in A\exists q\in A\left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)$$
53		r19.42v	$$⊢\exists q\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \exists q\in A\left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)$$
54	53	rexbii	$$⊢\exists p\in A\exists q\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \exists p\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \exists q\in A\left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)$$
55		an32	$$⊢\left(\left(y\in B\wedge \exists p\in A\exists q\in A\left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \exists p\in A\exists q\in A\left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)$$
56	52 54 55	3bitr4ri	$$⊢\left(\left(y\in B\wedge \exists p\in A\exists q\in A\left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists p\in A\exists q\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)$$
57	51 56	syl6bb	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\left(y\in \mathrm{LLines}\left(K\right)\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists p\in A\exists q\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\right)$$
58	57	rexbidv	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\exists r\in A\left(y\in \mathrm{LLines}\left(K\right)\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \exists r\in A\exists p\in A\exists q\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\right)$$
59	48 58	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\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \exists r\in A\left(y\in \mathrm{LLines}\left(K\right)\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)$$
60		r19.42v	$$⊢\exists r\in A\left(y\in \mathrm{LLines}\left(K\right)\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(y\in \mathrm{LLines}\left(K\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)$$
61	59 60	syl6bb	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\exists p\in A\exists q\in A\exists r\in A\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \left(y\in \mathrm{LLines}\left(K\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)$$
62	61	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\left(\left(y\in B\wedge \left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\wedge \left(p\ne q\wedge y=p\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \exists y\left(y\in \mathrm{LLines}\left(K\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)$$
63	44 62	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\left(p\ne q\wedge \neg r\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }q\right)\wedge X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\leftrightarrow \exists y\left(y\in \mathrm{LLines}\left(K\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\right)\right)$$
64	8 63	bitr4id	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(\exists y\in \mathrm{LLines}\left(K\right)\exists r\in A\left(\neg r\underset{\dot{}}{\le }y\wedge X=y\underset{\dot{}}{\vee }r\right)\leftrightarrow \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 X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
65	7 64	bitrd	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(X\in P\leftrightarrow \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 X=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$