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		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}$$
9		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$$
10		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$$
11	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$$
12	8 9 10 11	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$$
13	12	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)$$
14		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)$$
15		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)$$
16	14 15	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)$$
17	16	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)$$
18		ovex	$$⊢p\underset{\dot{}}{\vee }q\in \mathrm{V}$$
19		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)$$
20		eleq1	$$⊢y=p\underset{\dot{}}{\vee }q\to \left(y\in B\leftrightarrow p\underset{\dot{}}{\vee }q\in B\right)$$
21		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)$$
22	21	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)$$
23		oveq1	$$⊢y=p\underset{\dot{}}{\vee }q\to y\underset{\dot{}}{\vee }r=\left(p\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r$$
24	23	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)$$
25	22 24	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)$$
26	25	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)$$
27		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)$$
28	26 27	syl6bbr	$$⊢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)$$
29	20 28	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)$$
30	19 29	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)$$
31	30	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)$$
32		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)$$
33		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)$$
34	31 32 33	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)$$
35	18 34	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)$$
36	17 35	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)$$
37	13 36	syl6rbbr	$$⊢\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)$$
38	37	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)$$
39		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)$$
40	39	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)$$
41		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)$$
42	40 41	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)$$
43	38 42	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)$$
44	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)$$
45	44	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)$$
46	45	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)$$
47		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)$$
48		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)$$
49	48	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)$$
50		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)$$
51	47 49 50	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)$$
52	46 51	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)$$
53	52	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)$$
54		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)$$
55	54	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)$$
56		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)$$
57	55 56	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)$$
58	53 57	syl6rbbr	$$⊢\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)$$
59		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)$$
60	58 59	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)$$
61	60	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)$$
62	43 61	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)$$
63		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)$$
64	62 63	syl6rbbr	$$⊢\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)$$