Theorem isline

Description: The predicate "is a line". (Contributed by NM, 19-Sep-2011)

	Ref	Expression
Hypotheses	isline.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	isline.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	isline.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	isline.n	$$⊢N=\mathrm{Lines}\left(K\right)$$
Assertion	isline	$$⊢K\in D\to \left(X\in N\leftrightarrow \exists q\in A\exists r\in A\left(q\ne r\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isline.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		isline.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		isline.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		isline.n	$$⊢N=\mathrm{Lines}\left(K\right)$$
5	1 2 3 4	lineset	$$⊢K\in D\to N=\left\{x|\exists q\in A\exists r\in A\left(q\ne r\wedge x=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right\}$$
6	5	eleq2d	$$⊢K\in D\to \left(X\in N\leftrightarrow X\in \left\{x|\exists q\in A\exists r\in A\left(q\ne r\wedge x=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right\}\right)$$
7	3	fvexi	$$⊢A\in \mathrm{V}$$
8	7	rabex	$$⊢\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\in \mathrm{V}$$
9		eleq1	$$⊢X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\to \left(X\in \mathrm{V}\leftrightarrow \left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\in \mathrm{V}\right)$$
10	8 9	mpbiri	$$⊢X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\to X\in \mathrm{V}$$
11	10	adantl	$$⊢\left(q\ne r\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\to X\in \mathrm{V}$$
12	11	a1i	$$⊢\left(q\in A\wedge r\in A\right)\to \left(\left(q\ne r\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\to X\in \mathrm{V}\right)$$
13	12	rexlimivv	$$⊢\exists q\in A\exists r\in A\left(q\ne r\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\to X\in \mathrm{V}$$
14		eqeq1	$$⊢x=X\to \left(x=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\leftrightarrow X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)$$
15	14	anbi2d	$$⊢x=X\to \left(\left(q\ne r\wedge x=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\leftrightarrow \left(q\ne r\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right)$$
16	15	2rexbidv	$$⊢x=X\to \left(\exists q\in A\exists r\in A\left(q\ne r\wedge x=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\leftrightarrow \exists q\in A\exists r\in A\left(q\ne r\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right)$$
17	13 16	elab3	$$⊢X\in \left\{x|\exists q\in A\exists r\in A\left(q\ne r\wedge x=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right\}\leftrightarrow \exists q\in A\exists r\in A\left(q\ne r\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)$$
18	6 17	bitrdi	$$⊢K\in D\to \left(X\in N\leftrightarrow \exists q\in A\exists r\in A\left(q\ne r\wedge X=\left\{p\in A|p\underset{\dot{}}{\le }\left(q\underset{\dot{}}{\vee }r\right)\right\}\right)\right)$$